- •Введение
- •Глава 1. Пропозициональная логика §1. Пропозициональная теория
- •1. Высказывания, простые и составные
- •2. Алфавит
- •3. Формальный язык
- •4. Пропозициональная теория
- •5. Общая картина
- •§2. Исчисление высказываний
- •Предварительное обсуждение
- •2. Аксиоматика
- •3. Правило вывода
- •4. Доказательство. Теорема
- •5. Вывод. Выводимость
- •6. Транзитивность выводимости
- •7. Теорема о дедукции для исчисления высказываний
- •8. Общая картина
- •§3. Полнота исчисления высказываний
- •1. Мотивировка
- •Первое доказательство
- •3. Второе доказательство
- •Общая картина
- •§4. Исчисление секвенций
- •1. Мотивировка
- •Аксиомы и правила вывода исчисления секвенций
- •§5. Интуиционистская пропозициональная логика
- •Обсуждение
- •Модели Крипке
- •Полнота интуиционистского исчисления высказываний относительно шкал Крипке
- •Общая картина
- •Глава 2. Предикаты и выразимость §6. Формулы языка логики предикатов. Интерпретации
- •Обсуждение
- •Алфавит языка логики предикатов
- •Формулы логики предикатов
- •Интерпретации
- •Определение истинности
- •§7. Выразимость предикатов
- •1. Выразимые предикаты
- •2. Невыразимые предикаты: автоморфизм
- •3. Невыразимые предикаты: элиминация кванторов
Полнота интуиционистского исчисления высказываний относительно шкал Крипке
Хорошо. С формулой справились . Но с любой ли формулой можно справиться подобным образом? Существует ли формула, невыводимая в интуиционистском исчислении высказываний, истинная во всех мирах всех шкал, невыводимость которой, соответственно, надо доказывать как-то по-другому? Или шкалы Крипке являются окончательным ответом?
Теорема 5.4. (Полнота интуиционистского исчисления высказываний относительно шкал Крипке)
Для любой формулы, невыводимой в интуиционистском исчислении высказываний, существует шкала Крипке, в некотором мире которой эта формула ложна.
Доказательство следует начать с определения предполагаемого стандартного вида миров.
Определение 5.2. (1) Пусть Р и Q – два конечных множества пропозициональных формул. Пару назовём совместной, если существуют шкала Крипке и мир в ней, в котором все формулы из Р истинны, а все формулы из Q ложны.
(2) Пару назовём противоречивой, если в интуиционистском исчислении высказываний выводима формула .
Замечания. (1) Понятно, что противоречивая пара совместной быть не может. Оказывается, что верно и обратное, причём это «обратное» есть переформулировка обсуждаемой теоремы.
(2) Немного похоже на секвенции, нет?
(3) Эти пары (при одном дополнительном предположении) и будут играть роль миров в конструируемых шкалах.
Аналогом начала доказательства леммы 3.4. для данного случая является следующее утверждение.
Лемма 5.5. Пусть пара не является противоречивой, r – произвольная формула. Тогда хотя бы одна из пар или также не является противоречивой.
Доказательство. Введём обозначение (с небольшой коллизией) , . Если обе пары противоречивы, то в интуиционистском исчислении высказываний выводимы обе импликации: и . Достаточно показать, что в этом случае выводима и импликация . Для этого достаточно (по лемме о дедукции) . Поскольку, по той же лемме о дедукции, выводимость у нас уже есть, остаётся доказать, что . Для доказательства этого, в свою очередь, достаточно установить, что и . Первое очевидно, второе – равносильно выводимости .
QED
Замечание. Принята такая терминология: лемма 5.5. показывает, что в интуиционистской логике допустимо правило сечения, позволяющее «иссечь» формулу r из импликаций и , после чего от них остаётся только .
Теперь зафиксируем некоторое конечное множество формул F, содержащее вместе с любой формулой и все её подформулы (научно говоря – замкнутое относительно перехода к подформулам).
Определение 5.3. Пусть . Пару будем называть полной, если она не является противоречивой и .
Следующее утверждение – точный аналог леммы 3.4. очевидно следует из леммы 5.5.
Лемма 5.6. Для любой непротиворечивой пары существует полная непротиворечивая пара , такая, что и (её естественно называть расширением исходной пары).
Мирами шкалы Крипке, которую мы будем строить, являются полные непротиворечивые пары . При этом тогда и только тогда, когда . Интуитивный смысл этого понятен: предполагается, что в мире формулы множества X истинны, а формулы множества Y ложны. Это нетривиально и это придётся доказывать, но, во всяком случае, позволяет определить, какие переменные в каких мирах истинны: переменная s истинна в тех и только тех мирах, в которых формула s входит в множество X.
Лемма 5.7. В построенной шкале в мире истинны все формулы из X и ложны все формулы из Y.
Доказательство проводится индукцией по формулам. База уже есть, осталось только провести восемь вариантов индукционного перехода (четыре связки помноженные на две множества из пары).
Случай . Пусть формула входит в X. Тогда формулы s и t не могут входить в Y (иначе пара противоречива), поэтому они тоже входят в X (так как пара полна), и, по индукционному предположению, в мире они обе истинны. Поэтому в этом мире истинна и формула .
Случай . Пусть формула входит в Y. Тогда по крайней мере одна из формул s или t не должна входить в X (непротиворечивость), то есть одна из них должна входить в Y (полнота). Пусть, не умаляя общности, . Тогда она ложна в этом мире и вместе с ней ложна формула .
Связка рассматривается аналогично (упражнение).
Случай . Пусть формула входит в X. Проверим, что она истинна в этом мире. Это означает, что в любом мире , таком, что , из истинности s следует истинность t. Итак, пусть s истинна в некотором таком мире. По индукционному предположению . С другой стороны, . Если бы в этом случае оказалось, что , то пара оказалась бы противоречивой, а это не так. Поэтому и по индукционному предположению она истинна в мире .
Случай .Пусть формула входит в Y. Требуется доказать, что она ложна в мире . Это означает, что найдётся мир , где , такой, что в нём s истинна, а t ложна, то есть и . Соответственно, надо такой мир построить.
Рассмотрим пару . Она непротиворечива: в противном случае выводима формула , поэтому, по лемме о дедукции выводима и формула , но тогда пара противоречива.
Непротиворечивую пару можно расширить до полной, которая и будет искомым миром.
Отрицание есть просто импликация , поэтому оно рассматривается аналогично (упражнение).
QED
Завершим доказательство теоремы. Пусть формула р невыводима в интуиционистском исчислении высказываний. Тогда пара непротиворечива. Возьмём в качестве F множество всех подформул формулы р. Построим соответствующую шкалу Крипке. Полное расширение рассмотренной пары и есть тот мир, в котором будет ложна формула р.
QED
Замечание. Множество F известно, поэтому верхняя граница размера шкалы Крипке известна. Поэтому все шкалы можно перебрать, поэтому интуиционистская пропозициональная теория разрешима.