Верещагин Н.К., Шень А. - Языки и исчисления (1076783), страница 15
Текст из файла (страница 15)
Для любой невыводимой в интуиционистском исчислении формулы ϕ можно подобрать шкалу Крипке,в которой ϕ ложна в некотором мире. Напомним схему доказательства полноты классического исчисления высказываний, приведённого в разделе 2.2. Пусть формула ϕневыводима. Мы хотим найти значения переменных, при которыхформула ϕ ложна, то есть формула ¬ϕ истинна. Само по себе требование истинности ¬ϕ не определяет значения переменных однозначно. Чтобы избавиться от произвола, мы расширяем непротиворечи-[п. 4]Интуиционистская пропозициональная логика67вое множество {¬ϕ} до полного множества Γ и объявляем истинными те переменные, которые входят в Γ.Для интуиционистского случая в этой схеме требуются некоторыеизменения.
Раньше ложность формулы ϕ была равносильна истинности формулы ¬ϕ. В шкалах Крипке это уже не так, и мы будемотдельно говорить об истинных и ложных (не истинных) формулах.Пусть A и B — конечные множества пропозициональных формул. Будем говорить, что пара (A, B) совместна, если существуетшкала Крипке и её мир, в котором все формулы из A истинны, а всеформулы из B ложны.
Будем говорить, что пара (A, B) противоречива, если в интуиционистском исчислении высказываний выводимаформула(A1 ∧ A2 ∧ . . . ∧ An ) → (B1 ∨ B2 ∨ . . . ∨ Bm ),где A1 , . . . , An — формулы множества A, а B1 , . . . , Bm — формулымножества B. (Без ограничения общности можно считать, что перечислены все формулы множеств A и B, поскольку пропущенныеформулы можно добавить, не нарушив выводимость.)Пример: если одна и та же формула входит в обе части пары, тотакая пара противоречива.Легко проверить, что противоречивая пара не может быть совместна.
В самом деле, если в некотором мире все формулы из A истинны, а все формулы из B ложны, то посылка импликации в этоммире истинна, а заключение ложно. Поэтому импликация ложна,что противоречит её выводимости (теорема о корректности).Мы докажем, что верно и обратное: всякая непротиворечивая пара совместна. В частности, когда B состоит из единственной формулы, получается утверждение теоремы о полноте. (Мы предполагаем,как это обычно делается, что конъюнкция пустого множества формул есть тождественно истинная формула, а дизъюнкция — тождественно ложная. Поэтому противоречивость пары (∅, {ϕ}) означаетвыводимость формулы ϕ.
Заметим кстати, что противоречивость пары ({ϕ}, ∅) означает выводимость формулы ¬ϕ.)Итак, пусть имеется непротиворечивая пара (A, B). Как доказатьеё совместность? Как и в классическом случае, мы устраним произвол, расширив A и B. Основным средством здесь является такаялемма.Лемма 1. Пусть (A, B) — непротиворечивая пара, а τ — произвольная формула.
Тогда хотя бы одна из пар (A∪{τ }, B) и (A, B∪{τ })непротиворечива.68Исчисление высказываний[гл. 2]Доказательство леммы 1. Пусть обе пары с добавленным τ противоречивы. Надо доказать, что противоречива исходная пара. Другими словами, надо показать, что если в интуиционистском исчислениивысказываний выводимы формулы(A ∧ τ ) → B,A → (B ∨ τ ),то выводима и формула A → B (для простоты мы отождествляеммножества A и B с конъюнкцией и дизъюнкцией их элементов исчитаем A и B формулами).В самом деле, по лемме о дедукции достаточно доказать, чтоA ` B.
Для этого достаточно установить, чтоA ` (B ∨ τ ) → B,поскольку (B ∨ τ ) в предположении A у нас уже есть. Для этого, всвою очередь, достаточно установить, что A ` (B → B) и A ` (τ →B). Первое очевидно (и посылка A не нужна), второе равносильновыводимости формулы (A ∧ τ ) → B, которая нам дана по условиюлеммы. Лемма 1 доказана.Проведённое рассуждение, как говорят, устанавливает допустимость (в интуиционистской логике) правила сечения, позволяющего«иссечь» формулу τ из формул (A∧τ ) → B и A → (B ∨τ ) и получитьформулу A → B.Возвращаясь к доказательству теоремы, рассмотрим произвольную непротиворечивую пару (A, B).
Рассматривая по очереди различные формулы τ , мы будем добавлять их к левой или правой части. Чтобы этот процесс («пополнение») был конечным, мы ограничимся формулами из некоторого множества.Фиксируем некоторое конечное множество формул F , которое содержит все формулы из A, B и замкнуто относительно перехода кподформулам (если формула входит в F , то все её подформулы входят в F ). Например, можно включить в F все подформулы всехформул из A и из B.Пару (X, Y ), у которой X, Y ⊂ F , будем называть полной, еслиона непротиворечива и любая формула из F входит либо в X, либо вY (то есть X ∪Y = F ). Заметим, что из непротиворечивости следует,что X ∩ Y = ∅, так что полная пара задаёт разбиение F на двечасти. (Более точно полные пары следовало бы называть «полнымиотносительно F », но у нас множество F фиксировано.)[п.
4]Интуиционистская пропозициональная логика69Лемма 2. Исходная пара (A, B) может быть расширена до полной:существует полная пара (X, Y ), для которой A ⊂ X, B ⊂ Y .Доказательство очевидно: применяем по очереди лемму 1 ко всемформулам из F .Точно так же любую непротиворечивую пару, составленную изформул множества F , можно расширить до полной. (Это замечаниенам впоследствии понадобится.)Для завершения доказательства теоремы 26 нам осталось показать, что всякая полная пара (A, B) совместна (существует шкала имир, в котором формулы из A истинны, а формулы из B ложны).
Вотличие от классического случая построение будет использовать нетолько пару (A, B), но и все полные пары.Шкала Крипке строится так. Мирами будут полные пары (R, S)(то есть всевозможные непротиворечивые разбиения множества F налевую и правую части). Истинность переменных определяется естественным образом: всякая переменная p, входящая в одну из формулмножества F , сама принадлежит множеству F (замкнутость относительно подформул); если p входит в левую часть полной пары (R, S),то p истинна в мире (R, S), если в правую — то ложна. (Впоследствииэто свойство мы распространим на все формулы: любая формулаиз R окажется истинной в мире (R, S), а любая формула из S —ложной.)Осталось определить порядок на множестве пар. Считаем, что(R1 , S1 ) 6 (R2 , S2 ), если R1 ⊂ R2 .
(Такое определение не удивительно, если вспомнить, что истинность формул наследуется вверх.)Лемма 3. В построенной шкале в мире (R, S) истинны все формулы из R и ложны все формулы из S.Доказательство леммы 3 проводится индукцией по построениюформул. Для переменных она верна по определению истинности.Пусть некоторая формула из F не является переменной. Тогда онаесть конъюнкция, дизъюнкция, импликация или отрицание и для еёчастей утверждение леммы верно по предположению индукции.
Рассмотрим все случаи по очереди, начав с конъюнкции и дизъюнкции(истинность которых не зависит от других миров).(∧R ) Пусть формула ϕ ∧ ψ входит в R. Тогда формулы ϕ и ψне могут входить в S, иначе пара (R, S) была бы противоречивой(из ϕ ∧ ψ выводится ϕ и ψ). Значит, ϕ и ψ входят в R (полнота),поэтому они истинны (предположение индукции), и потому ϕ ∧ ψистинна (определение истинности).(∧S ) Пусть формула ϕ ∧ ψ входит в S. Могут ли обе формулы ϕ70Исчисление высказываний[гл.
2]и ψ входить в R? Нет, так как в этом случае пара (R, S) была быпротиворечивой. Значит, хотя бы одна из формул входит в S, тогдапо предположению индукции она ложна, и потому формула ϕ ∧ ψложна в мире (R, S).(∨R ) Если формула ϕ ∨ ψ входит в R, то формулы ϕ и ψ не могутодновременно входить в S, и потому хотя бы одна из них истинна,так что и вся формула ϕ ∨ ψ истинна.(∨S ) Если формула ϕ ∨ ψ входит в S, то формулы ϕ и ψ не могутвходить в R, поэтому обе они ложны и формула ϕ ∨ ψ ложна.(→R ) Пусть формула ϕ → ψ входит в R.
Проверим, что она истинна в (R, S). Это значит, что в любом мире (R0 , S 0 ), который вышенашего (то есть R0 ⊃ R) и в котором истинна формула ϕ, должнабыть истинна и формула ψ. В самом деле, если ϕ истинна в (R0 , S 0 ),то она входит в R0 (предположение индукции). С другой стороны, иϕ → ψ входит в R0 , поскольку R0 ⊃ R. Теперь ясно, что формула ψне может входить в S 0 , так как в этом случае пара (R0 , S 0 ) была быпротиворечивой (из ϕ и ϕ → ψ выводится ψ).
Значит, ψ входит в R0и потому истинна в (R0 , S 0 ) по предположению индукции.(→S ) Это наиболее интересный случай, где нам снова потребуется пополнение. Пусть формула ϕ → ψ входит в S. Мы должныдоказать, что она ложна в мире (R, S). Согласно определению, этоозначает, что найдётся мир (R0 , S 0 ), для которого R0 ⊃ R и в котором формула ϕ истинна, а формула ψ ложна (то есть ϕ ∈ R0 иψ ∈ S 0 , согласно предположению индукции).
Как найти такой мир?Рассмотрим пару (R ∪ {ϕ}, {ψ}). Эта пара непротиворечива. В самомделе, если бы формула R ∧ ϕ → ψ была бы выводима, то и формулаR → (ϕ → ψ) была бы выводима (лемма о дедукции), и потому пара(R, S) была бы противоречива. Теперь можно расширить непротиворечивую пару (R ∪ {ϕ}, {ψ}) до полной пары (R0 , S 0 ), которая ибудет искомым миром.Отрицание рассматривается аналогично импликации (как мы говорили, можно вместо отрицания ввести тождественную ложь ⊥ ивообще его не рассматривать).(¬R ) Пусть формула ¬ϕ входит в R. Надо доказать, что формула ϕ ложна в любом мире (R0 , S 0 ) выше мира (R, S). Формула ϕ неможет входить в R0 , так как в R0 входит формула ¬ϕ (напомним, чтоR ⊂ R0 ), а из ϕ ∧ ¬ϕ выводится любая формула.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
