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

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

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

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

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

,

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

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

$\psi \leftrightarrow \psi ^{\ast }$ доказуемо в $T'$ , и
$T'$ представляет собой консервативное продолжение $T$ .

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

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

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

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

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

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

,

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

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

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

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

$\psi \leftrightarrow \psi ^{\ast }$ доказуемо в $T'$ , и
$T'$ представляет собой консервативное продолжение $T$ .

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

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

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

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

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

Примеры

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

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

,

и мы получаем расширение по определениям

T'

из

T

. Затем в

T'

мы можем доказать, что для каждого x существует единственный y такой, что x × y = y × x = e . Следовательно, теория первого порядка

T''

получено от

T'

добавив унарный функциональный символ

f

и аксиома

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

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

T

. Обычно,

f(x)

обозначается

x^{-1}

.

См. также

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

С. К. Клини (1952), Введение в метаматематику , Д. Ван Ностранд
Э. Мендельсон (1997). Введение в математическую логику (4-е изд.), Чепмен и Холл.
Дж. Р. Шенфилд (1967). Математическая логика , издательство Addison-Wesley Publishing Company (переиздано в 2001 г. А. К. Питерсом)