#import "cfg.typ": cfg
#show: cfg

= Логика высказываний
Пропозициональные формулы:
- Всякая пропозициональная переменная (у Клини она называется атомом, элементарной формулой)
  есть формула.
- Если $A$ - пропозициональная формула, то $not A$ - пропозициональная формула.
- Если $A$ и $B$ - пропозициональные формулы, то $(A and B), (A or B), (A => B)$ -
  пропозициональные формулы.

Пропозициональная формула задаёт булеву функцию от $n$ переменных.

Тавтология $:=$ пропозициональные формула, истиннае независимо от переменных.

$models A := A$ - тавтология.

$A_1, ..., A_n models B :=$ в строках, где одновременно $A_1, ..., A_n$ истинны,
$B$ тоже истинна.

Множество формул совместно $:= exists$ набор значений переменных, при которых все формулы
множества истинны.

Формула выполнима $:= exists$ набор значений переменных, при которых она истинна.

$A models B <-> med models A => B$

Две формулы эквивалентны $:=$ они задают одну и ту же булеву функцию.

$A <=> B := (A => B) and (B => A)$

Формулы $A$ и $B$ эквивалентны $<->$ $models A <=> B$.

Пропозициональные формулы однозначны для разбора.

Теорема о полноте системы связок: булева функция задаётся пропозициональной формулой.

Литерал $:=$ переменная или отрицание переменной. Конъюнкт $:=$ произвольная конъюнкция
литералов. Дизъюнктивная нормальная форма $:=$ дизъюнкция конъюнктов. Другая форма - это
конъюнктивная нормальная форма.

Булева функция задаётся дизъюнктивной нормальной формой. То же самое про конъюнктивную
нормальную форму.

Система связок $and, not$ является полной. $and, or, =>$ неполна.

Булева функция однозначно представляется полиномом над $ZZ_2$ с многими переменными -
полиномом Жегалкина.

<NAME>: Набор булевых функций является полным $<=>$ он не содержится целиком
ни в одном из пяти следующих "предполных классов":
- монотонные функции
- функции, сохраняющие нуль ($f(0, ..., 0) = 0$)
- функции, сохраняющие единицу
- линейные функции
- самодвойственные функции ($f(1 - p_1, ..., 1 - p_n) = 1 - f(p_1, ..., p_n)$)

Теория моделей: заменяя атомы истинностными значениями во всевозможных сочетаниях,
мы получаем, так сказать, "модели", конкретные "реализации", воплощения того, что могут
выражать высказывания.

Теория доказательств: аксиомы и правила.

Аксиомы (cхемы аксиом) ичисления высказываний (вообще скобки были, согласно индуктивному
определению, но я их опустил):
+ $A => B => A$
+ $(A => B => C) => (A => B) => A => C$
+ $A and B => A$
+ $A and B => B$
+ $A => B => A and B$
+ $A => A or B$
+ $B => A or B$
+ $(A => C) => (B => C) => A or B => C$
+ $not A => A => B$
+ $(A => B) => (A => not B) => not A$
+ $A or not A$
Тут переменные - это "шаблонные" переменные, в которые подставляются пропозициональные
формулы. В Шень различают эти переменные и пропозициональные переменные. То же в Клини.

В ИВ входит ещё modus ponens: $(A, A => B)/B$.

Вывод в ИВ $:=$ конечная последовательность формул, каждая из которых есть аксиома или
получается из предыдущих по правилу MP.

Пропозициональная формула выводима в ИВ или теоремой ИВ $:= exists$ вывод, в котором
эта формула встречается.

Вывод из $Gamma :=$ конечная последовательность формул, каждая из которых
является аксиомой, принаждлежит $Gamma$ или получается из предыдущих по правилу MP.
Другими словами, мы как бы добавляем формулы из $Gamma$ к аксиомам ИВ - именно как
формулы, а не как схемы аксиом. $Gamma = emptyset =>$ формула выводима в ИВ. $A tack.r
Gamma$. Вместо $emptyset tack.r A$ пишут $tack.r A$. $Gamma union {A}$ обозначается
$Gamma, A$

Теорема о дедукции: $Gamma tack.r A => B <-> Gamma, A tack.r B$

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

10 аксиома интуиционистская, но при наличии 11 выводится.

$Gamma$ противоречиво $:= Gamma tack.r A, not A$

$Gamma$ полное $:= cases(delim: "[", Gamma tack.r A, Gamma tack.r not A)$

Теорема о корректности ИВ: $Gamma tack.r A -> Gamma tack.double.r A$

Вторая форма: совместное множество формул непротиворечиво.

Теорема о полноте ИВ: $Gamma tack.double.r A -> Gamma tack.r A$

Вторая форма: непротиворечивое множество формул совместно.

Теорема о компактности ИВ: $forall$ конечное подмножество $Gamma$ совместно $-> Gamma$
совместно.

Это было ичисление гильбертовского типа.
