Глава 4. Исчисления языка 1-го порядка.

§1 Формулы и аксиомы.

Литература: Новиков. Матлогика.

Аксиомы:

I-V:

Во всех аксиомах логики высказываний переименуем $x_i$ в $F$:

1. $A \rightarrow (B \rightarrow A)$

   $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$

2. $A \land B \rightarrow A$

   $A \land B \rightarrow B$

   $((A \rightarrow B) \rightarrow ((A \rightarrow C) \rightarrow (A \rightarrow B \land C))$

3. $A \rightarrow A \lor B$

   $B \rightarrow A \lor B$

   $(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \lor B \rightarrow C))$

4. $(A \leftrightarrow B) \rightarrow (A \rightarrow B)$

   $(A \leftrightarrow B) \rightarrow (B \rightarrow A)$

   $(A \rightarrow B) \rightarrow ((B \rightarrow A ) \rightarrow (A \leftrightarrow B))$

5. $A \rightarrow \neg (\neg A)$

   $\neg (\neg A) \rightarrow A$

   $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$

VI:

$\forall x \space F (x)\rightarrow F(y)$ //$x$ не встречается как связанная переменная в $F$

$F (y)\rightarrow \exists x\space F(x)$ //$x$ свободная переменная в $F$

Пусть $F$ не содержит $x$ как свободный символ.

$\forall x \space (F \rightarrow G(x)) \rightarrow (F \rightarrow \forall x\space G(x))$

Правила вывода:

1. Правило подстановки:

   Вместо любой свободной переменной можно подставить терм, в котором нет переменных, связанных в формуле

2. Modus Ponens:

   $\displaystyle\frac{F \rightarrow G, F}{G}$

3. Правило обобщения:

   $\displaystyle\frac{F(x)}{\forall x F(x)}$, где $x$ - свободная переменная

$\Gamma \vdash F$

$F_1, ... , F_n = F$

$F$ выводима из $\Gamma$, если:

1. $\forall F_i \in \Gamma$
2. Получена из предыдущих по ПП
3. Получена из двух предыдущих по МП
4. Получена из предшествующих по ПО

Если $F$ - выводима, то она является формальной теоремой.

Опр. Модель теории с аксиомами $\Gamma$ - модель, в которой все формулы истинны

Теорема. Если из $\Gamma$ выводима $F$, то $F$ - логическое следствие системы $\Gamma$ (если $\Gamma \vdash F \Rightarrow \Gamma \models F$)

Опр. $F'$ - замыкание формулы $F$, если в формуле $F$ ко всем свободным переменным применено ПО

Опр. Совокупность всех истинных замкнутых формул в моделях данной аксиоматики называется теорией с данной аксиоматикой.

Пример:

$\Sigma=\{P_1^2\}$

$\Gamma=\{\neg P_1^2xy,\space P_1^2xy \land P_1^2yz \rightarrow P_1^2xz \}$

Это теория, описывающая отношение строгого неравенства (первая формула - антирефлексивность, вторая - транзитивность)

Теория групп - тоже аксиоматическая теория:

$\Sigma=\{f_1^2,\space f_1^1, \space f_1^0, \space P_1^2\}$

умножение, обратный элемент, нейтральный элемент, равенство

§2 Теорема дедукции.

Теорема:

Если $\Gamma \cup \{F\}\vdash G$, то $\Gamma \vdash F \rightarrow G$

Верно только если $F$ - замкнутая формула!

Доказательство:

$\Gamma$ $G_1 ... G_n=G$

$F \rightarrow G_i \space \space \space \space i<n$ Это уже есть

$G_{i+1}=\forall x_i G_i$

$F \rightarrow \forall x_i G_i$ Это вроде хотим доказать

$F$ - замкнутая, применим аксиому и MP, и готово.

$\forall x \space (F \rightarrow G(x)) \rightarrow (F \rightarrow \forall x\space G(x))$

§3 Теорема о полноте исчисления языка 1-го порядка.

Лемма 1. Пусть $F \lor H$ и $G \lor \neg H$ - выводимые формулы. Тогда $F \lor G$ тоже выводимы.

$(F \lor H) \rightarrow ((G \lor \neg H) \rightarrow (F \lor G))$ - истинна. Метод резолюции

Опр. Множество формул называется противоречивым, если из него выводится какая-то формула и одновременно её отрицание.

Лемма 2. Пусть $F$ - замкнутая формула. $F \cup \{\neg F\}$ противоречиво. Тогда $\Gamma \vdash F$

Доказательство:

$F \cup \{\neg F\}\vdash G$ $\Gamma \vdash \neg F \rightarrow G$

$F \cup \{\neg F\}\vdash \neg G$ $\Gamma \vdash \neg F \rightarrow \neg G$

Применим аксиому II.3 и MP и выведем из этих двух формул следующее:

$\neg F \rightarrow (G \land \neg G)\space \vdash \space \neg (G \land \neg G) \rightarrow F \space \vdash\space F$

​ $\uparrow$форм.теорема

Теорема (о полноте). $\Gamma \models F$, то $\Gamma \vdash F$ ($F$ - замкнутая)

Доказательство:

$\Gamma \cup \{\neg F\}$ - невыполнимое множество, так как $\Gamma \models F$

Возьмём какие то два противоположных литерала $L$ и $\neg L$

Применим метод резолюций, получим пустой дизъюнкт.

$\Gamma \cup \{\neg F\} \vdash L$

$\Gamma \cup \{\neg F\} \vdash \neg L$

Теорема. Теория языков первого порядка неразрешима, то есть не существует алгоритма, который по формуле мог бы определить, является ли она теоремой. (без доказательства)

§4 Теория 1-го порядка с равенством.

$\Gamma$- наши старые аксиомы. Добавим к ним дополнительное бесконечное множество формул:

• $P_1^2x_1x_1$
• $P_1^2x_1x_2 \rightarrow (F(x_1) \rightarrow F(x_2))$ //$F$ - любая формула, в которой $x_1$ свободна

Вторая запись – это схема аксиом, поэтому мы и говорим, что $\Gamma$ содержит бесконечное число аксиом

Теорема 1. Формула $P_1^2x_1x_2 \rightarrow P_1^2x_2x_1$ - формальная теорема. (коммутативность)

Доказательство: Пусть $F(x)=P_1^2xx_3$

Тогда, используя схему, получаем аксиому:

$P_1^2x_1x_2 \rightarrow (P_1^2x_1x_3 \rightarrow P_1^2x_2x_3)$

Сделаем подстановку, заменяя $x_3$ на $x_1$:

$P_1^2x_1x_2 \rightarrow (P_1^2x_1x_1 \rightarrow P_1^2x_2x_1)$

Вспомогательные теоремы:

1. $(p\rightarrow(q\rightarrow r) \rightarrow(p\land q \rightarrow r))$
2. $((p\land q \rightarrow r) \rightarrow (q\rightarrow (p \rightarrow r)) )$

Из первой теоремы и аксиомы по MP:

$(P_1^2x_1x_2 \land P_1^2x_1x_1) \rightarrow P_1^2x_2x_1$

По второй теореме:

$P_1^2x_1x_1 \rightarrow (P_1^2x_1x_2 \rightarrow P_1^2x_2x_1)$

Используем первую аксиому по MP:

$(P_1^2x_1x_2 \rightarrow P_1^2x_2x_1)$ #

Теорема 2. Формула $P_1^2x_1x_2 \rightarrow (F(x_2) \rightarrow F(x_1))$, где $F$ любая функция, в которой $x_2$ - свободная переменная, формальная теорема

Доказательство: переименовывая переменные из второй схемы аксиом, получаем:

$P_1^2x_2x_1 \rightarrow (F(x_2) \rightarrow F(x_1))$ (1)

Вспомогательная теорема:

$(p\rightarrow q) \rightarrow ((q \rightarrow r) \rightarrow(p\rightarrow r))$

$(P^1_1x_1x_2 \rightarrow P^1_1x_2x_1) \rightarrow ((P_1^1x_2x_1 \rightarrow (F(x_2) \rightarrow F(x_1))\rightarrow (P_1^1x_1x_2\rightarrow (F(x_2)\rightarrow F(x_1)))))$

/ Первая теорема \ / (1) \ => по MP получаем $\uparrow$

Теорема 3. Формула $P_1^2x_1x_2 \rightarrow (P_1^2x_2x_3 \rightarrow P_1^2x_1x_3)$ - формальная теорема.

Доказательство: В теорему 2 подставим $F(x) = P_1^2xx_3$:

$P_1^2x_1x_2 \rightarrow (P_1^2x_2x_3 \rightarrow P_1^2x_1x_3)$ . Done.

Теорема 4. Формула $P_1^2x_1x_{n+1} \rightarrow P_1^2f_n^mx_1x_2...x_nf_n^mx_{n+1}x_2...x_n$- формальная теорема.

Из схемы второй аксиомы получаем новую аксиому:

$F(x) = P_1^2f_n^mx_{n+2}x_2...x_nf_n^mxx_2...x_n$

$P_1^2x_1x_{n+1} \rightarrow (P_1^2f_n^mx_{n+2}x_2...x_nf_n^mx_1x_2...x_n \rightarrow P_1^2f_n^mx_{n+2}x_2...x_nf_n^mx_{n+1}x_2...x_n)$

Заменим $x_{n+2}$ на $x_1$ (уже формальная теорема):

$P_1^2x_1x_{n+1} \rightarrow (P_1^2f_n^mx_1x_2...x_nf_n^mx_1x_2...x_n \rightarrow P_1^2f_n^mx_1x_2...x_nf_n^mx_{n+1}x_2...x_n)$

Применяем вспомогательные теоремы из теоремы *1, сначала первую:

$(P_1^2x_1x_{n+1} \land P_1^2f_n^mx_1x_2...x_nf_n^mx_1x_2...x_n) \rightarrow P_1^2f_n^mx_1x_2...x_nf_n^mx_{n+1}x_2...x_n$

Затем вторую:

$P_1^2f_n^mx_1x_2...x_nf_n^mx_1x_2...x_n \rightarrow (P_1^2x_1x_{n+1} \rightarrow P_1^2f_n^mx_1x_2...x_nf_n^mx_{n+1}x_2...x_n)$

/ это первая аксиома \ => по MP выполняется $\uparrow$ #

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

$P_1^2x_1x_{n+1} \rightarrow (P_1^2f_m^nx_1x_2...x_nf_m^nx_{n+2}x_2...x_n \rightarrow P_1^2f_m^nx_{n+1}x_2...x_nf_m^nx_{n+2}x_2...x_n)$

можно поменять посылки местами

$P_1^2f_m^nx_1x_2...x_nf_m^nx_{n+2}x_2...x_n \rightarrow (P_1^2x_1x_{n+1}\rightarrow P_1^2f_m^nx_{n+1}x_2...x_nf_m^nx_{n+2}x_2...x_n)$

​ меняем местами аргументы по т.1

А. Чёрч назвал эту теорию Ё-теория, но болеее принято называть её Е-теория (Equal)

Опр. Модель, в которой $P_1^2$ интерпретируется как совпадение объектов, называется нормальной.

А мы будем интерпретировать его как равенство (алфавитный символ)! $x_1=x_2$

Вторая схема аксиом теперь превращается вот в это:

$x_1=x_2 \rightarrow (F(x_1) \rightarrow F(x_2))$

А потом легко обобщается до этого:

$x_1=x_{n+1} \land x_2=x_{n+2} \land...\land x_n=x_{n+n} \rightarrow (F(x_1..x_n) \rightarrow F(x_{n+1}...x_{2n}))$

Теорема 5. Если существует модель для некоторой Ё-теории, то существует и нормальная модель этой теории.

Доказательство, кажется, следует из определение нормальной модели.

§5 Формальная теория натуральных чисел.

Нам нужен нуль-арный символ $f_1^0$ и унарный $f_1^1$

(Аксиомы Пеано?):

• $\neg f_1^0 = f_1^1x_1$

• $x_1=x_2 \rightarrow f_1^1x_1=f_1^1x_2$

  эта аксиома не нужна, так как по теории равенства мы это уже доказали.

• $f_1^1x_1 = f_1^1x_1 \rightarrow x_1=x_2$

Принцип индукции?

• $(F(f_1^0) \land \forall xF(x) \rightarrow F(f_1^1x)) \rightarrow F(y)$

  Или, что то же самое в дальнейшем: $(F(0) \land \forall xF(x) \rightarrow F(x')) \rightarrow F(y)$

  ​ БИ ПИ\ШИ чтд

Опр. Теория называется полной, если все модели этой теории изоморфны.

M={0, }

//тут я что-то упустила

Теорема:

//

Лемма. $A$ - модель, $f_1^0$ - интерпретирован как некоторый элемент $a$. Тогда для $b \neq a$ существует $b=c'$

Доказательство:

$M$ - носитель модели

$N =\{a, a', (a')', ((a')')', ...\}$ - подмножество $M$ //натуральный ряд, штрих - это $f_1^1$

Аксиоматика натурального ряда:

$f_1^0, f_1^1, =$

$\neg f_1^0 = f_1^1x$

$f_1^1x = f_1^1y \rightarrow x=y$

Индукция:

$(F(f_1^0) \land \forall xF(x) \rightarrow F(f_1^1x)) \rightarrow F(y)$

Если докажем, что подмножество N совпадает с M - будет супер. У всех элементов, кроме $a$ есть предшествующие. Будем действовать от противного.

$P(x)$:

$P_1^1x_i = ИСТИНА$, если $x_i$ интепретируется как элемент из $N$

$P_1^1x_i = ЛОЖЬ$, если $x_i$ интерпретируется как элемент $M \setminus N$

Смотрим на аксиому индукции: посылка всегда истинна (берём P вместо F). Получается истина для любого элемента => $M \setminus N=\varnothing$

§6 Формальная арифметика.

Теория рекурсивных функций: Мальцев "Алгоритмы и рекурсивные функции"; Новиков

Нам нужны два функциональных символа, которые будем использовать как сложение и умножение: $f_1^2, f_2^2$

Теорема (Коммутативность с нулём):

$\vdash 0 + x = x + 0$

Доказательство:

$F(x) := 0+x = x+0$ (1)

$F(0): 0+0 = 0+0$ //верно по аксиоме равенства

$F(x) \rightarrow F(x')$?

$x+0=x$ - аксиома

$x + 0 = x \rightarrow (x+0)' = x'$ //из аксиомы теории равенства !!!

[M.P]: $(x+0)' = x'$

$0+x' = (0+x)'$ _~

$F(x) \rightarrow (0+x)' = (x+0)'$ //верно из (1) и аксиомы теории равенства _~

$x'+0 = x'$ //по аксиоме правого нуля

$x' + 0 = x' \rightarrow x' = x'+0$ //из теоремы о симметричности равенства

$x' = x' + 0$ !!!

$(x+0)' = x' \rightarrow (x'=x'+0 \rightarrow (x+0)' = x'+0)$ //теорема о транзитивности равенства

Применяем M.P. используя !!!:

$(x+0)' = x'+0$

Что-то сделали

$0+x' = (0+x)' \rightarrow ((0+x)' = (x+0)' \rightarrow 0+x' = (x+0)')$

$F(x) \vdash 0+x = (x+0)'$

Потом используем _~: (возможно)

$0+x' = (0+x)' \rightarrow ((x+0)' = x' + 0 \rightarrow 0 + x' = x' + 0)$

$F(x) \vdash 0+x = (x+0)' \vdash 0+x' = x'+0$

​ | это F(x') |

$F(x) \rightarrow F(x')$ //по теореме дедукции, что и требовалось

$F(0) \land \forall x F(x) \rightarrow F(x') \rightarrow F(y)$ //зачем-то индукция

Подобные теоремы будут на экзамене

§7 Языки 2-го порядка.

В первом порядке есть проблема с несчётными множествами.

Доказательства теоремы Гёделя о неполноте не будет! Можно почитать у Успенского :)

Название этого параграфа тут просто так, потому что Гейн только философски размышлял на тему