To Do: нет доказательства законов, доказательства ПНФ и СНФ.

Глава 2. Логика первого порядка

§1 Понятие логики первого порядка

Основные определения

Опр. Алфавит состоит из:

• Предметных символов: $x_1, x_2, .., x_n, ...$
• Функциональных символов: $f_1^0, f_2^0, ..., f_n^0, f_1^1, f_2^1, ..., f_n^2, ..., f_n^m$ (вверху пишут арность, снизу просто индекс)
• Предикатных символов: $P_1^0, P_2^0, ..., P_n^0, P_1^1, P_2^1, ..., P_n^2, ..., P_k^l$
• Связок и кванторов: $\and, \or, \neg, \rightarrow, \leftrightarrow,(,),\forall, \exists$

Опр. Термами называются:

1. Любой предметный символ;
2. Выражения вида $f_n^m t_1t_2\dots t_m$, где $t_1,\ t_2,\ \dots,\ t_m$ - термы;
3. Других термов нет.

Опр. Формулами логики первого порядка называются:

1. Выражения $P_n^m t_1t_2\dots t_m$, где $P_n^m$ - предикатный символ, $t_1,\ t_2,\ \dots,\ t_m$ - термы.
2. Если $F$ и $G$ формулы, то $(\neg F), (F \or G), (F \and G), (F \rightarrow G), (F \leftrightarrow G)$ тоже формулы.
3. Если $F$ - формула, то $(\forall x_i) (F), (\exists x_i) (F)$ тоже формулы
4. Других формул нет.

Пропущенный фрагмент: Здесь что-то про алгебраическую систему, где предметные переменные - носитель, функциональные символы - операции, предикаты - отношения

Опр. Если переменная стоит непосредственно за квантором или входит в область действия квантора по этой переменной., то она называется связной, иначе - свободной.

Опр. Переменная называется свободной в формуле, если существует хотя бы одно свободное вхождение переменной в формулу.

Интерпретация формул

Опр. Модель - это какое-то множество $M$ и набор определенных на $M$ предикатов и функций.

При интерпретации мы ставим в соответствие:

• константам - константы из $M$.
• Предикатам - $P_m^n \in M^n$
• Функциональным символам - $F_M^n \in M^n$

В итоге, получаем $n$-местный предикат, где $n$ - количество свободных переменных в исходной формуле.

Опр. Формула $F$:

• называется истинной, если $\exists$ модель, в которой соовет. ей функция $F \equiv 1$
• называется общезначимой, если для любой модели соовет. ей функция $F \equiv 1$.
• называется выполнимой, если $\exists$ модель и $\exists x_1, x_2 , .. , x_n: F(x_1, x_2, ... x_n) = 1$
• называется противоречием в данной модели, если если соответствующая ей функция $F \equiv 0$
• называется логическим противоречием, если она - противоречие в любой модели

Опр. Формулы $F$ и $G$ равносильны ($F \equiv G$) в данной модели , если $FInt(F) \equiv FInt(G)$

Теорема. Критерий равносильности. $F \equiv G \Leftrightarrow$ $F \leftrightarrow G$ общезначима в данной модели.

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

$F \equiv G \Leftrightarrow Fint(F) = Fint(G) \Leftrightarrow Fint(F \leftrightarrow G) = 1$

§2 Законы логики

Мы живем в системе, в которой выполняются законы высказываний (идемпотентность, коммутативность, ассоциативность и отрицание). Давайте к этим законам добавим еще несколько новых.

Теорема. Пусть $F$ и $G$ - некоторые формулы.

1. Следующие формулы равносильны:

   $\forall x_i (F \land G) \equiv \forall x_i F \land \forall x_i G$

   $\exists x_i (F \or G) \equiv \exists x_i F \lor \exists x_i G$

   $\forall x_i \forall x_j F \equiv \forall x_j \forall x_i F$

   $\exists x_i \exists x_j F \equiv \exists x_j \exists x_i F$

   $\neg \forall x_i F \equiv \exists x_i(\neg F)$

   $\neg \exists x_i F \equiv \forall x_i (\neg F)$

2. Пусть $G$ не содержит $x_i$ как свободную переменную. Тогда равносильны:

   $\forall x_i (F \lor G) \equiv \forall x_i F \lor G$

   $\exists x_i(F \land G) \equiv \exists x_i F \land G$

   $\forall x_i G \equiv G$

   $\exists x_i G \equiv G$

3. Пусть $F$ не содержит своей записи переменную $x_j$. Тогда равносильны:

   $\forall x_i F \equiv \forall x_j S_{x_i}^{x_j} F$

   $\exists x_i F \equiv \exists x_j S_{x_i}^{x_j} F$

Доказательство. Нужно доказать все. Якобы доказываются в 1-2 строки подстановкой конкретных значений (интерпретаций)

Warning! Achtung! Внимание опасность! Такие формулы не верны:

• $\forall x_i (F \lor G) \neq \forall x_i (F) \lor \forall x_i (G)$
• $\exists x_i (F \land G) \neq \exists x_i (F) \land \exists x_i (G)$

Следствие. Пусть $G$ не содержит $x_i$ как свободную переменную, тогда

1. $\forall x_i (F \rightarrow G) \equiv \forall x_i F \rightarrow G$
2. $\exists x_i(F \rightarrow G) \equiv \exists x_i F \rightarrow G$
3. $\forall x_i (G \rightarrow F) \equiv G \rightarrow \forall x_i F$
4. $\exists x_i (G \rightarrow F) \equiv G \rightarrow \exists x_i F$

Доказательство. $F \rightarrow G \equiv (\neg F) \lor G$

$\forall x_i (F \rightarrow G) \equiv \forall x_i \neg F \lor G \equiv \neg(\exists x_i F) \lor G \equiv \exists$ не успел

2. $G \rightarrow F = (\neg G) \lor F$

   $\forall x_i(G \rightarrow )$

Ну а 4-е аналогично

Логическое следствие

Совершенно аналогичное определение и теорема.

Опр. Говорят, что формула $G$ является логическим следствием $F_1, F_2, .... F_n$, если при любой интерпретации, когда значения этих формул равно $1$, $G$ тоже равно $1$. Это обозначают так: $\{F_1, F_2, ..., F_n\} \models G$.

Теорема 2.

1. Формула $G$ - логическоре следствие $F_1, F_2, ... , F_n \Leftrightarrow F_1 \land F_2 \land ... \land F_n \rightarrow G$ - тавтология
2. Формула $G$ - логическое противоречием $\Leftrightarrow F_1 \land F_2 \land.... \land F_n \land \neg G$ - противоречие
   

§3 Нормальные формы

Предваренная нормальная форма

Опр. Говорят, что формула $q_1x_{i_1}q_2x_{i_2} ...q_nx_{i_n}F$ имеет предваренную нормальную форму, если $q_i \in \{\forall, \exists\}$, а формула $F$ не содержит кванторов.

Это определение станет чуть-чуть понятнее, если его сформулировать так:

Опр. Формула $G$ имеет ПНФ, если $G = (Q_1 x_1)…(Q_n x_n )F$, где $Q_1, …, Q_n$ - кванторы , а формула $F$ не содержит кванторов.

Например , формула $(\forall x)(\exists y)(P(x,y) \land \neg Q(y))$ имеет ПНФ, а формула $\neg (\forall x) (T(x) \land S(x, y))$ не имеет

Теорема 1. Для всякой формулы $F$ языка логики 1 порядка существует равносильная формула $G$ , имеющая ПНФ.

Доказательство будем вести индукцией по числу связок в данной формуле.

Пусть есть какая-то формула $F, m$ - число связок в ней.

• Б.И. $m = 0$, значит формула уже в ПНФ.

• Ш.И. связок $< m$, то все доказано.

  Пусть связок теперь ровно $m$. Где может стоять последняя связка?

  Ну, например, рассмотрим связку $\neg$. Она может стоять в начале, между кванторами или в конце. Пока она стоит где-то в серединке, тогда на левую часть можно внимания не обращать.

  $\neg q_1 x_{i_1} ... q_n x_n F \equiv \neg q_1 x_{i_1}.... q_n x_n q_{n+1}x_{n+1}...q_s x_{i_s} G \equiv .....$ там с чертой

Алгоритм приведения к ПНФ

1. Исключить $\leftrightarrow$ и $\rightarrow$.
2. Занести отрицание к атомарным формулам.
3. Вынести кванторы вперед, используя при необходимости переименование связанных переменных.

Сколемова нормальная форма

Скольм (Скульм) - норвежский математик, в учебниках обычно говорят "скольмовская" .

Опр. Скольмовой нормальной формой называется формула, имеющая вид: $\forall x_{i_1}, \forall x_{i_1}, \forall x_{i_1} ..., \forall x_{i_n} H$, где $H$ - безкванторна и записана в КНФ.

Теорема 2. Для любой формулы языка первого порядка существует формула в СНФ, которая выполнима тогда и только тогда, когда выполнима исходная формула.

Для начала рассмотрим пример.

Пусть есть какая-то формула, например $\exists x_1 \forall x_2 \forall x_3 \exists x_4 \forall x_5 \exists x_6 f(x_1, x_2, x_3, x_4, X-5, x_6)$. Мы хотим их ликвидировать элиминация кванторов . Давайте в нашем алфавите выберем такой символ нулярный, который в формуле $F$ не встречается и вместо $x_1$ подставим этот нулярный символ.

$F(f_i^0, x_2, x_3, f_j^2x_2x_3)$

Доказательство. Есть какая-то формула $q_1x_{i_1}q_2x_{i_2} ...q_nx_{i_n}F$ - предваренная нормальная форма