1. Система аксиом
1.1. Первая группа
1.1.1. 1: x → (y → x)
1.1.2. 2: (x → (y → z)) → ((x → y) → (x → z))
1.2. Вторая группа
1.2.1. 1: x & y → x
1.2.2. 2: x & y → y
1.2.3. 3: (z → x) → ((z → y) → (z → x & y))
1.3. Третья группа
1.3.1. 1: x → x | y
1.3.2. 2: y → x | y
1.3.3. 3: (x → z) → ((y → z) → (x | y → z))
1.4. Четвертая группа
1.4.1. 1: (x → y) → (!y → !x)
1.4.2. 2: x → !!x
1.4.3. 3: !!x → x
2. Правила
2.1. Правило вывода
2.1.1. Если A → B и A - истина, следовательно B тоже истина
2.2. Правило подстановки
2.2.1. Если формула A доказуема в исчислении высказываний, x – переменная, B – произвольная формула исчисления высказываний, то формула, полученная в результате замены в формуле A переменной x всюду, где она входит, формулой B, является также доказуемой формулой
2.3. Правило заключения
2.3.1. Если Α и Α ⊃ B тавтологии, то B тавтология
2.4. Производные правила вывода
2.4.1. Правило одновременной подстановки
2.4.1.1. Пусть ⊨A – доказуемая формула, x1 … xn – переменные; B1 … Bn – любые формулы исчисления высказываний. Тогда результат одновременной подстановки в A вместо переменных x1 … xn соответственно формул B1 … Bn является доказуемой формулой
2.4.2. Правило сложного заключения
2.4.2.1. Пусть дана формула A1→(A2→(…(An→L))…)(*). Тогда, если формулы A1… An и (*) являются доказуемыми, то доказуема будет и формула L
2.4.3. Правило силлогизма
2.4.3.1. Если формулы A→B и B→C доказуемы, то доказуема будет и формула A→C
2.4.4. Правило контрапозиции
2.4.4.1. Если доказуема формула A→B, то будет доказуема и формула B̅→A̅
2.4.5. Правило снятия двойного отрицания
2.4.5.1. а) Если формула A→𝐵̿ является доказуемой, то формула A→B будет доказуемой
2.4.5.2. б) Если формула 𝐴̿→B является доказуемой, то формула A→B будет доказуемой
3. Доказуемость формулы
3.1. Всякая аксиома – это доказуемая формула (доказуемая = тождественно истинная)
3.2. Формула, полученная из доказуемой формулы путем применения подстановки вместо переменной x произвольной формулы B есть доказуемая формула
3.3. Формула B, полученная из доказуемых формул A и A→B путем применения правила заключения есть доказуемая формула
4. Формальные системы
4.1. Понятие
4.1.1. Формальная система (ФС) представляет собой совокупность чисто абстрактных объектов, не связанных с внешним миром, в которой представлены правила оперирования множественных символов только в синтаксической трактовке без учета смыслового содержания.
4.2. Способ задания
4.2.1. задается конечное множество символов, которое образует алфавит ФС
4.2.2. устанавливаются процедуры построения формул ФС
4.2.3. устанавливается множество аксиом
4.2.4. устанавливается конечное множество правил вывода, которые позволяют получать новые формулы из некоторого множества известных формул
4.3. Примеры
4.3.1. Исчесление высказываний
4.3.2. Лямбда-исчесление
4.3.3. Логика первого порядка
4.3.4. Логика высшего порядка
5. Алфавит
5.1. Символы первой категории: x, y, z,…,x1, x2,…, которые называются переменными высказывания
5.2. Символы второй категории, которые называются логическими связками: дизъюнкция, конъюнкция, импликация, отрицание
5.3. Символы третьей категории: скобки
6. Формула
6.1. Всякая переменная x, y, z,… является формулой
6.2. Если A и B – формулы, то слова (A | B), (A & B), (A → B), !A – формулы
6.3. Никакая другая строчка символов не является формулой
6.4. Подформула
6.4.1. Подформулой элементарной формулы является только она сама
6.4.2. Если формула имеет вид !A, то ее подформулами являются: она сама, формула A и все подформулы формулы A
6.4.3. Если формула имеет вид (A * B) (под символом * понимается любая из трех связок ), то ее подформулами являются: она сама, формулы A и B, все подформулы формул A и B
7. Выводимость
7.1. Свойства
7.1.1. 1) Всякий начальный отрезок вывода из совокупности H есть вывод из H
7.1.2. 2) Если между двумя соседними членами вывода из H вставить некоторый вывод из H, то полученная новая последовательность формул будет выводом из H
7.1.3. 3) Всякий член вывода из совокупности H, является формулой, выводимой из H
7.1.4. 4) Если H ⊂ W, то всякий вывод из H является из W
7.1.5. 5) Для того, чтобы формула B была выводима из совокупности H, необходимо и достаточно, чтобы существовал вывод этой формулы из H
7.2. Правила
7.2.1. 1) Если формула A выводима из совокупности H, то формула A выводима из совокупности H,W
7.2.2. 2) Если формула A выводима из совокупности H,C, а формула C выводима из совокупности H, то формула A выводима из совокупности H
7.2.3. 3) Если формула A выводима из совокупности H,C, а формула C выводима из совокупности W, то формула A выводима из совокупности H,W
7.2.4. 4) Если формула C→A выводима из совокупности H, то формула A выводима из совокупности H,C
7.2.5. 5) Теорема дедукции. Если формула A выводима из совокупности H,C, то формула C→A выводима из совокупности H
7.2.6. 6) Правило введения конъюнкции. Если формулы A и B выводимы из совокупности H, то формула A & B выводима из совокупности H
7.2.7. 7) Правило введения дизъюнкции. Если формула C выводима из совокупностей H,A и H,B, то формула C выводима из совокупности H, A | B