Основы математики

Sylvain Poirier

http://settheory.net/

1.Первые основы математики

1.1. Основы математики. Введвние.

Математика –это наука, изучающая системы абстрактных элементарных объектов, воспринимаемых как существующие отдельно от нашего мира, единственная цель которых –быть точными, недвусмысленными (два объекта могут быть равными или разными, связанными друг с другом или нет; операция дает точный результат, и т.д.). Математика разделена на много областей: концепций или объектов изучения, которые можно формально определить как разнообразие (аксиоматичных) теорий. Каждая теория изучает какую-либо предположительно фиксированную систему (мир математических объектов), вид которой изначально определен (выбран из всех возможных математических систем) с помощью математического описания, которое называется основой этой теории.
Некоторые теории можно расположить в виде иерархий , где одни теории могут быть основой для других. Например, основы нескольких теорий могут иметь общую часть, которая представляет собой более простую теорию, модификации которой применимы к ним всем.
Наука, изучающая основы математики как единого целого, была разработана как область математики под названием математическая логика,Она состоит (как и любая другая область) из определений и теорем, описывающих системы объектов (общая форма объектов, теории и их соответствующие, возможно, изученные системы), отвечая на многие философские вопросы и создавая общую структуру для всей математики.
Во-первых и всегда, основы математики или теории –это то, что о них известно или выборочно принято. Затем изучение продвигается вперед путем выбора некоторых возможных следствий этой теории : новых понятий и информации вытекающих из предыдущей основы и присоединяющихся к ней, чтобы сформировать следующую основу. Другие варианты, не выбранные в данный момент, могут быть выбраны позднее, так как основа, на которой они могут возникнуть, продолжает существовать. Таким образом, совокупность возможных следствий уже образует некую минимальную «реальность» и можно сказать, что они ее исследуют, пока не возникнет возможность продемонстрировать нечто лучшее (см. Теорему полноты, представленную в Части 3). Фундаментальная работа состоит в том, чтобы, исходя из простой первоначальной основы, разработать более полную основу, которая наилучшим образом облегчает создание дальнейших интересных следствий данной теории.
Несмотря на элементарность математических объектов, основы математики (где основа каждой основы, в отличие от обычных математических работ, продвигается вперед от предполагаемой основы),оказываются достаточно сложными (хотя и не настолько, как физическая «теория всего»):будучи сами по себе одной из ветвей математики, укорененной на них, основы математики образуют не стартовую точку, а широкую движущую силу, петлей приблизительно соединяющуюся с самой собой, образованную из более или менее сложных этапов.
(Это напоминает то, как в словарях дается определение каждого слова с помощью других слов, или это напоминает другую науку конечных систем: компьютерное программирование. Действительно, компьютерами можно просто пользоваться, зная, чтó ты делаешь, но не зная, почему это работает. Их работа основана на программном обеспечении, которое было написано на некоем языке, потом скомпилировано другим программным обеспечением, а также на аппаратном обеспечении («железе») и процессоре, которые были сконструированы и изготовлены при помощи компьютеров. И это гораздо лучше, чем обстояло дело при зарождении этой области науки.)
И все же эта петля является истинной основой математики, поскольку ее части богаты полезными понятиями для разнообразных областей математики. В ней доминируют две теории:
Теория множеств изучает вселенную «всех математических объектов»,от простейших до самых сложных, таких как бесконечные системы.Но в деталях она имеет неограниченное разнообразие возможных вариантов (не всегда одинаковых).
Теория моделей это общая теория теорий (описывающая их формализм как систему символов) (миров) объектов, которые они могут описывать, называемые их моделями (их возможными интерпретациями). Ее дополняет теория доказательств (описывающая правила доказательств). Она по существу уникальна, она придает ясное и окончательное значение понятиям теории и теоремы в каждой теории.
Каждая из них –это естественная структура, позволяющая дать формальное представление другой: теория моделей описывает каждую теорию множеств как аксиоматическую теорию, а также и ее саму лучше представить как следствие теории множеств (построение теорий и моделей как сложных объектов в теории множеств)чем как отдельную теорию. Таким образом, теория множеств –это одновременно и базовая структура для теории моделей, и ее объект изучения (но эти две копии теории множеств нельзя путать, даже если они построены по одним и тем же правилам). Но завершение этих формальных представлений потребует много времени.
Специалисты по основам математики выбрали аксиоматическую теорию множеств Цермело-Френкеля (сокращенно ЦФ; или ЦФВ - Система Цермело-Френкеля с аксиомой выбора) как мощную теорию в увеличенном круге основания, которая может доказать многие сложные пропозиции или их недоказуемость.
Математика начинается с введения некоторых простых понятий (круге основания), которые, на первый взгляд, не основаны на других. Естественно начать с теории множеств, которая не полностью формализована как аксиоматическая теория. Ее обычно представляют как популяризированную или НЕЯВНУЮ версию ЦФВ, признавая ее аксиомы как необходимые или очевидные.
Но ЦФВ не является идеальным стартовым ориентиром для начал математики. Ее аксиомы менее НАТУРАЛЬНЫ, чем кажутся; полное обоснование их существования тоньше, чем то, что они просто результаты интуиции, исторически выбранные для связности и удобства результирующей системы. Но аксиомы только приносят свои требования в рассматриваемый мир внутри необходимой существующей коллекции теорий моделей, которая придает смысл этим аксиомам. Также, ЦФВ assumes рассматривает всё как множества, множества множеств и т.д., построенные над пустым множеством. Но обычная математика при разработке на этой основе несколько громоздка и использует много объектов, не рассматриваемых как множества. Поскольку множества могут играть все эти роли, это не обязательно было формализовывать, но это по-прежнему представляет собой расхождение между «теорией» и практикой математики.

1.2. Переменные, множества, функции и операции

Давайте начнем рассмотрение математики с теории множеств, более непосредственно подходящей для математической практики, имеющей больше понятий и объяснений о контексте основ (теория моделей) и ее основных тонкостей (парадоксов). Начнем с трех понятий (видов объектов): элементов, множеств и функций; и по мере необходимости будем развивать ФОРМАЛЬНОЕ ПРЕДСТАВЛЕНИЕ, вместе с другими понятиями, символами и аксиомами, которые можно рассматривать как примитивные или нет, и которые могут быть необязательными.

Константы
Символ константы –это символ, обозначающий уникальный объект, который называют ее значением. Примеры: 3, Ø, ℕ. В английском языке это имена собственные и названия, начинающиеся с определенного артикля (в единственном числе без дополнения).

Свободные и связанные переменные
Символ переменной (или просто переменная)–это символ без закрепленной интерпретации. Каждая возможная интерпретация придает ему определенное значение и таким образом рассматривает его как константу.
Можно представить себе это как нечто, находящееся в пределах коробки. Если смотреть изнутри коробки, это можно использовать как константу : ее называют свободной или фиксированной. Если смотреть снаружи, ее возможные значения рассматриваются во всем своем разнообразии: такую переменную называют связанной.

Диапазоны и множества
Диапазон переменной–это ее значение, когда она рассматривается как связанная: это знание (определение) всех ее возможных или допустимых значений, которые называются элементами этого диапазона. Любой диапазон переменной называется множеством. (Это «знание» в отличие от человеческой мысли, - абстрактное целое, которое может включать бесконечные количества объектов; элементы рассматриваются в массе: неупорядоченными, без учета контекста). Переменная имеет диапазон, если его можно связать, т.е. когда возможен обзор, охватывающий все ее возможные значения.
Говорят, что переменная ИЗМЕНЯЕТСЯ В ПРЕДЕЛАХ/ЗАКЛЮЧАЕТСЯ В ПРЕДЕЛАХ/ОХВАТЫВАЕТ множества, если она связана с этим множеством как с диапазоном. В данном диапазоне может быть представлено любое количество переменных, независимо друг от друга и от других переменных.
Кантор определял множество как «соединение в единое целое хорошо различимых предметов нашего созерцания или нашего мышления». Он объяснял Дедекинду : «Если совокупность элементов множественности можно представить как «существующие одновременно», так, чтобы их можно было воспринимать как «единый объект» (или «завершенный объект»), я называю это непротиворечивой множественностью или «множеством».» (Мы выразили эту «множественность» как множественность значений переменной).
Он описал противоположный случай как «противоречивую множественность» где «признание совместного существования всех ее элементов ведет к противоречию». Но непротиворечивости не достаточно для того, чтобы дать общее определение множеств: непротиворечивость не означает истинности (противоположное этому заявление может быть истинно, но недоказуемо); факты непротиворечивости сами представляют собой распространенный случай недоказуемых истин; и две множественности, которые отдельно друг от друга непротиворечивы, могут противоречить друг другу (Парадокс всемогущества).
Систематическое переименование связанной переменной во всем объеме «коробки» в другой символ, не используемый в том же контексте (той же коробке), с тем же диапазоном, не меняет значения целого. На практике, одна и та же буква может обозначать несколько отдельных связанных переменных (у которых отдельные коробки), которые могут принимать различные значения, так как их никогда не интерпретируют (свободно) вместе, и поэтому они не сравнимы. Обычный язык постоянно это делает, используя небольшое количество переменных символов («он», «она», «оно»...)

Функции
Функция–это любой объект f ведущий себя как переменная зависящая от другой переменной с диапазоном, обозначенным Dom f, называемого ее аргументом, диапазон которого обозначается символом Dom f : когда этот аргумент фиксированный (обозначенный как символ x), f превращается в константу (обозначена как f(x)). Другими словами, f содержит следующие данные:

Операции
Операция –это обобщенная функция к случаю конечного списка аргументов (переменных с данными относительными диапазонами), дающая результат (значение), когда все аргументы фиксированные. Число n аргументов называют его арностью ; операция называется n-арной. Ее называют унарной, если n=1 (это функция), бинарной если n=2, тернарной если n=3... Нульарные операции бесполезны, поскольку их можно заменить их значением; мы увидим, как создавать операции с арностью > 1 посредством функций.
Значение бинарной операции f над ее фиксированными аргументами называется (со значениями, придаваемыми)) x и y, обозначается f(x,y). Так что, вместо символов, аргументы представлены левым и правым положением в скобках, которые заполняются любым выражением, которое придает им желаемое значение.

1.3. Структура теорий: объекты, метаобъекты, типы и структуры

Основание теории имеет два уровня. Во-первых, мы должны установить формальное представление которое будет содержать теорию: логическую структуру, или грамматику. Это определяет, каким образом можно выразить содержание теории и вывести ее следствия. Вначале, мы введем только 2 из этих потенциально полезных видов формального представления. Теории в формальном представлении логики первого порядка будут называться здесь генерическими теориями ; особое формальное представление будет введено для теории множеств. В третьей части будут представлены другие виды формального представления.
Каждая теория имеет свои собственные понятия, обычно обозначаемые общими названиями. Понятие –это вид переменных, допускаемых в языке теории, которые в каждой модели (интерпретации теории) относятся к диапазону возможных значений этого вида переменной. Объект теории в модели –это любой допускаемый элемент любого понятия (возможное значение любой переменной) теории в этой модели. разные возможные формальные представления, кроме представления в нашей теории множеств, будут управлять переменными следующим образом: их единственными принятыми понятиями будут типы их количество обычно является конечным), классифицирующие и переменные, и объекты. Каждый объект будет принадлежать только к одному типу - типу переменных, которые могут давать ему название.
В имплицитной структуре теории моделей мы обсудим несколько теорий T и их возможные модели M (системы, описываемые T). Итак, переменные T и M –это переменные теории моделей, соответственно принадлежащие ее понятиям «теория» и «модель». Но когда мы будем концентрироваться на одной теории (множеств) с предположительно фиксированной моделью, эти переменные будут фиксированными и, таким образом, исчезнут вместе с понятиями, к которым они относятся, так как станут имплицитными. Из теории моделей, структура будут сведена к теории одной модели. Различные версии теории (одной) модели соответствуют различным формальным представлениям для теорий, но по-прежнему имеют много сходств (общих понятий). (Мы не будем здесь указывать формальные представления, которыми выражены сами теория моделей и теория одной модели.)
Примеры понятий из различных теорий:

Теория   Виды объектов (понятии))
Общая теория    чистые элементы классифицированные по типам
Теория наборов    Элементы, комплекты, функции, операции, отношения, tuples ...
Теория моделей    Теории, системы и их компоненты (см. ниже)
Теория одной модели    объекты, символы, типы, структуры (операторы, предикаты), формулы...
Арифметика    Натуральные числа
Линейная алгебра    Векторы, скаляры...
Геометрия    Точки, линии, круги...

Вся система изготовлена ​​из данных теории T и системы M что является моделью T, представляет собой модель [T,M] из теории одной модели T1. Понятия теории одной модели, обычно интерпретируется в [T,M],классифицирует компоненты T («тип», «символ», «формула»...), а те, из M («объект» , и инструменты для интерпретации T там). Но те же представления о теории одной модели можно интерпретировать в своём другом моделе [T1,[T,M]],которая будет выражаться, поставив префикс мета-на них.
По понятии своего «обьекта»,теория одной модели отличает объекты T в M среди своих объектов в [T,M], которые являются мета-объектами. Таким образом, каждый объект будет мета-объектом. Однако на практике мы будем делать исключение и называть мета-объектами только то, что не является объектами. .
В отличие от теории множеств, теория одной модели дает диапазон каждой переменной своей изученной теории. Однако каждый диапазон, то есть понятие, является только мета-объектом.
Как только зафиксировано формальное представление, приходит очередь содержания основ теории, которое является отличительной чертой теории и пытается определить предполагаемый вид ее моделей и их различные концепции (вокабуляр). Эта основа теории состоит из (математически условного, но интуитивно сконструированного) тройного списка данных, структурированных в виде 3 слоев:
1) Список абстрактных типов цель которых – установить типы объектов;
2)Язык : список символов структуры, цель которых –установить отношения объектов к конкретным типам;
3)Список формул, называемых аксиомами выбранных из множества всех возможных закрытых формул, т.е 1.4.).
Вместо того,чтобы быть описанным c помошью теории одной модели, та же система, [T,M]может быть понята как переведено на теории множеств, представляющая компоненты из Tкомпонентами теории множеств в то время как только те из M становятся объектами, следующим образом. Переменные из Tсохраняются в качестве переменных теории множеств. Каждый абстрактный тип становится свободной переменной, значением которой является набор по имени интерпретированный тип. Точнее, используя стандартную форму перевода, которая подходит для любой генерической теории: все объекты будут переведены в чистые элементы (в отличие от обычной точки зрения, что геометрия определяет линии как множества точек).
Абстрактные типы и структурные символы все переводятся как свободные переменные, которые остаются свободными, пока модель остается фиксированной. Их значения являются основными компонентами модели, компонентами, которые определяют ее. Это объединяет все теории (арифметика, геометрия ...) и их разнообразие возможных моделей, в той же теории множеств с фиксированной модели также называется как вселенная).

1.4. Структуры и выражения


Структуры
Структуры (и, таким образом структурные символы) могут быть 2 видов: операторы и предикаты. Как переменная теории множеств, значение каждого символа оператора является оператором оператор, т.е. операция, где диапазон каждого аргумента представляет собой тип, и значения относятся к одному типу; арность (или список аргументов предоставленных как зона вокруг символа), абстрактный тип каждого аргумента и тип значений даны с каждым символом. Нульарный оператор –это постоянный символ, напрямую называющий фиксированный объект. Но тем не менее это свободная переменная теории множеств. Унарный оператор, т.е. функция, будет называться функтор.
Модель завершается стандартным специальным типом: типом булевых выражений, состоящих из обоих элементов «истинно» (1) and «ложно» (0). Переменная этого типа (за пределами теории) называется Булева переменная. Ее добавление к списку типов обобщает операторы до пара-операторовпара-операторов. A Связка– это пара-оператор с только булевыми аргументами и значениями. Предикат –это пара-оператор с одним или более аргументами, среди которых нет булевых, и с булевыми значениями. Структура–это оператор или предикат.
Структуры (интерпретация символов с языка теории в моделе) дают каждому элементу любого типа свои роли возможных сложных объектов. В теории множеств, роль множеств дано бинарным предикатом ∈ для любого элемента: x и любого множества E, утверждение, что (значение) x является возможным значением переменной с диапазона E, написана xE (которая гласит, что : x есть в E,или или элемент из E). ZFC теоряи множеств определяется как общая теория с одним типом «множества»,только одной структуры символа ∈ , и аксиомой.Но наша теория множеств не будет общим, и будет включать в себя другие символы способствуя приданию их роли наборам, функциям и другим типов объектов.
функции играют свою роль с помощью функтора Dom  (задавая их области) и оценщика функции ,бинарным оператором давая значение f(x) любой функции f в любой элемент x из Dom f.
Теория одной модели, формализованная как генерическая теория, будет придавать «типам» двойную роль абстрактных и интерпретированных типов. Также, те же мета-объекты могли бы играть роли структурных символов и структур, за исключением того, что понятие «структуры» будет включать другие операции между типами, помимо операций, обозначенных символами (мы не можем допустить их «все» независимо от внешней вселенной, из которой они взяты, которая не релевантна здесь).

Terms and formulas
Для любого данного списка абстрактных типов и символов структуры теории, a термин является конечной системой вхождений символов, с целью назначить объектам (его значение) как только модель и значения свободных переменных зафиксированы. (Вхождение символа –это его появление где-то, например, «x+x» имеет два вхождения х и одно вхождение +.). Мы называем формулой систему, сходную с термом, но без булевых значений. Выражение может быть термом или формулой.
Выражения могут использовать следующие виды символов :
Выражения строятся последовательно, каждое как данные (вхождение) символа, называемого его корнем, и список ранее построенных выражений (и, возможно, переменных символов). Этот корень определяет тип значений (и таким образом проводит различие между термами и формулами) и формат этого списка (количество пунктов и тип каждого из них). Для символа пара-оператора, этот формат задается списком его аргументов.
Первые термы –это термы, сведенные к вхождению символа константы или переменной, они называются атомные термы. Булевы константы 1 и 0 (нульарные связки) – это первые формулы.
Для других символов требуется непустой список, таким образом, им нужны условные знаки, чтобы его представить. Большая часть символов бинарных пара-операторов выглядят как условный знак между двумя аргументами (добавление обозначается x+y вместо первоначального формата операций +(x,y)); другие (умножение, степень) обозначаются неявно, без использования условного обозначения. Другие символы выражаются несколькими условными знаками, устанавливающими границы пунктов списка. Скобки могут или компоновать буквенные изображения символов как интерпретатор функции, или использоваться для того, чтобы выделить под-выражения и их соответствующие корни, как в (x+y)n.
Выражение закрыто, если оно не имеет свободной переменной (все переменные связаны с связками см. 1,7), так что его значение зависит только от системы объектов (модели) интерпретирующей типы и символы теории. Списокаксиом, выбранный из множества замкнутых формул, выражает необходимые свойства моделей, т.е. выбор систем, где все эти аксиомы истинны, чтобы они могли быть«возможными моделями»теории, исключив из названия «модели» любую систему, где аксиома не верна.

Структуры определённые выражениями; классы
В теории одной модели структура (оператор или предикат) это любая операция между типами объектов (например, объекты, названные структурными символами), определяемая выражением (термином или формулой) и списком выбранных свободных переменных чтобы связать в роли аргументов. Эта структура зависит от других переменных оставшихся свободными, называемых ее параметрами (в то время как связанные переменные внутри выражения, невидимые снаружи, здесь не учитываются). Класс унарный предикат рассматриваемый как множество объектов, для которых он истинный.
Давайте расширим язык теории, введя один (или более) структурный символ. Если «константы» (то есть, нульарные константы ) ведут себя, как свободные переменные, их роль могут выполнять обычные переменные теории. Это можно использовать, чтобы назвать структуру, определяемую выражением (или одним из конечного списка выражений), тем самым сокращая это выражение. В этом случае, такой символ может быть связан (совпасть по диапазону со структурами, которые являются его предполагаемыми значениями) путем связывания параметров этого выражения. Но в других случаях (символы с ненулевой арностью, могущие представлять любую структуру, даже структуру, не определяемую параметрами), эти символы, как правило, больше не могут быть связанными, поскольку никакая аксиома не может формально заявить, что они совпадают по диапазону со всеми операциями данной арности между данными типами объектов.
Назовем инвариантной структурой любую структуру, определяемую без параметров. Каждый символ в языке теории представляет инвариантную структуру (которую он определяет без параметров). Наоборот, инвариантные структуры могут быть названы новыми символами, которые будут добавлены к языку теории, сохраняя ее глубокий смысл (доказуемость, структуры, инвариантные структуры...). Такие правила для разработки теории подробно изложены в п. 3.2.

1.5. Связки

Вот наиболее полезные связки в порядке арности n > 0, по своим свойствам для всех значений логических переменных (заменяемых формулами) A, B, C.
n=1 : отрицание ¬ обменивает булевы выражения (¬A читается «не как A»): ¬1 ⇔ 0, ¬0 ⇔ 1, ¬(¬A) ⇔ A. обозначается также корнем из аргумента (формируя другой символ в том же формате)): (xy) ⇔ ¬(x=y) («x отличается от y»); xE ⇔ ¬(xE) («x не принадлежит к E»).
in
n=2 :
 ∧  (и): верно только тогда, когда оба аргумента верны;
 ∨  (или): верно, за исключением случаев, когда оба аргумента ложны;
 ⇒  : A ⇒ B может быть прочитано как «A подразумевает B», «A -достаточное условие для B», или «B является необходимым условием A», и означает ((¬A)  ∨ B). Когда это верно за исключением случаев, когда A истинно, а B is false, ложно, это означает, что если верно A, то B также верно, но в противном случае оно не дает нам информации (будучи истинно).
Формула (¬B ⇒ ¬A) называется контрапозитивной   из (A ⇒ B), и эквивалентна ей.
 ⇔  (эквивалент), равенство логических значений: (A ⇔ B) ⇔ ((A ⇒ B) ∧ (B ⇒ A)). Доказательство что A ⇔ B может быть получено из импликации (A ⇒ B), то другой (B ⇒ A), называется его обратное.
Его отрицание AB можно также прочитать как отрицание аргумента (A ⇔ ¬B), либо как «исключающее или» ((A ∨ B) ∧ ¬(A ∧ B)). Отрицания обменивают различные связки:
(A ∨ B)
⇎ (¬A  ∧ ¬B)
(A ∧ B)
⇎ (¬A ∨ ¬B)
(A ⇒ B)
⇎ (A ∧ ¬B)
Это превращает свойства ассоциативности и дистрибутивности в различные формулы:
((A ∧ B) ∧ C)
 ⇔ (A ∧ (B ∧ C))
((A ∨ B) ∨ C)
 ⇔ (A ∨ (B ∨ C))
(A ⇒ (B ⇒ C))
 ⇔ ((A ∧ B) ⇒ C)
(A ⇒ (B ∨ C))
 ⇔ ((A ⇒ B) ∨ C)

(A ∧ (B ∨ C))
 ⇔ ((A ∧ B) ∨ (A ∧ C))
(A ∨ (B ∧ C))
 ⇔ ((A ∨ B) ∧ (A ∨ C))
(A ⇒ (B ∧ C))
 ⇔ ((A ⇒ B) ∧ (A ⇒ C))
((A ∨ B) ⇒ C)
 ⇔ ((A ⇒ C) ∧ (B ⇒ C))
((A ⇒ B) ⇒ C)
 ⇔ ((A ∨ C) ∧ (B ⇒ C))
(A ∧ (B ⇒ C))
 ⇔ ((A ⇒ B) ⇒ (A  ∧ C))
n ≥ 3 : последовательности  ∧  (конъюнкции) такие как (A ∧ B ∧ C), а  ∨  (дизъюнкции) такие как (A ∨ B ∨ C) получают путем удаления скобок благодаря ассоциативности. Утверждение конъюнкции равнозначного утверждению всех его компонентов. Кроме того, любая последовательность формул связанных  ⇔  и  ⇒  сокращает последовательность требований (связанных  ∧ ) каждого звена между соседними формулам:
0
 ⇒ A ⇒ A ⇒ 1
A)
 ⇔ (A ⇒ 0) ⇔ (A ⇔ 0)
(A ⇒ B ⇒ C)
< /table>
 ⇔ ((A ⇒ B) ∧ (B ⇒ C)) ⇒ (A ⇒ C)
(A ⇔ B ⇔ C)
< /table>
 ⇔ ((A ⇔ B) ∧ (B ⇔ C)) ⇒ (A ⇔ C)
(A ∧ A) ⇔ (A ∧ 1)
 ⇔ A ⇔ (A ∨ A) ⇔ (A ∨ 0) ⇔ (1 ⇒ A)  ⇔ (A ⇔ 1)
(B ∧ A) ⇔ (A ∧ B)
 ⇔ (A ∧ (A ⇒ B)) ⇒ B ⇒ (A ∨ B)& nbsp;⇔ (B ∨ A)
Аксиомы равенства
для любого функтора T и объектов x, y (что может символизировать термы с параметрами),
x=y ⇒ T(x)=T(y)
Аналогично для любого унарного предиката A мы имеем x=y ⇒ (A(x) ⇔ A(y)).
Таким образом, равенство между термами x=y позволяет заменять любое вхождение (я) x на y в любом выражении без влияния на результат. Это относится, в частности, к случаям, когда символ определен термом: они равны, и взаимозаменяемы в любом выражении. Также аксиомы и другие законы выражаются с использованием переменных символов заменяемых термами в их использовании.

1.6. Классы в теории множеств


Теория множеств в создании цикла
Теория одной модели не может быть полностью формализована в логике первого порядка (требуется аксиома второго порядка чтобы исключить бесконечно большие «выражения» и «доказательства », см. часть 3), но только при переводе в теорию множеств. Как компоненты ее модели [T, M] названы там свободными переменными, их изменчивость создает это множественно-теоретическое выражение теории моделей (общий обзор основ математики).
Теперь пусть T0 будет множество теоретическим выражением внешней теории, что соответствует T (определяется по тем же правилам): каждый компонент T0 переводится в T преобразованием его в замкнутый терм (по-прежнему теории множеств) определяя его образ в T. Таким образом, модель M из T косвенно является также моделью из T0.
Но мы выберем теории T как формализацию теории множеств (переведенную как родовая теории методом объясненным в 1.8 и 1.9), интерпретируя его концепции в M. Таким образом наше выше установленное использование теоретической концепции множество во внешней вселенной необходимо будет отличить от него путем добавления префикса «мета-» .
теоретические концепции множеств могут быть хорошо отражены интерпретацией их мета-множеств, но их не следует путать. Вместо стандартного представления всех объектов в виде чистых мета-элементов, роль множеств обычно будут играть мета- множества из тех же элементов (аналогично и для функций), позволяя любому множеству E быть классом (определенным с xE аргументом x и параметром E), в то время как любой класс является мета-множеством объектов. Но некоторые мета-множества объектов, будучи неопределимыми, не являются классами; и некоторые классы, такие как вселенная (класс всех объектов, определяются путем 1), не являются множествами.

Определенность классов
Классы являются очень общим видом понятий, которые заменят типы для выражения теории множеств. Действительно, все объекты должны быть включены в качестве «элементов» которые могут принадлежать множествам (чтобы избежать бесконечного деления на множества элементов, множества, функции, смешанные множества...). Таким образом, понятия множеств и функций будут представлять собой классами названные символы: множество = «представляет собой множество», Fnc = «функция».
(Для этого мы могли бы сохранить 3 типа, где каждое множество будет включено дважды, как множество и элемент, определенные функтором из множеств к элементам. И то же самое для функций. но этой идеи все равно недостаточно для нашей теории множеств которой потребуется больше классов как понятий)
В общих теориях, синтаксическая коррекция выражения (что подразумевается в понятии «выражения») гарантирует, что оно примет определенное значение, для всех данных в модели с фиксированной системой значений ее свободных переменных в этой модели. Но в теории множеств, это по-прежнему может зависеть от ее свободных переменных. Таким образом, структура или выражение 𝓐 будет названо определенной когда он на самом деле принимает значение для данных значений своих аргументов в модели. Это определенное состояние 𝓐 само по себе является определенным предикатом (выраженным формулой) d𝓐, с теми же свободными переменными. Выражения должны использоваться только, где они определены, что и будет сделано естественно.
Классы определяются определенными одноместными предикатами. Мета-область любой унарной структуры 𝓐, это класс определенный d𝓐, с теми же аргументами и параметрами, и называется его классом определенности..
Определенное состояние (xE) установлено Set(E)). Состояние оценщика функции f(x) это (Fnc(f) ∧ xDom f). Но определенность последней формулы должна быть объяснена следующим образом.

Расширенные определенности
теория с частично определенной структурой может быть формализована (переведена) как теория с одним типом и везде определенными структурами, сохраняя нетронутыми все выражения и их значения, где они определенные: модели переводятся в одном направлении, путем придания условных значений неопределенным структурам (например, постоянное значение), а в обратном направлении, путем игнорирования этих значений. Таким образом, выражение с неопределенным подвыражением могут быть признано определенным, если его значение не зависит от этих дополнительных значений.
Для всех предикатов 𝓐 и 𝓑, давайте придадим 𝓐 ∧ 𝓑 и 𝓐 ⇒ 𝓑 одно и то же условие определенности (d𝓐 ∧ (𝓐 ⇒ d𝓑)) (нарушая для 𝓐 ∧ 𝓑, симметрию между 𝓐 и 𝓑, которую не обязательно восстанавливать). Таким образом, они будут рассматриваться как определенные, если 𝓐 ложно и 𝓑 не является определенным, с соответствующими значениями 0 и 1.
Это гарантирует определенность самих условий определенности, а также d𝓐 ∧ 𝓐 и d𝓐 ⇒ 𝓐 (соответственно расширеняя 𝓐 на 0 и 1 где это не было определенным). Формулы 𝓐 ∧ (𝓑 ∧ 𝓒) и (𝓐 ∧ 𝓑) ∧ 𝓒 имеют одно и то же условие определенности (d𝓐 ∧ (𝓐 ⇒ (d𝓑 ∧ (𝓑 ⇒ d𝓒)))).
Для любого класса 𝓐 и любого унарного предиката 𝓑 определенного во всех 𝓐, класс определенный (всюду определенным) предикатом (𝓐 ∧ 𝓑), называется подкласс 𝓐 определяемый на 𝓑.

1.7. Связанные переменные в теории множеств

последний вид символообразующих выражений - это связки (связывающие символы), которые связывают одну (или более) переменные (скажем, х) с выражением F, которое использует переменную х в дополнение к переменным символам , которые присутствуют (со значением) снаружи. Такой символ таким образом отделяет «внутреннее» подвыражение F с помощью x как свободное, с «наружи» где x связан. Выражение закрыто если все его переменные связаны (содержатся связками).
Таким образом, он принимает в качестве данных, символ x и выражение F, и придает значение в зависимости от структуры, с аргументом x, определяемым F. Это значение не может записывать всю структуру (которая не является объектом), но дает информацию от нее. Точный синтаксис отличается в теории множеств и в общей теории, которые управляют диапазонами по-разному. В общих теориях, диапазоны - это типы, неявные данные связывающих символов. Но в теории множеств, диапазон связанной переменной представляет собой множество, объект, заданный в качестве аргумента связки (как значение терма, который не использует x), в дополнение к вышеуказанным данным.
Давайте рассмотрим основные связки в теории множеств.

Определения функций термами
Определитель функции (  ∋   ↦  ) связывает переменную x с диапазоном E на терме сокращенно обозначенным как t(x) (с возможными неявными параметрами), соблюдая синтаксис (Ext(x)), иногда сокращенно обозначается как (xt(x)) когда E определяется контекстом. Определенный, если t(x) является определенным для всех x из E, он принимает функтор определяемый t и ограничивает его класс определенности до E, чтобы дать его как функцию с областью E. Этот перевод с функтора на функции, приблизительно переворачивает перевод, сделанный другим определителем функции (от функций к их роли определителей функторов в множествах).
Другие понятия будут определены как классы объектов с помощью инструментов перевода объекта в его роль, и наоборот. Для любого вида мета-объектов, играющих роль объектов (которые можно опосредованно использовать в выражениях в качестве объектов: класс как множество...), теория множеств обогатится инструментами которые позволят прямо представить их как объекты. Существующие обьекты (множества или функции) могут играть новые роли, предлагая свои инструменты новым объектам. Таким образом, единственные необходимые переводы между объектами играющими одну и ту же роль, свяжут различные полезные представления нового объекта с помощью старых.

Формализация операций и каррирование
n-арные операции выступающие в качестве n-арных операторов между n множествами, оформляются:
  • n функторами области (имеющими мало практической пользы);
  • an (n + 1)-арной оценщиком, с аргументами операции f и ее аргументами x1,…,xn, написанными f(x1,…,xn);
  • определителем операции, связующим n переменные с их соответствующими диапазонами на терме. Единственное связывание x к E и y к F на t пишется (Ex, Fyt(x,y)). Мы можем сократить (Ex, Eyt(x,y)) как (Ex, yt(x,y)).
Понятие операции может быть представлено в виде класса функций, следующим образом называемых каррирование. В качестве операции определителя (связывание n переменных) возьмем последовательность n средств определителя функции (по одному для каждой переменной, которые надо связать); а подобно оценщику, n использование оценщика функции:
f=(Ex, Fyt (x,y))
≅ (Ex ↦ (Fyt(x,y)))=g
f(x,y)
=g(x)(y)=t(x,y)
промежуточная функция g(x)=(Fyt(x,y)) с аргументом y, рассматривает x as свободный и y связанный. Но это нарушает симметрию между аргументами и теряет данные F когда E пусто. Формализация без этих недостатков будет возможна с помощью наборов(2.1.).

Отношения и множествообразующие символы
отношение выглядит как операция, но с логическими значениями, действующими в качестве предиката, аргументы которого встречаются в диапазоне множеств. The n-арные отношения оцениваются с (n+1)-арным предикатом, и определяются связывающими n переменными по формуле. Они могут быть представлены операциями по переводу Логических представлений в объекты. Но есть и другой метод.
Для любого унарного предиката 𝓡 определенного в множестве E, подкласс E определенный 𝓡 представляет собой множество (диапазон переменной x введенной в диапазоне E, так что она может быть связанной, из чего мы выбираем случаи удовлетворяющие 𝓡(x)), таким образом, подмножество E, обозначаемое {xE|𝓡(x)} (множество x в E такое, что 𝓡(x)): для всех y,
y ∈ {xE|𝓡(x)} ⇔ (yE ∧ 𝓡(y))
образователь множества {  ∈  | }, связывающий x к E на 𝓡, будет использован в качестве определяющего для унарных отношений в E, фигурирующих в качестве подмножества F от E, оцениваемые ∈ как предикаты (xF) с аргументом x. Но эти предикаты определены по всей вселенной, давая 0 вне E чьи данные будут потеряны. Это отсутствие оператора Dom  не имеет значения, так как области E как правило, определяются контекстом.
Как определитель функции (соответственно множествообразующий символ) записывает всю структуру определенную данным выражением на данном множестве, достаточно задать любой другой связующий символ на том же выражении с той же областью, словно из функтора или унарного предиката добавлен к результату что функция, соответственно множества); n-арные отношения могут быть определены в каррированной форме одним средством образователя множества и n−1 средств определителя функции.

1.8. Кванторы

Квантор является связующим символом для формулы, с логическими значениями. Квантор Q связывающий x с диапазоном E по формуле 𝓡(x), полностью пишется Q xE,𝓡(x). Иногда, область (тип или класс) ставится в качестве индекса: QEx,𝓡(x), или остается неявным (установленным контекстом): Qx,𝓡(x). Два основных квантора (под которыми и другие будут определены позже) - это:
- Квантор существования ∃, который гласит «There exists x (in...) such that... »
- Квантор всеобщности ∀, который гласит «Для всех (или: для любого) x (в...),... »).
Они могут быть мета-определяемыми с помощью мета-функции (x ↦ 𝓡(x)) с одной и той же областью в силу
(∀x,𝓡(x))  ⇔  (x ↦ 𝓡(x))=(x ↦ 1)  ⇎  (∃x, ¬𝓡(x)) ⇔  (x ↦ ¬𝓡(x)) ≠ (x ↦ 0)
В теории множеств, (∀xE,𝓡(x)) ⇔ {xE|𝓡(x)}=E. Формула (∀x,1) всегда истинна. С классами,
(∃𝓒 x,𝓡(x))
 ⇔ (∃x, 𝓒(x)  ∧ 𝓡(x)) ⇔ ∃𝓒∧𝓡 x,1
(∀𝓒 x,𝓡(x))
 ⇔ (∀x, 𝓒(x)  ⇒ 𝓡(x))
x,(𝓒(x)
 ⇔ (∃𝓒 y, x=y))

Включение между классами
Считается, что Класс 𝓐 включен в класс 𝓑 когда ∀x, 𝓐(x) ⇒ 𝓑(x). Тогда 𝓐 - это подкласс 𝓑, как ∀x,𝓐(x) ⇔ (𝓑(x) ∧ 𝓐(x)). И наоборот, любой подкласс 𝓐 включен в подкласс 𝓑 что подразумевает для любого предиката 𝓒 (в случаях определенности):
(∀𝓑 x, 𝓒(x))
 ⇒ (∀𝓐 x, 𝓒(x))
(∃𝓐 x, 𝓒(x))
 ⇒ (∃𝓑 x, 𝓒(x))
(∃𝓒 x, 𝓐(x))
 ⇒ (∃𝓒 x, 𝓑(x))
(∀𝓒 x, 𝓐(x))
 ⇒ (∀𝓒 x, 𝓑(x))

Правила доказательств для квантификаторов по унарному предикату 𝓡

Экзистенциальное введение. Если у нас есть условия t, t′, …и доказательство 𝓡(t) ∨ 𝓡(t′) ∨ …, тогда x,𝓡(x).

Экзистенциальное устранение. Если x,𝓡(x), то мы можем ввести новую свободную переменную z с гипотезой 𝓡(z) (последствия будут истинными, без ограничения общности).
Эти правила выражают смысл ∃ : переходя от t, … к ∃ затем из ∃ к z, это все равно что позволить z представлять одну из t, t′, … (не зная, какую именно). Они придают тот же смысл ∃𝓒 относительно его 2 вышеприведенных эквивалентных формул, минуя расширенное правило определенности для (𝓒 ∧ 𝓡) сосредоточив внимание на случае, когда 𝓒(x) является истинным и, следовательно 𝓡(x) является определенным.
В то время как ∃ появился как обозначение объекта, ∀ появляется в качестве правила вычета:

Универсальное Введение. Если из всего лишь гипотезой 𝓒(x) на новой свободной переменной x мы могли вывести 𝓡(x), то 𝓒 x, 𝓡(x).

Универсальное Устранение. Если 𝓒 x, 𝓡(x) и t является термом, выполняющим 𝓒(t), то 𝓡(t) .
Представляя затем устранение ∀ как замену x на t в начальном доказательстве.
Отчисления могут быть сделаны этими правилами, отражающие формулы
((∀𝓒 x, 𝓐(x)) ∧ (∀𝓒 x, 𝓐(x) ⇒ 𝓑(x)))
 ⇒ (∀𝓒 x, 𝓑(x))
((∃𝓒 x, 𝓐(x)) ∧ (∀𝓒 x, 𝓐(x) ⇒ 𝓑(x)))
 ⇒ (∃𝓒 x, 𝓑(x))
(∀𝓒 x, 𝓐(x)) ∧ (∃𝓒 x, 𝓑(x)))
 ⇒ (∃𝓒 x, 𝓐(x) ∧ 𝓑(x))

статус открытых кванторов в теории множеств
Теория множеств переводится в генерическую теорию путем преобразования в классах области кванторов:
(∃xE, 𝓡(x))
→(∃x, xE ∧ 𝓡(x))
(∀xE, 𝓡(x))
→(∀x, xE ⇒ 𝓡(x))
Теория множеств допускает только квантор над множествами, с названием ограниченный квантор, в своих формулах, что для усиления будут называться ограниченными формулами (которые определяют предикат и могут быть использованы в выражении). Но его форма перевода как родовой теории позволяет существование кванторов на любых классах (или вселенной), называемых открытыми кванторами.Формулы с открытым кванторами в теории множеств будут называться претензиями. Их использование будет существенно ограничено декларацией истины замкнутых определенных претензий. Они сначала будут аксиомами, потом теоремами (выведены из аксиом и с разными именами в зависимости от их важности: теорема является более важной, чем предложение, может быть выведена из леммы, и легко может привести к следствию.
Открытые кванторы в претензии часто будут выражены как общие артикуляции языка (неявно используя вышеуказанные правила доказательств) между их ограниченными подформулами (написанными символами теории множеств).
Образователь множества определяется претензиями. Он будет использован , чтобы показать, что класс всех множеств это не множество, создавая все эти различия между классами и множествами, а также между открытыми и ограниченными кванторами:

Теорема (парадокс Рассела). Для любого множества E существует множество F такое, что FE.
Доказательство. F={xE|Set(x) ∧ xx} ⇒ (FF ⇔ (FE  ∧ FF)) ⇔ (FF ∧ FE). ∎

1.9. Первые аксиомы теории множеств

Предикат включения ⊂ между двумя множествами E и F, определяется в EF ⇔ (∀xE, xF). В нем говорится: E входит в F, или E является подмножеством F, или в F входит E.
У нас всегда есть EE. Последствия цепи также являются включениями цепей:
(EFG) ⇔ (EF ∧ FG) ⇒ EG.
Первые аксиомы:
x,    ¬(Set(x) ∧ Fnc(x))
Fnc x,   Set(Dom x)
Для каждого терма t, ∀E, ∀(параметы), Fnc(Ext(x))
Set E,F,    EFE  ⇒ E=F (аксиома объемности).
Последний переопределяет равенство между множествами их равенством как классы (позволяя элементы в натуральном выражении): EFE означает, что E и F имеют одинаковые элементы (∀x, xE ⇔ xF) и подразумевает для любого предиката 𝓡 что (∀xF, 𝓡(x)) ⇔ (∀xE, 𝓡(x)), а так же для ∃.

Переводя определитель
При переводе теории множеств как родовой теории, определитель функции становится бесконечным символом операторов: для каждого терма t с одним аргументом (и параметром), все выражение (Ext(x)) становится символом другого оператора, аргументы которых E и параметры t. (Те, где каждое подвыражение внутри t без вхождений x является единственным вхождением параметра, достаточно, чтобы определить другие).
Следующие аксиомы могут быть прочитаны как аксиомы общей теории, на что теория множеств переводится; а те, в зависимости от терм t являются схемами аксиом (схема претензий = бесконечный список полученных претензий, заменяя дополнительный символ структуры любым возможным определяемым выражением):

Аксиомы для функций. Для каждого терма t с одним аргументом, любые значения его параметров, любого множества E где t является определенными, и любые функции f и g, первая из этих аксиом обобщает следующие 3 из них:
f=(Ext(x)) ⇔ ( Dom
 f=E ∧ (∀xE, f(x)=t(x)))
Dom
 (Ext(x))=E
xE, (Eyt(y))(x)=t(x)
( Dom
 f= Dom
 g ∧ ∀x Dom
 f, f(x)=g(x)) ⇒ f=g



File translated from TEX by TTH, version 4.03.
On 03 Oct 2013, 13:09.