Перейти к содержимому
Topos Uranos

Краткое содержание

До сих пор формулы были цепочками кружков и дисков, а выводы были действиями над цепочками: об их истинности не было сказано ничего. Этот урок придаёт им значение. Оценка сопоставляет каждой переменной одно из двух истинностных значений, 11 (истина) и 00 (ложь), и единственным образом продолжается на все формулы рекурсией по их сложности с помощью одного-единственного пункта: (φ↓ψ)(\varphi \downarrow \psi) принимает значение 11 в точности тогда, когда φ\varphi и ψ\psi принимают значение 00. Из этого пункта и официальных сокращений вычисляются, без каких-либо новых соглашений, значения отрицания, дизъюнкции, конъюнкции, импликации, эквиваленции и строгой дизъюнкции. Лемма о совпадении, доказанная индукцией по сложности, гарантирует, что значение формулы зависит только от значений её переменных; из неё следует, что таблица истинности, в которой 2n2^n строк для nn переменных, содержит всё, что бесконечно многие оценки могут сказать о формуле. С помощью этого определяются выполнение, общезначимость, выполнимость, противоречие и нейтральность, фиксируются формулы ⊤\top и ⊥\bot и ставится задача распознавания общезначимости, которую таблицы решают ценой затрат, растущих экспоненциально с числом переменных.

Цели обучения

  1. Вычислять истинностное значение формулы при оценке с помощью её рекурсивного продолжения и получать из официальных сокращений значение каждой производной связки.
  2. Доказывать индукцией по сложности лемму о совпадении и объяснять с её помощью, почему таблицы истинности из 2n2^n строк достаточно для изучения формулы с nn переменными.
  3. Строить таблицы истинности столбец за столбцом и классифицировать формулы как общезначимые, нейтральные или противоречия, а множества формул как выполнимые или невыполнимые, не смешивая ⊭φ\not\models \varphi с противоречием.
  4. Решать вопрос об общезначимости формулы поиском оценки, которая её опровергает, и определять, как растут затраты метода таблиц в зависимости от числа переменных.

Значение формул

Раздел о языке построил в уроке о языке логики высказываний множество цепочек из двух символов, а раздел о выводе научил получать одни цепочки из других с помощью аксиом и правил. Ни один из них не говорил об истинности: дедуктивная система преобразует символы по их форме, как машина, которая не понимает того, что пишет. Однако язык строился для того, чтобы представлять высказывания, и урок о формализации естественного языка приписал им неформальные прочтения: (φ↓ψ)(\varphi \downarrow \psi) истинна, когда φ\varphi и ψ\psi обе ложны, а прочтения остальных связок были получены из этого. Семантика превращает эти прочтения в математические определения.

В её основе лежат два решения. Первое есть двузначность: имеется ровно два истинностных значения, которые записываются 11 (истина) и 00 (ложь), и каждая формула в каждой ситуации имеет одно из них. Второе есть истинностная функциональность: значение составной формулы зависит только от значений её компонент, а не от её предмета, так что истинность переменных определяет истинность всех формул. Урок о формализации показал цену этого второго решения (причинность, модальность и время остаются за пределами языка); награда за него в том, что семантика всего языка получается из одного-единственного пункта, пункта для исходной связки.

Следует, кроме того, заметить, что этот раздел целиком работает в метаязыке. Утверждения «φ\varphi истинна при такой-то оценке» или «φ\varphi есть тавтология» не являются формулами; это математические высказывания о формулах, и они доказываются обычными рассуждениями, часто индукцией по сложности; они не являются выводами в системе курса. Связь между двумя мирами, а именно то, что всё выводимое истинно и что всё истинное в точном смысле этого раздела выводимо, составляет предмет раздела о метатеории.