Расширение по определениям

В математической логике , а точнее в теории доказательств теорий первого порядка , расширения по определениям формализуют введение новых символов посредством определения. Например, в наивной теории множеств принято вводить символ для множества , не имеющего элементов. В формальной постановке теорий первого порядка это можно сделать, добавив к теории новую константу и новую аксиому , означающую «для всех x , x не является элементом ». Затем можно доказать, что это по сути ничего не добавляет к старой теории, как и следовало ожидать от определения. Точнее, новая теория является консервативным расширением старой. ${\displaystyle \emptyset }$ ${\displaystyle \emptyset }$ ${\displaystyle \forall x(x\notin \emptyset )}$ ${\displaystyle \emptyset }$

Определение символов отношения

Пусть будет теорией первого порядка и формулой из , такой что , ..., различны и включают переменные, свободные в . Образуем новую теорию первого порядка из , добавив новый символ -арного отношения , логические аксиомы, содержащие символ и новую аксиому ${\displaystyle T}$ ${\displaystyle \phi (x_{1},\dots ,x_{n})}$ ${\displaystyle T}$ ${\displaystyle x_{1}}$ ${\displaystyle x_{n}}$ ${\displaystyle \phi (x_{1},\dots ,x_{n})}$ ${\displaystyle T'}$ ${\displaystyle T}$ ${\displaystyle n}$ ${\displaystyle R}$ ${\displaystyle R}$

${\displaystyle \forall x_{1}\dots \forall x_{n}(R(x_{1},\dots ,x_{n})\leftrightarrow \phi (x_{1},\dots ,x_{n}))}$,

называемая определяющей аксиомой . ${\displaystyle R}$

Если — формула , пусть — формула , полученная из заменой любого вхождения на (изменяя связанные переменные в , если необходимо, так, чтобы переменные, встречающиеся в , не были связаны в ). Тогда выполняется следующее: ${\displaystyle \psi }$ ${\displaystyle T'}$ ${\displaystyle \psi ^{\ast }}$ ${\displaystyle T}$ ${\displaystyle \psi }$ ${\displaystyle R(t_{1},\dots ,t_{n})}$ ${\displaystyle \phi (t_{1},\dots ,t_{n})}$ ${\displaystyle \phi }$ ${\displaystyle t_{i}}$ ${\displaystyle \phi (t_{1},\dots ,t_{n})}$

1. ${\displaystyle \psi \leftrightarrow \psi ^{\ast }}$доказуемо в , и ${\displaystyle T'}$
2. ${\displaystyle T'}$является консервативным расширением . ${\displaystyle T}$

Тот факт, что является консервативным расширением, показывает, что определяющая аксиома не может быть использована для доказательства новых теорем. Формула называется переводом в . Семантически формула имеет то же значение , что и , но определяемый символ был исключен. ${\displaystyle T'}$ ${\displaystyle T}$ ${\displaystyle R}$ ${\displaystyle \psi ^{\ast }}$ ${\displaystyle \psi }$ ${\displaystyle T}$ ${\displaystyle \psi ^{\ast }}$ ${\displaystyle \psi }$ ${\displaystyle R}$

Определение функциональных символов

Пусть будет теорией первого порядка ( с равенством ) и формулой из такой, что , , ..., различны и включают переменные, свободные в . Предположим, что мы можем доказать ${\displaystyle T}$ ${\displaystyle \phi (y,x_{1},\dots ,x_{n})}$ ${\displaystyle T}$ ${\displaystyle y}$ ${\displaystyle x_{1}}$ ${\displaystyle x_{n}}$ ${\displaystyle \phi (y,x_{1},\dots ,x_{n})}$

${\displaystyle \forall x_{1}\dots \forall x_{n}\exists !y\phi (y,x_{1},\dots ,x_{n})}$

в , т.е. для всех , ..., , существует единственный y такой, что . Сформируйте новую теорию первого порядка из , добавив новый символ -арной функции , логические аксиомы, включающие символ и новую аксиому ${\displaystyle T}$ ${\displaystyle x_{1}}$ ${\displaystyle x_{n}}$ ${\displaystyle \phi (y,x_{1},\dots ,x_{n})}$ ${\displaystyle T'}$ ${\displaystyle T}$ ${\displaystyle n}$ ${\displaystyle f}$ ${\displaystyle f}$

${\displaystyle \forall x_{1}\dots \forall x_{n}\phi (f(x_{1},\dots ,x_{n}),x_{1},\dots ,x_{n})}$,

называемая определяющей аксиомой . ${\displaystyle f}$

Пусть будет любой атомарной формулой из . Мы определяем формулу из рекурсивно следующим образом. Если новый символ не встречается в , пусть будет . В противном случае выберем вхождение в такое, которое не встречается в терминах , и пусть будет получено из заменой этого вхождения новой переменной . Тогда, поскольку встречается на один раз меньше, чем в , формула уже определена, и мы позволим быть ${\displaystyle \psi }$ ${\displaystyle T'}$ ${\displaystyle \psi ^{\ast }}$ ${\displaystyle T}$ ${\displaystyle f}$ ${\displaystyle \psi }$ ${\displaystyle \psi ^{\ast }}$ ${\displaystyle \psi }$ ${\displaystyle f(t_{1},\dots ,t_{n})}$ ${\displaystyle \psi }$ ${\displaystyle f}$ ${\displaystyle t_{i}}$ ${\displaystyle \chi }$ ${\displaystyle \psi }$ ${\displaystyle z}$ ${\displaystyle f}$ ${\displaystyle \chi }$ ${\displaystyle \psi }$ ${\displaystyle \chi ^{\ast }}$ ${\displaystyle \psi ^{\ast }}$

${\displaystyle \forall z(\phi (z,t_{1},\dots ,t_{n})\rightarrow \chi ^{\ast })}$

(изменяя связанные переменные в , если необходимо, так что переменные, встречающиеся в , не связаны в ). Для общей формулы формула формируется путем замены каждого вхождения атомарной подформулы на . Тогда выполняется следующее: ${\displaystyle \phi }$ ${\displaystyle t_{i}}$ ${\displaystyle \phi (z,t_{1},\dots ,t_{n})}$ ${\displaystyle \psi }$ ${\displaystyle \psi ^{\ast }}$ ${\displaystyle \chi }$ ${\displaystyle \chi ^{\ast }}$

1. ${\displaystyle \psi \leftrightarrow \psi ^{\ast }}$доказуемо в , и ${\displaystyle T'}$
2. ${\displaystyle T'}$является консервативным расширением . ${\displaystyle T}$

Формула называется переводом в . Как и в случае с символами отношения, формула имеет то же значение, что и , но новый символ был исключен. ${\displaystyle \psi ^{\ast }}$ ${\displaystyle \psi }$ ${\displaystyle T}$ ${\displaystyle \psi ^{\ast }}$ ${\displaystyle \psi }$ ${\displaystyle f}$

Конструкция этого абзаца применима также к константам, которые можно рассматривать как 0-арные функциональные символы.

Расширения по определениям

Теория первого порядка, полученная из путем последовательного введения символов отношений и символов функций, как указано выше, называется расширением по определениям . Тогда является консервативным расширением , и для любой формулы из мы можем сформировать формулу из , называемую переводом из в , такую, что она доказуема в . Такая формула не является единственной, но можно доказать, что любые две из них эквивалентны в T . ${\displaystyle T'}$ ${\displaystyle T}$ ${\displaystyle T}$ ${\displaystyle T'}$ ${\displaystyle T}$ ${\displaystyle \psi }$ ${\displaystyle T'}$ ${\displaystyle \psi ^{\ast }}$ ${\displaystyle T}$ ${\displaystyle \psi }$ ${\displaystyle T}$ ${\displaystyle \psi \leftrightarrow \psi ^{\ast }}$ ${\displaystyle T'}$

На практике расширение по определениям T не отличается от исходной теории T. Фактически, формулы можно рассматривать как сокращенные переводы в T. Манипулирование этими сокращениями как фактическими формулами тогда оправдывается тем фактом, что расширения по определениям консервативны. ${\displaystyle T'}$ ${\displaystyle T'}$

Примеры

• Традиционно, теория множеств первого порядка ZF имеет (равенство) и (членство) в качестве своих единственных примитивных символов отношений и не имеет функциональных символов. Однако в повседневной математике используются многие другие символы, такие как символ бинарного отношения , константа , символ унарной функции P ( операция мощности множества ) и т. д. Все эти символы фактически принадлежат расширениям по определениям ZF. ${\displaystyle =}$ ${\displaystyle \in }$ ${\displaystyle \subseteq }$ ${\displaystyle \emptyset }$
• Пусть будет теорией первого порядка для групп , в которой единственным примитивным символом является двоичное произведение ×. В T можно доказать, что существует единственный элемент y такой, что x × y = y × x = x для любого x . Поэтому можно добавить к T новую константу e и аксиому ${\displaystyle T}$

${\displaystyle \forall x(x\times e=x{\text{ and }}e\times x=x)}$,

и то, что мы получаем, является расширением по определениям . Тогда в мы можем доказать, что для каждого x существует единственный y такой, что x × y = y × x = e . Следовательно, теория первого порядка, полученная из добавлением символа унарной функции и аксиомы ${\displaystyle T'}$ ${\displaystyle T}$ ${\displaystyle T'}$ ${\displaystyle T''}$ ${\displaystyle T'}$ ${\displaystyle f}$

${\displaystyle \forall x(x\times f(x)=e{\text{ and }}f(x)\times x=e)}$

является расширением по определениям . Обычно обозначается . ${\displaystyle T}$ ${\displaystyle f(x)}$ ${\displaystyle x^{-1}}$

Смотрите также

• Консервативное расширение
• Расширение новыми именами констант и функций

Библиография

• SC Kleene (1952), Введение в метаматематику , Д. Ван Ностранд
• Э. Мендельсон (1997). Введение в математическую логику (4-е изд.), Chapman & Hall.
• JR Shoenfield (1967). Математическая логика , Addison-Wesley Publishing Company (переиздано в 2001 году AK Peters)