Часть I. Синтаксис
1. Формальная система и обыденное рассуждение
В заметке строится исчисление высказываний (ИВ): в части I язык, аксиомы, правило вывода и выводимость, в части II его модели. Построению предшествуют два вопроса: в каком отношении эта система находится к обыденной логике (настоящий параграф) и с чего следует начинать построение, чтобы избежать круга (§ 2). Обозначения вводятся по мере надобности.
ИВ строится в §§ 3–5 как семейство предикатов на словах конечного алфавита. В определениях не участвуют понятия истины, смысла и следования; знак \(\to\) является графическим знаком, и его чтение как «если …, то» в определения не входит. Поэтому утверждение о том, что ИВ моделирует логику обыденного рассуждения, из построения не следует. Теоремой оно быть не может: одна из сравниваемых сторон, обыденное рассуждение, формальным объектом не является.
Отождествление ИВ с обыденной логикой опирается на три обстоятельства: чтение знаков \(\neg, \land, \lor, \to\) как союзов «не», «и», «или», «если …, то»; согласие ИВ с практикой математических доказательств; теорему о полноте. Первое есть соглашение о произношении. Сопоставление с обыденной речью обнаруживает следующие расхождения. Каждая из приведённых формул является теоремой ИВ в смысле § 4; буквы \(\mathcal{A}, \mathcal{B}, \mathcal{C}\) обозначают произвольные формулы.
- 1.
Импликация без связи посылки и заключения. Теоремой является \((\mathcal{A} \to \mathcal{B}) \lor (\mathcal{B} \to \mathcal{A})\). При указанном чтении она утверждает, что из любых двух высказываний одно влечёт другое, тогда как обыденное «если» предполагает связь посылки с заключением (парадоксы материальной импликации, К. И. Льюис, 1918; спор о критерии истинности условного высказывания восходит к Филону и Диодору). Теорема \(\mathcal{A} \to \mathcal{A}\), напротив, с обыденной логикой согласуется.
- 2.
Порядок и причина в конъюнкции. Теоремой является \((\mathcal{A} \land \mathcal{B}) \to (\mathcal{B} \land \mathcal{A})\). Высказывания «приняли лекарство и выздоровели» и «выздоровели и приняли лекарство» сообщают разное (П. Стросон, 1952; Г. П. Грайс относит это различие к импликатурам и исключает его из условий истинности).
- 3.
Двузначность. Формула \(\mathcal{A} \lor \neg\mathcal{A}\) является аксиомой. Высказывания с нечётким предикатом («куча из ста зёрен велика»), высказывания о случайных будущих событиях (Аристотель, «Об истолковании», гл. 9) и высказывания с неудавшейся пресуппозицией («нынешний король Франции лыс»; Б. Рассел, 1905, П. Стросон, 1950) под эту схему очевидным образом не подпадают. Применительно к математическим утверждениям закон оспаривается интуиционистами (Л. Э. Я. Брауэр).
- 4.
Вывод и рассуждение. Выводимость монотонна (предложение 5.4): добавление гипотезы не отменяет выводимой формулы. Правовое рассуждение монотонности не подчиняется: более поздний закон частично отменяет более ранний, причём ранний закон не признаётся ложным с самого начала, а посылки упорядочены шкалой приоритетов. Правило modus ponens также не предписывает принять заключение: принявший \(\mathcal{A}\) и \(\mathcal{A} \to \mathcal{B}\) и обнаруживший ложность \(\mathcal{B}\) отказывается от одной из посылок (Г. Харман, 1986). Выводимость есть отношение между формулами; рассуждение есть пересмотр убеждений.
Математическая практика. В математических доказательствах расхождения 1–2 существенной роли не играют. Математические утверждения не зависят от времени и контекста, а основная форма условного утверждения является общей: «для всякого целого числа: если оно делится на \(4\), то оно чётно». Такое утверждение опровергается только контрпримером, в котором посылка верна, а заключение ложно. Числа \(8\) (обе части верны), \(2\) (посылка ложна, заключение верно) и \(3\) (обе части ложны) контрпримерами не являются. Если условное высказывание трактуется как функция истинностных значений, это требование определяет таблицу импликации, называемой материальной: она ложна только при истинной посылке и ложном заключении. Для записи доказательств в арифметике создавалось и исчисление Г. Фреге (1879), который сравнивал отношение своей записи к обыденному языку с отношением микроскопа к глазу.
Экспликация. Соотношение ИВ с обыденной логикой описывается понятием экспликации (Р. Карнап, 1950): неточное понятие (экспликандум) заменяется точным (экспликатом), который оценивается по сходству с экспликандумом, точности, плодотворности и простоте. Совпадения употреблений не требуется: биологическое понятие Piscis заменяет обиходное «рыба» и не охватывает кита. У. Куайн (1960, § 53) описывает экспликацию как устранение: выделяются функции неясного выражения, ради которых оно употребляется, для этих функций вводится замена, а синонимия не утверждается. Образцом служит упорядоченная пара в форме Куратовского: равенство \(\langle X,Y \rangle=\{\{X\},\{X,Y\}\}\) не выражает того, что подразумевалось под парой, и обеспечивает единственное требуемое свойство: \(\langle X,Y \rangle=\langle U,V \rangle\) тогда и только тогда, когда \(X=U\) и \(Y=V\).
В этом смысле ИВ является заменой обыденной логики и её моделью не является. Материальная импликация выполняет те функции условного высказывания, которые нужны в доказательствах: отделение заключения и запись общих утверждений. Другие функции союза «если» она не выполняет. Различие между моделью и заменой проявляется при расхождении: модель исправляется, когда расходится с моделируемым явлением, а при расхождении ИВ с обыденным суждением исправляется суждение. Импликация с ложной посылкой принимается истинной вопреки обыденному суждению, и критерием правильности математического рассуждения становится выводимость. Таким образом, ИВ обслуживает математику, включая информатику; для других областей знания такого обоснования у него нет, и переносить его туда не следует. Выбор замены не единствен: интуиционистская логика, релевантные логики и логики условных высказываний сохраняют иные функции обыденных союзов и оцениваются по тем же критериям.
Теорема о полноте. Теорема о полноте (§ 9) связывает два формальных предиката: выводимость и истинность по таблицам. Таблица импликации сама входит в замену, поэтому теорема о соотношении с обыденной логикой ничего не сообщает. Аргумент сжатия Г. Крайзеля (1967, для логики первого порядка; схема та же) выводит из полноты совпадение интуитивной общезначимости с обоими формальными понятиями при двух условиях: всё выводимое интуитивно общезначимо, и всё интуитивно общезначимое истинно по таблицам. Первое условие требует признания общезначимыми формул вида \(\neg\mathcal{A} \to (\mathcal{A} \to \mathcal{B})\). Оно выполнено для понятия правильности, принятого в математической практике, и не выполнено для обыденного употребления союза «если». Аргумент относится к уже отрегулированному понятию.
Замена не устраняет обыденную логику полностью. Определения ИВ формулируются на содержательном метаязыке, который сам пользуется союзами «если», «и», «не» (пункт Б4 соглашения 2.1). Соотношение объектного языка и метаязыка составляет предмет следующего параграфа.
2. Проблема порочного круга и выбор точки старта
Построение формальной логики без предварительных соглашений наталкивается на препятствие, описанное в диалоге Л. Кэрролла «Что Черепаха сказала Ахиллу» (1895) и в статье У. Куайна Truth by Convention (1936). Правила чтения и преобразования символов объектного языка формулируются на некотором метаязыке. Полная формализация метаязыка требует мета-метаязыка, что даёт бесконечный регресс; обоснование базовой логики средствами самой этой логики есть порочный круг (petitio principii).
В учебном изложении это препятствие обходится двумя способами, каждый из которых вызывает возражения с точки зрения оснований:
- 1)
Теоретико-множественное определение. Формула определяется как элемент пересечения всех индуктивных подмножеств свободного моноида \(\Alf^*\) над алфавитом \(\Alf\) (конструкция, восходящая к Фреге и Дедекинду, с квантором по \(\mathcal{P}(\Alf^*)\)) либо как последняя компонента конечного кортежа сборки \(\langle \xi_1, \dots, \xi_N \rangle \in (\Alf^*)^N\). Такое определение предполагает известными аксиоматическую теорию множеств (с аксиомами бесконечности и степени) или арифметику натурального ряда \(\mathbb{N}\), которые сами формулируются средствами логики предикатов и ИВ. Формального противоречия здесь нет, поскольку определяемая система и метатеория различны; возражение относится к порядку обоснования.
- 2)
Смешение определения и употребления. Формулировка «пусть \(\mathcal{A}, \mathcal{B}\) — произвольные формулы; тогда \((\mathcal{A} \to \mathcal{B})\) — формула» совмещает определение предиката «быть формулой» с употреблением уже определённого предиката. Возникает видимость, будто метапеременные \(\mathcal{A}, \mathcal{B}\) пробегают область значений, которая к моменту записи правила ещё не задана.
Разрыв круга достигается явной фиксацией точки старта. В соответствии с программой финитизма Д. Гильберта и П. Бернайса, каноническими исчислениями Э. Поста, теорией алгорифмов А. А. Маркова и изложением С. К. Клини предъявляется запас первичных понятий метатеории, принимаемых без формального определения. В этот запас не входят понятие множества, актуальная бесконечность и формальная теория арифметики. Выбор точки старта не единствен; критерием служит простота исходных понятий (см. замечание 2.1).
Мета-соглашение 2.1 (Первичная финитарная база метатеории). Без определения принимаются следующие понятия и умения содержательного метаязыка (русского языка с техническими обозначениями).
- Б1.
Знаки. Распознавание конечного списка конкретных графических знаков, их различение и отождествление различных вхождений одного знака.
- Б2.
Слова и приписывание. Слово — конечная линейная цепочка знаков, записанная слева направо. Операции: приписывание второго слова вплотную справа к первому и проверка посимвольного совпадения двух слов (обозначение: \(\equiv\)).
- Б3.
Предикаты. Предикаты \(\Atom\), \(\Form\), \(\Ax\), \(\Thm\) на словах языка обозначают определённые свойства слов, зависящие от их состава. Запись \(\Form\mo \xi\mc \) читается: «слово \(\xi\) есть формула».
- Б4.
Логика метаязыка. На метауровне используется обычная общечеловеческая логика в максимально простых и однозначных формулировках.
- Б5.
Рекурсивное построение классов слов. Сначала задаётся база: из всех слов выделяются определённые слова, относящиеся к классу. Затем задаются правила порождения новых слов из уже известных слов класса; класс должен быть замкнут относительно этих правил. Наконец, объявляется, что других слов в классе нет. Цепочка применений правил, начинающаяся с базы и оканчивающаяся данным словом, называется построением этого слова. Для класса теорем построение называется выводом.
- Б6.
Метапеременные. Буквы метаязыка, обозначающие слова, называются метапеременными. Если утверждение записано с метапеременной \(\mathcal{A}\), ограниченной формулами, то перед ним подразумевается условие «если \(\mathcal{A}\) — формула, то». Так же для метапеременных, ограниченных другими классами.
Замечание 2.1 (Потенциальная бесконечность и арифметика). Условие «других слов в классе нет» в Б5 — единственное место базы, где локализована потенциальная бесконечность. Оно не требует существования «множества всех слов» как завершённого объекта и обосновывает метод структурной индукции: свойство, которым обладают слова базы и которое сохраняется правилами, есть у всех слов класса. Если посылки каждого правила короче заключения или относятся к ранее определённому классу, то та же рекурсия даёт алгоритм распознавания: слово разбирается по правилам до базы. Для атомов и формул этот алгоритм работает за время, полиномиальное от длины слова. Для теорем условие нарушено: посылка \(\mathcal{A}\) правила Modus Ponens не входит в заключение \(\mathcal{B}\), и разрешимость класса теорем доказывается отдельно (замечание 4.4).
3. Алфавит, слова и синтаксические предикаты
Фиксируется объектный алфавит \(\Alf\), состоящий ровно из восьми знаков: \[|\qquad \st\qquad (\qquad )\qquad \neg\qquad {\land}\qquad {\lor}\qquad {\to}\] Словом в алфавите \(\Alf\) называется конечная цепочка его знаков; класс всех таких слов обозначается \(\Alf^*\) (звезда Клини). Греческие буквы \(\xi, \eta, \zeta\) являются метапеременными по словам из \(\Alf^*\). Приписывание записывается подряд: \((\xi\to\eta)\) есть слово, составленное из скобки, слова \(\xi\), знака \(\to\), слова \(\eta\) и скобки. Скобки при предикатах принадлежат метаязыку и выделены синим; составное слово в аргументе предиката заключается в одинарные кавычки: \(\Form\mo \q{(\xi\to\eta)}\mc \).
Пропозициональными переменными служат строки, составленные только из палочек и заключённые с двух сторон в решётки: \(\atm{|}\), \(\atm{||}\), \(\atm{|||}\) и т. д. Такая запись отвечает трём требованиям. Запас переменных должен быть потенциально бесконечным, поэтому конечного набора букв недостаточно. Этот запас должен задаваться простейшими правилами над конечным алфавитом, поэтому буквы с числовыми индексами, требующие цифр и понятия индекса, не используются. Замена переменной должна работать безошибочно, поэтому переменная не может быть подсловом другой переменной: слово \(|||\) является подсловом слова \(||||\), и при замене формула попала бы внутрь него, а атом \(\atm{|||}\) подсловом атома \(\atm{||||}\) не является. Буквы \(a, b, c\) встречаются далее только как метапеременные по атомам и в алфавит не входят.
Палочки наращиваются только в атомах, поэтому вводятся два предиката, \(\Atom\) и \(\Form\); первый входит в определение второго только как посылка правила F1.
Определение 3.1 (Предикат «быть атомом»). Предикат \(\Atom\mo \xi\mc \) задаётся рекурсивно:
- A1.
База: \(\Atom\mo \q{\atm{|}}\mc \).
- A2.
Правило: если \(\Atom\mo \q{\st\xi\st}\mc \), то \(\Atom\mo \q{\st\xi|\st}\mc \).
- A3.
Замыкание: никакие другие слова свойством \(\Atom\) не обладают.
Свойством \(\Atom\) обладают слова \(\atm{|}\), \(\atm{||}\), \(\atm{|||}\) и т. д. Вместо таких сложных записей переменных можно мысленно представлять себе \(p_1,p_2,p_3\) и т.д.
Определение 3.2 (Предикат «быть формулой»). Предикат \(\Form\mo \xi\mc \) задаётся рекурсивно:
- F1.
База: если \(\Atom\mo \xi\mc \), то \(\Form\mo \xi\mc \).
- F2.
Правило для отрицания: если \(\Form\mo \xi\mc \), то \(\Form\mo \q{\neg\xi}\mc \).
- F3.
Правила для бинарных связок: если \(\Form\mo \xi\mc \) и \(\Form\mo \eta\mc \), то \[\Form\mo \q{(\xi\land\eta)}\mc ,\qquad \Form\mo \q{(\xi\lor\eta)}\mc ,\qquad \Form\mo \q{(\xi\to\eta)}\mc .\]
- F4.
Замыкание: никакие другие слова свойством \(\Form\) не обладают.
Импликация в правиле F1 действует в одну сторону: всякий атом есть формула, а формула, содержащая связку или скобку, атомом не является.
Заглавные каллиграфические буквы \(\mathcal{A}, \mathcal{B}, \mathcal{C}\) обозначают формулы, строчные латинские \(a, b, c\) — атомы; это метапеременные, ограниченные в смысле Б6 (рис. 1). Запись \(\mathcal{A}(a)\) обозначает формулу \(\mathcal{A}\) с выделенной пропозициональной переменной \(a\); ни вхождение \(a\) в \(\mathcal{A}\), ни отсутствие в \(\mathcal{A}\) других переменных не требуются.
Сокращение скобок. Скобки сокращаются только в записи на метаязыке; само слово содержит их все. Внешние скобки опускаются: \(\mathcal{A} \to \mathcal{B}\) обозначает слово \((\mathcal{A}\to\mathcal{B})\). При вхождении в более длинную формулу они восстанавливаются: \(\neg(\mathcal{A} \to \mathcal{B})\), \(\mathcal{C} \to (\mathcal{A} \to \mathcal{B})\). Отрицание скобок не вводит, поэтому \(\neg\mathcal{A} \to \mathcal{B}\) однозначно читается как \((\neg\mathcal{A}) \to \mathcal{B}\). Употребительные дальнейшие соглашения (связки \(\land, \lor\) связывают сильнее, чем \(\to\); цепочка импликаций группируется вправо) в настоящем тексте не применяются.
Раскрытие условия. Раскрытие условия из Б6 устраняет видимость круга. Формулировка «если \(\mathcal{A}\) и \(\mathcal{B}\) — формулы, то \(\mathcal{A} \to \mathcal{B}\) — формула» записывается как \(\Form\mo \q{\mathcal{A} \to \mathcal{B}}\mc \) и означает \[\text{для всяких слов } \xi, \eta:\quad \text{если } \Form\mo \xi\mc \text{ и } \Form\mo \eta\mc , \text{ то } \Form\mo \q{(\xi\to\eta)}\mc ,\] то есть правило F3 для импликации. В этой записи \(\xi, \eta\) пробегают слова, заданные независимо от понятия формулы, а предикат \(\Form\) входит только в посылку и заключение правила. Совокупность формул заранее не предполагается. Сокращённая запись законна после определения 3.2; прочитанная как само определение, она и создаёт видимость круга.
Определение 3.3 (Подстановка). \(\mathcal{A}[\mathcal{B}/a]\) есть слово, получаемое из \(\mathcal{A}\) заменой всех вхождений атома \(a\) на формулу \(\mathcal{B}\). Для формулы, записанной как \(\mathcal{A}(a)\), пишется также \(\mathcal{A}(\mathcal{B})\).
Предложение 3.4. \(\mathcal{A}[\mathcal{B}/a]\) есть формула. Подстановка перестановочна со связками: \((\neg\mathcal{A})[\mathcal{B}/a] \equiv \neg\mathcal{A}[\mathcal{B}/a]\) и \((\mathcal{A} \circ \mathcal{C})[\mathcal{B}/a] \equiv \mathcal{A}[\mathcal{B}/a] \circ \mathcal{C}[\mathcal{B}/a]\), где \(\circ\) — один из знаков \(\land, \lor, \to\).
Доказательство. Атомы формулы разделены скобками и связками, поэтому вхождение атома \(a\) в формулу совпадает с одним из её атомов и не пересекает ни скобок, ни связок. Отсюда следует перестановочность. Структурная индукция по \(\mathcal{A}\): для атома результат есть \(\mathcal{B}\) или сам атом; для составной формулы применяются перестановочность, предположение индукции и правила F2, F3.
Анализ слов. Слова и формулы анализируются средствами рекурсивной арифметики (Т. Скулем, 1923): подсчитываются скобки, скобочный баланс и длина слова, применяется индукция по длине слова. Такое употребление арифметики есть содержательное, в смысле замечания 2.1.
Лемма 3.5 (Скобочный баланс и начальные отрезки).
- (a)
В формуле открывающих и закрывающих скобок поровну; в каждом её начальном отрезке открывающих не меньше, чем закрывающих; в каждом непустом собственном начальном отрезке формулы, начинающейся со скобки, открывающих строго больше.
- (b)
Собственный начальный отрезок формулы формулой не является.
Доказательство. (a) Структурная индукция.
(b) Структурная индукция по формуле \(\mathcal{C}\); пусть \(\mathcal{A}\) — формула и собственный начальный отрезок \(\mathcal{C}\). Если \(\mathcal{C}\) — атом, то \(\mathcal{A}\) начинается с решётки и потому является атомом, но в \(\mathcal{A}\) меньше двух решёток. Если \(\mathcal{C} \equiv \neg\mathcal{C}_1\), то \(\mathcal{A}\) начинается со знака \(\neg\); единственное правило, дающее такие формулы, есть F2, поэтому \(\mathcal{A} \equiv \neg\mathcal{A}_1\), где формула \(\mathcal{A}_1\) — собственный начальный отрезок \(\mathcal{C}_1\), что противоречит предположению индукции. Если \(\mathcal{C}\) начинается со скобки, то по (a) в \(\mathcal{A}\) открывающих скобок строго больше, чем закрывающих, что противоречит (a) для формулы \(\mathcal{A}\).
Предложение 3.6 (Однозначность разбора). Всякая формула \(\mathcal{A}\) имеет ровно один из следующих видов: атом; \(\neg\mathcal{A}_1\); \((\mathcal{A}_1\circ\mathcal{A}_2)\), где \(\circ\) — один из знаков \(\land, \lor, \to\). При этом формулы \(\mathcal{A}_1, \mathcal{A}_2\) и знак \(\circ\) определены однозначно.
Доказательство. Вид формулы определяется её первым знаком: решёткой, \(\neg\) или открывающей скобкой. В случае отрицания единственность \(\mathcal{A}_1\) очевидна. Пусть \((\mathcal{A}_1\circ\mathcal{A}_2) \equiv (\mathcal{B}_1\bullet\mathcal{B}_2)\). Если \(\mathcal{A}_1 \not\equiv \mathcal{B}_1\), то одна из этих формул есть собственный начальный отрезок другой, что противоречит лемме 3.5 (b). Следовательно, \(\mathcal{A}_1 \equiv \mathcal{B}_1\), откуда \(\circ \equiv \bullet\) и \(\mathcal{A}_2 \equiv \mathcal{B}_2\).
4. Аксиомы и теоремы исчисления
Предикат «быть теоремой ИВ» определяется чисто синтаксически: фиксируются аксиомы и замыкание относительно правила вывода. От него отличается понятие тавтологии: тавтологией называется формула, истинная по таблицам при всех распределениях значений на входящих в неё атомах (определение 7.2). Совпадение этих двух предикатов есть содержание теорем о корректности и о полноте (Э. Пост, 1921; вывод по таблице истинности строится в доказательстве Л. Кальмара, 1935), а не определение.
Аксиомы задаются схемами.
Определение 4.1 (Предикат «быть аксиомой»). Выражения следующего списка содержат метапеременные и словами языка ИВ не являются. Аксиомой называется всякая их реализация, то есть слово, получаемое заменой метапеременных \(\mathcal{A}, \mathcal{B}, \mathcal{C}\) конкретными формулами. Никакие другие слова аксиомами не являются.
утверждение консеквента: \(\mathcal{A} \to (\mathcal{B} \to \mathcal{A})\);
аксиома Фреге: \((\mathcal{A} \to (\mathcal{B} \to \mathcal{C})) \to ((\mathcal{A} \to \mathcal{B}) \to (\mathcal{A} \to \mathcal{C}))\);
удаление конъюнкции: \((\mathcal{A} \land \mathcal{B}) \to \mathcal{A}\), \((\mathcal{A} \land \mathcal{B}) \to \mathcal{B}\);
введение конъюнкции: \(\mathcal{A} \to (\mathcal{B} \to (\mathcal{A} \land \mathcal{B}))\);
введение дизъюнкции: \(\mathcal{A} \to (\mathcal{A} \lor \mathcal{B})\), \(\mathcal{B} \to (\mathcal{A} \lor \mathcal{B})\);
конструктивная дилемма: \((\mathcal{A} \to \mathcal{C}) \to ((\mathcal{B} \to \mathcal{C}) \to ((\mathcal{A} \lor \mathcal{B}) \to \mathcal{C}))\);
закон Дунса Скота: \(\neg\mathcal{A} \to (\mathcal{A} \to \mathcal{B})\);
введение отрицания: \((\mathcal{A} \to \mathcal{B}) \to ((\mathcal{A} \to \neg\mathcal{B}) \to \neg\mathcal{A})\);
закон исключённого третьего: \(\mathcal{A} \lor \neg\mathcal{A}\).
Каждая реализация получается подстановкой формул вместо атомов в конкретную формулу и по предложению 3.4 является формулой.
Определение 4.2 (Предикат «быть теоремой ИВ»). Предикат \(\Thm\) задаётся рекурсивно:
- T1.
База: если \(\Ax\mo \mathcal{A}\mc \), то \(\Thm\mo \mathcal{A}\mc \).
- T2.
Правило Modus Ponens: если \(\Thm\mo \mathcal{A}\mc \) и \(\Thm\mo \q{\mathcal{A} \to \mathcal{B}}\mc \), то \(\Thm\mo \mathcal{B}\mc \).
- T3.
Замыкание: никакие другие слова свойством \(\Thm\) не обладают.
Замечание 4.3 (Конечный список аксиом). Тот же класс теорем получается из 11 конкретных формул, в которых вместо \(\mathcal{A}, \mathcal{B}, \mathcal{C}\) стоят атомы \(\atm{|}, \atm{||}, \atm{|||}\), при добавлении правила «если \(\mathcal{A}\) — теорема, то \(\mathcal{A}[\mathcal{B}/a]\) — теорема». Подстановка в аксиому схемы даёт аксиому той же схемы; обратно, произвольная аксиома схемы получается последовательными подстановками через промежуточные атомы, более длинные, чем все атомы, входящие в \(\mathcal{A}, \mathcal{B}, \mathcal{C}\). Без промежуточных атомов подстановка вместо атома \(\atm{||}\) затронула бы его вхождения в уже подставленную формулу \(\mathcal{A}\).
Замечание 4.4 (Разрешимость). Классы атомов, формул и теорем ИВ разрешимы: для любого слова \(\xi\) за конечное число шагов устанавливается как выполнение, так и невыполнение каждого из предикатов \(\Atom\mo \xi\mc \), \(\Form\mo \xi\mc \), \(\Thm\mo \xi\mc \). Для атомов и формул алгоритмом служит разбор по предложению 3.6; он полиномиален по длине слова. Для теорем также существует метод конечного поиска доказательства, опирающийся на функциональную модель исчисления высказываний.
5. Выводимость в контексте списка гипотез
В теоретико-множественном изложении отношение выводимости связывает произвольное, возможно бесконечное, множество формул и одну формулу. В финитарной метатеории понятия множества нет, и гипотезы записываются конечным списком формул. Однако чтобы сформировать список формул, требуется ввести в алфавит какой-то свежий символ — разделитель формул в списке, чтобы уметь этот список однозначно разбирать на формулы. Поэтому мы добавим в алфавит запятую в качестве нового символа и обозначим новый расширенный алфавит за \(\Alf'\).
Поскольку расширенный алфавит содержит в себе исходный, то предикаты \(\Atom\), \(\Form\), \(\Thm\) над новым алфавитом будут задавать ровно те же самые классы слов, и смысл переменных \(\mathcal{A},\mathcal{B},\dots\) и \(a,b,\dots\) остаётся тем же. Запятая позволяет определить новый вид слова: список формул. Поскольку ранее мы закрепили за строчными греческими буквами только слова в исходном алфавите, для слов нового алфавита будем использовать прописные греческие буквы: \(\Gamma,\Delta\). В их область действия автоматически попадают и слова старого алфавита.
Определение 5.1 (Список формул и вхождение в список). Предикат \(\List\mo \Gamma\mc \) и утверждение \(\mathcal{A} \trianglelefteq \Gamma\) («формула \(\mathcal{A}\) входит в список \(\Gamma\)») определяются совместной рекурсией:
- L1.
Одноэлементный список: \(\List\mo \mathcal{B}\mc \) и \(\mathcal{B} \trianglelefteq \mathcal{B}\).
- L2.
Присоединение формулы к списку: если \(\List\mo \Gamma\mc \), то \(\List\mo \q{\Gamma,\mathcal{B}}\mc \) и \(\mathcal{B} \trianglelefteq \Gamma,\mathcal{B}\); если к тому же \(\mathcal{A} \trianglelefteq \Gamma\), то \(\mathcal{A} \trianglelefteq \Gamma,\mathcal{B}\).
- L3.
Замыкание: никакие другие слова списками не являются, и никакие другие пары из формулы и списка отношением \(\trianglelefteq\) не связаны.
Формулы запятой не содержат, поэтому разбиение списка на составляющие его формулы однозначно.
Список гипотез фиксируется и называется контекстом. Вместо бинарного отношения между списками и формулами вводится предикат на формулах, зависящий от контекста как от параметра. Допускается и пустой контекст, то есть отсутствие гипотез. Пустой контекст словом не является: это случай, когда параметр не указан, поэтому обозначения для него не требуется. Далее буквы \(\Gamma, \Delta\) обозначают контексты. При пустом \(\Gamma\) ни одна формула в него не входит, запись \(\Gamma, \mathcal{A}\) означает список из одной формулы \(\mathcal{A}\), а запись \(\Gamma \vdash \mathcal{A}\) принимает вид \(\vdash \mathcal{A}\).
Определение 5.2 (Выводимость в контексте). Пусть \(\Gamma\) — контекст. Предикат \(\Gamma \vdash \mathcal{A}\) («формула \(\mathcal{A}\) выводима в контексте \(\Gamma\)») задаётся рекурсивно:
- D1.
База аксиом: если \(\Ax\mo \mathcal{A}\mc \), то \(\Gamma \vdash \mathcal{A}\).
- D2.
База гипотез: если \(\mathcal{A} \trianglelefteq \Gamma\), то \(\Gamma \vdash \mathcal{A}\).
- D3.
Правило Modus Ponens: если \(\Gamma \vdash \mathcal{A}\) и \(\Gamma \vdash \mathcal{A} \to \mathcal{B}\), то \(\Gamma \vdash \mathcal{B}\).
- D4.
Замыкание: никакие другие формулы в контексте \(\Gamma\) не выводимы.
В пустом контексте правило D2 не применяется, поскольку ни одна формула в него не входит: выводимость \(\vdash \mathcal{A}\) задаётся правилами D1, D3, D4.
Пример вывода. Вывод в контексте есть конечная цепочка формул, каждая из которых является аксиомой (D1), гипотезой (D2) или получена из двух предшествующих по правилу Modus Ponens (D3). Для любых атомов \(a, b\) выполнено \(a, \neg a \vdash b\):
| 1. | \(\neg a\) | гипотеза |
| 2. | \(\neg a \to (a \to b)\) | аксиома (закон Дунса Скота) |
| 3. | \(a \to b\) | Modus Ponens: 1, 2 |
| 4. | \(a\) | гипотеза |
| 5. | \(b\) | Modus Ponens: 4, 3 |
Строки таблицы содержат метапеременные и словами языка ИВ не являются, поэтому приведён не один вывод, а схема вывода: каждая реализация метапеременных \(a, b\) конкретными атомами даёт отдельный вывод, и таких выводов бесконечно много.
Предложение 5.3.
- (a)
\(\Thm\mo \mathcal{A}\mc \) тогда и только тогда, когда \(\vdash \mathcal{A}\).
- (b)
Замена посылки \(\Ax\mo \mathcal{A}\mc \) на \(\Thm\mo \mathcal{A}\mc \) в правиле D1 даёт тот же предикат.
Доказательство. (a) Правила D1 и D3 без контекста совпадают с правилами для \(\Thm\). (b) По (a) теорема имеет вывод в пустом контексте, в котором применяются только D1 и D3; тот же вывод годится в контексте \(\Gamma\).
Предложение 5.4 (Монотонность по контексту). Если \(\Gamma \vdash \mathcal{A}\) и всякая формула, входящая в \(\Gamma\), входит в контекст \(\Delta\), то \(\Delta \vdash \mathcal{A}\). В частности, \(\Gamma, \mathcal{B} \vdash \mathcal{A}\).
Доказательство. Индукция по выводу: правила D1 и D3 от контекста не зависят, а гипотеза из \(\Gamma\) есть гипотеза из \(\Delta\).
Предложение 5.5 (Теорема о дедукции; Ж. Эрбран, 1930). \(\Gamma,\mathcal{A} \vdash \mathcal{B}\) тогда и только тогда, когда \(\Gamma \vdash \mathcal{A} \to \mathcal{B}\).
Доказательство. Обратное утверждение есть Modus Ponens. Для прямого применяется индукция по выводу \(\Gamma,\mathcal{A} \vdash \mathcal{B}\). При \(\mathcal{B} \equiv \mathcal{A}\) используется теорема \(\mathcal{A} \to \mathcal{A}\), выводимая двумя применениями Modus Ponens к реализациям аксиомы Фреге и утверждения консеквента. Если \(\mathcal{B}\) — аксиома или гипотеза из \(\Gamma\), то применяется утверждение консеквента. Шаг Modus Ponens обслуживается аксиомой Фреге.
Через \(\Gamma[\mathcal{B}/a]\) обозначается контекст, получаемый из \(\Gamma\) подстановкой в каждую его формулу.
Предложение 5.6 (Подстановка в выводе). Если \(\Gamma \vdash \mathcal{A}\), то \(\Gamma[\mathcal{B}/a] \vdash \mathcal{A}[\mathcal{B}/a]\). В частности, если атом \(a\) не входит в формулы контекста \(\Gamma\), то \(\Gamma \vdash \mathcal{A}[\mathcal{B}/a]\), а если \(\Thm\mo \mathcal{A}\mc \), то \(\Thm\mo \mathcal{A}[\mathcal{B}/a]\mc \).
Доказательство. Индукция по выводу \(\Gamma \vdash \mathcal{A}\). Подстановка в аксиому даёт аксиому той же схемы. Из \(\mathcal{A} \trianglelefteq \Gamma\) следует \(\mathcal{A}[\mathcal{B}/a] \trianglelefteq \Gamma[\mathcal{B}/a]\). Для правила Modus Ponens применяется перестановочность подстановки с импликацией (предложение 3.4).
Ограничений на переменные формулы \(\mathcal{B}\) предложение 5.6 не требует: подстановка выполняется за один проход, и подставленные вхождения повторно не просматриваются. Условие появляется лишь при нескольких последовательных подстановках, если результат должен совпасть с заданной формулой: следующая подстановка затрагивает и атомы, внесённые предыдущей.
Предложение 5.7 (Инвариантность относительно перестановки атомов). Пусть \(\pi\) — перестановка конечного числа атомов; остальные атомы остаются на месте. Через \(\mathcal{A}^\pi\) обозначается формула, полученная из \(\mathcal{A}\) заменой за один проход каждого атома \(a\) атомом \(\pi(a)\), через \(\Gamma^\pi\) — контекст, полученный так же из \(\Gamma\). Тогда \(\Gamma \vdash \mathcal{A}\) тогда и только тогда, когда \(\Gamma^\pi \vdash \mathcal{A}^\pi\). В частности, \(\Thm\mo \mathcal{A}\mc \) тогда и только тогда, когда \(\Thm\mo \mathcal{A}^\pi\mc \).
Доказательство. Индукция по выводу \(\Gamma \vdash \mathcal{A}\). Реализация схемы аксиом переходит в реализацию той же схемы, гипотеза из \(\Gamma\) — в гипотезу из \(\Gamma^\pi\), а шаг Modus Ponens — в шаг Modus Ponens, поскольку \((\mathcal{A} \to \mathcal{B})^\pi \equiv \mathcal{A}^\pi \to \mathcal{B}^\pi\). Обратное утверждение получается применением обратной перестановки.
Взаимная однозначность существенна: формула \(a \to a\) есть теорема и получается склейкой атомов из формулы \(a \to b\), которая теоремой не является (§ 7).
Продолжение примера. Схема \(a, \neg a \vdash b\) переносится с атомов на формулы. Для формул \(\mathcal{A}, \mathcal{B}\) выбирается атом \(b\), не входящий в \(\mathcal{A}\), и атом \(a\), отличный от \(b\). Подстановка \(\mathcal{A}\) вместо \(a\) даёт \(\mathcal{A}, \neg\mathcal{A} \vdash b\). Поскольку в \(\mathcal{A}\) нет атома \(b\), в этот контекст он не входит, и подстановка \(\mathcal{B}\) вместо \(b\) даёт \(\mathcal{A}, \neg\mathcal{A} \vdash \mathcal{B}\). В силу монотонности (предложение 5.4) из всякого контекста, содержащего формулу и её отрицание, выводима любая формула.
Замечание 5.8 (Подстановка только в заключение). Подстановка в заключение без подстановки в контекст вывод не сохраняет: из \(a \vdash a\) получалось бы \(a \vdash a \land \neg a\), что неверно для любой переменной \(a\) по теореме о корректности (§ 7). Подстановка согласованная, \(a \land \neg a \vdash a \land \neg a\), верна. Поэтому подстановка не может быть правилом вывода в определении 5.2: при таком правиле теорема о дедукции дала бы теорему \(a \to (a \land \neg a)\).
Замечание 5.9 (Границы списочного определения). Конечности списка достаточно для определения выводимости, поскольку вывод использует конечное число гипотез. Бесконечная совокупность гипотез допускается, если она задана предикатом \(H\): правило D2 заменяется правилом «если \(H(\mathcal{A})\), то \(\mathcal{A}\) выводима в контексте \(H\)». Утверждения о произвольных бесконечных совокупностях формул (теорема компактности, лемма Линденбаума в общей форме) в базе не формулируются и требуют теоретико-множественной метатеории. Финитарная база достаточна для построения исчисления и не покрывает всей его метатеории.
Часть II. Модели исчисления высказываний
6. Назначение моделей
Часть I определяет теоремы и выводимость как свойства слов. Выводимость формулы подтверждается предъявлением вывода, а её невыводимость из определения напрямую не усматривается: для этого нужно перебрать все возможные выводы (с учётом правила Modus Ponens возникает проблема поиска нужной посылки \(\mathcal A\), отсутствующей в консеквенте). Модель решает эту проблему. Формулам сопоставляются элементы некоторой алгебры (означивание формул) так, что все выводимые формулы (теоремы) получают одно конкретное значение в этой алгебре; формулы с иными значениями не выводимы. Схема такого сопоставления приведена на рис. 3: значения атомов задаются произвольно, значение всякой другой формулы определяется её строением, а все теоремы получают значение \(1\).
Слово «модель» употребляется здесь в строгом математическом смысле, имея полностью противоположную коннотацию рассмотренному в § 1: там спрашивалось, моделирует ли ИВ внешнее явление, здесь математические структуры служат моделями ИВ. Истинностные таблицы являются частью той же замены и об обыденной логике ничего не сообщают.
Математическая модель может использоваться для интерпретации или обоснования того или иного явления или конструкции как за пределами математики, так и внутри неё самой. Модель исчисления высказываний — как раз второй случай: мы строим класс теоретико-множественных моделей некоторого формального исчисления. Целью такого моделирования является переложение чисто синтаксического исчисления на язык алгебры (или других разделов математики, например, топологии), чтобы, с одной стороны, воспользоваться более привычным набором понятий, а с другой стороны, получить доступ к инструментам развитого аппарата алгебраических структур (пример см. в § 10). В то же время построение модели (или, точнее, класса моделей) требует от неё в определённом смысле точности: при переводе с языка исчисления на язык алгебры мы должны воспроизвести все выводимые соотношения формул с точностью до их эквивалентности (корректность) и постараться не привнести новые (полнота).
Кроме того, этот перевод должен быть устроен таким образом, чтобы всякий результат о формулах можно было бы однозначно интерпретировать в моделях и, обратно, всякий общий для моделей данного класса алгебраический результат (уравнение) можно было бы однозначно (по модулю строго определённой эквивалентности формул) интерпретировать в исчислении. Именно поэтому два главных требования к классу моделей — корректность и полнота — являются определяющими при выборе класса моделей исчисления. Таких классов может быть несколько (или бесконечно много), такие классы могут содержать лишь одну-единственную модель или много (не обязательно изоморфных) моделей, способ их построения может быть каким угодно в рамках классической теории множеств, но корректность и полнота классов должны соблюдаться безусловно, если мы хотим иметь точное алгебраическое представление об исчислении.
Заметим, что именно класс моделей, а не одна конкретная модель решает задачи корректной и полной интерпретации, потому что каждая конкретная модель своего класса может обладать какими-то весьма конкретными алгебраическими теоремами, неверными для всего класса в целом и неверными (после обратного перевода) в исчислении. Это и упрощает ситуацию с интерпретацией, и одновременно усложняет её. Упрощает — потому что набор общих для всего класса моделей теорем может быть значительно ýже теории одной конкретной модели; усложняет — потому что нам приходится описывать много моделей одновременно, не забывая про различные «крайние случаи».
В этой части метатеория свободно пользуется множествами, функциями и отношениями; финитарные ограничения части I сняты для удобства и полной математической свободы рассуждений. Обозначения метапеременных \(\mathcal{A}, \mathcal{B}, \mathcal{C}\) (для формул), \(a, b, c\) (начало латинского алфавита, для пропозициональных переменных), \(\Gamma,\Delta\) (для контекстов), \(\vdash\) (выводимость) сохраняют тот же смысл, что и раньше. Новое: договоримся, что часть латинского алфавита (несколько букв в конце), т.е. такие буквы, как \(x, y, z\), мы резервируем для значений формул, т.е. элементов модели, греческую \(\varepsilon\) — для функции оценки, \(n,m,k\) — для натуральных чисел. Естественно, мы также не будем пренебрегать использованием индексов и акцентов для увеличения количества используемых переменных.
7. Функциональная модель
На множестве \(\mathbb{B}=\{0,1\}\) заданы операции: \(\neg x = 1-x\), \(x \land y = \min(x,y)\), \(x \lor y = \max(x,y)\), \(x \to y = \max(1-x, y)\). Таблица истинности этих операций: \[\def\arraystretch{1.15} \begin{array}{cc|cccc} x & y & \neg x & x \land y & x \lor y & x \to y \\ \hline 0 & 0 & 1 & 0 & 0 & 1 \\ 0 & 1 & 1 & 0 & 1 & 1 \\ 1 & 0 & 0 & 0 & 1 & 0 \\ 1 & 1 & 0 & 1 & 1 & 1 \end{array}\]
Определение 7.1 (Оценка). Оценка \(\varepsilon\) сопоставляет каждому атому элемент \(0\) или \(1\) и продолжается на все формулы равенствами \(\varepsilon(\neg\mathcal{A}) = \neg \varepsilon(\mathcal{A})\) и \(\varepsilon(\mathcal{A} \circ \mathcal{B}) = \varepsilon(\mathcal{A}) \circ \varepsilon(\mathcal{B})\). Корректность продолжения обеспечена однозначностью разбора (предложение 3.6).
Значение \(\varepsilon(\mathcal{A})\) зависит только от значений \(\varepsilon\) на атомах, входящих в \(\mathcal{A}\). Поэтому формула, все атомы которой содержатся среди \(a_1, \dots, a_n\), задаёт функцию \(f_{\mathcal{A}} \colon \mathbb{B}^n \to \mathbb{B}\). Множество \(B_n\) всех таких функций с поточечными операциями называется функциональной моделью от \(n\) переменных; при этом \(f_{\neg\mathcal{A}} = \neg f_{\mathcal{A}}\) и \(f_{\mathcal{A} \circ \mathcal{B}} = f_{\mathcal{A}} \circ f_{\mathcal{B}}\), где \(\circ\) в правой части понимается поточечно. В \(B_n\) ровно \(2^{2^n}\) элементов.
Подстановка формулы в формулу соответствует смещению оценки: \(\varepsilon(\mathcal{A}[\mathcal{B}/a]) = \varepsilon'(\mathcal{A})\), где оценка \(\varepsilon'\) совпадает с \(\varepsilon\) всюду, кроме \(\varepsilon'(a) = \varepsilon(\mathcal{B})\). Это проверяется структурной индукцией по \(\mathcal{A}\).
Определение 7.2 (Тавтология и семантическое следование). Формула \(\mathcal{A}\) есть тавтология (обозначается: \(\models_{\mathbb{B}} \mathcal{A}\)), если \(\varepsilon(\mathcal{A})=1\) при всякой оценке \(\varepsilon\), то есть \(f_{\mathcal{A}}\) есть функция, тождественно равная \(1\).
Формула \(\mathcal{A}\) логически (семантически) следует из контекста \(\Gamma\) (\(\Gamma \models_{\mathbb{B}} \mathcal{A}\)), если для любой оценки \(\varepsilon\): если \(\varepsilon(\mathcal{C})=1\) при всех \(\mathcal{C} \trianglelefteq \Gamma\), то \(\varepsilon(\mathcal{A})=1\) (то есть значение \(1\) переносится с формул контекста \(\Gamma\) на \(\mathcal{A}\)).
При пустом \(\Gamma\) посылка выполнена для всякой оценки, поэтому запись \(\models_{\mathbb{B}} \mathcal{A}\) согласована с обозначением тавтологии.
Предложение 7.3 (Корректность). Если \(\Gamma \vdash \mathcal{A}\), то \(\Gamma \models_{\mathbb{B}} \mathcal{A}\). В частности, всякая теорема есть тавтология (случай пустого контекста).
Доказательство. Индукция по выводу. Все 11 схем аксиом дают тавтологии: это конечная проверка таблицами от трёх переменных, а по формуле для подстановки она распространяется на все реализации. Гипотезы получают значение \(1\) по условию. Если \(\varepsilon(\mathcal{A})=1\) и \(\varepsilon(\mathcal{A})\to \varepsilon(\mathcal{B})=1\), то \(\varepsilon(\mathcal{B})=1\). Для теоремы применяется предложение 5.3 (a): она выводима в пустом контексте.
Отсюда атом не является теоремой (достаточно \(\varepsilon(a)=0\)), \(a \nvdash a \land \neg a\) и пара \(\vdash \mathcal{A}\), \(\vdash \neg\mathcal{A}\) невозможна (непротиворечивость ИВ).
Кортеж значений \(\langle x_1, \dots, x_n \rangle \in \mathbb{B}^n\) сокращённо обозначается \(\vec{x}\), так что \(f(\vec{x})\) означает \(f(x_1, \dots, x_n)\).
Определение 7.4 (Литерал и совершенная дизъюнктивная нормальная форма). Для атома \(a\) и значения \(s \in \mathbb{B}\) литерал \(a^s\) есть формула, определяемая условиями \(a^1 \equiv a\) и \(a^0 \equiv \neg a\). Для функции \(f \in B_n\), не равной тождественно нулю, совершенной дизъюнктивной нормальной формой называется формула \[\mathcal{D}_f \equiv \bigvee_{\substack{\vec{x} \in \mathbb{B}^n \\ f(\vec{x})=1}} \bigl(a_1^{x_1} \land \dots \land a_n^{x_n}\bigr),\] то есть дизъюнкция конъюнкций литералов по всем кортежам \(\vec{x}\), на которых \(f\) равна \(1\). Это запись на метаязыке: кортежи берутся в лексикографическом порядке, скобки в конъюнкциях и дизъюнкциях расставляются влево, так что \(\mathcal{C}_1 \land \mathcal{C}_2 \land \mathcal{C}_3\) обозначает \((\mathcal{C}_1 \land \mathcal{C}_2) \land \mathcal{C}_3\).
Предложение 7.5 (Функциональная полнота). Всякая функция из \(B_n\) при \(n \geqslant 1\) есть \(f_{\mathcal{A}}\) для некоторой формулы \(\mathcal{A}\) с атомами из \(a_1, \dots, a_n\).
Доказательство. Для функции \(f \in B_n\), не равной тождественно нулю, проверяется равенство \(f_{\mathcal{D}_f} = f\). Пусть \(\vec{y} \in \mathbb{B}^n\) и \(\varepsilon(a_i)=y_i\) при всех \(i\). По таблице истинности \(\varepsilon(a^s)=1\) тогда и только тогда, когда \(\varepsilon(a)=s\). Поэтому конъюнкция \(a_1^{x_1} \land \dots \land a_n^{x_n}\) получает значение \(1\) в точности при \(\vec{y}=\vec{x}\), а формула \(\mathcal{D}_f\) — в точности при \(f(\vec{y})=1\). Тождественному нулю соответствует формула \(a_1 \land \neg a_1\).
Функциональная полнота означает выразимость всякой функции формулой и от логической полноты отличается. Утверждение, обратное предложению 7.3 (всё, что истинно в модели, выводимо), следует из общей конструкции для булевых алгебр и доказывается в теореме 9.3.
8. Булевы алгебры как модели
Булева алгебра есть дистрибутивная решётка \(\langle B, \land, \lor, 0, 1 \rangle\) с дополнением: \(x \land \neg x = 0\), \(x \lor \neg x = 1\). В ней полагается \(x \to y = \neg x \lor y\), а \(x \leqslant y\) означает \(x \land y = x\). Примеры: \(\mathbb{B}\); функциональная модель \(B_n\); множество всех подмножеств множества \(X\) с теоретико-множественными операциями. Одноэлементная алгебра, в которой \(0=1\), не исключается.
Оценка со значениями в булевой алгебре \(B\) задаётся и продолжается как в определении 7.1. Запись \(\Gamma \models_{\mathsf{BA}} \mathcal{A}\) означает: в каждой булевой алгебре \(B\) всякая оценка \(\varepsilon\), для которой \(\varepsilon(\mathcal{C})=1\) при всех \(\mathcal{C} \trianglelefteq \Gamma\), удовлетворяет \(\varepsilon(\mathcal{A})=1\). Отношение \(\models_{\mathbb{B}}\) есть частный случай с единственной моделью \(\mathbb{B}\).
Лемма 8.1.
- (a)
\(x \to y = 1\) тогда и только тогда, когда \(x \leqslant y\).
- (b)
Булево тождество, верное в \(\mathbb{B}\), верно во всякой булевой алгебре.
Доказательство. (a) Если \(x \leqslant y\), то \(\neg x \lor y \geqslant \neg x \lor x = 1\). Если \(\neg x \lor y = 1\), то \(x = x \land (\neg x \lor y) = x \land y\). (b) Законы булевой алгебры приводят каждую часть тождества к совершенной дизъюнктивной нормальной форме, которая определяется таблицей значений в \(\mathbb{B}\); формы обеих частей совпадают.
Предложение 8.2 (Корректность относительно класса булевых алгебр). Если \(\Gamma \vdash \mathcal{A}\), то \(\Gamma \models_{\mathsf{BA}} \mathcal{A}\).
Доказательство. Индукция по выводу. Аксиомы суть тавтологии, поэтому по лемме 8.1 (b) получают значение \(1\) во всякой булевой алгебре. Гипотезы получают значение \(1\) по условию. Если \(\varepsilon(\mathcal{A})=1\) и \(\varepsilon(\mathcal{A}) \to \varepsilon(\mathcal{B})=1\), то по лемме 8.1 (a) имеем \(1 \leqslant \varepsilon(\mathcal{B})\).
9. Полнота
9.1. Полнота относительно класса булевых алгебр
Модель, опровергающая невыводимую формулу, строится из самого синтаксиса. Фиксируется контекст \(\Gamma\). Запись \(\mathcal{A} \preceq \mathcal{B}\) означает \(\Gamma \vdash \mathcal{A} \to \mathcal{B}\); формулы эквивалентны, \(\mathcal{A} \sim \mathcal{B}\), если \(\mathcal{A} \preceq \mathcal{B}\) и \(\mathcal{B} \preceq \mathcal{A}\).
Лемма 9.1. Выполнены следующие свойства; при их проверке применяется теорема о дедукции (предложение 5.5).
- (1)
\(\preceq\) рефлексивно (теорема \(\mathcal{A} \to \mathcal{A}\)) и транзитивно;
- (2)
\(\mathcal{A} \land \mathcal{B}\) есть точная нижняя грань \(\mathcal{A}\) и \(\mathcal{B}\) относительно \(\preceq\) (удаление и введение конъюнкции);
- (3)
\(\mathcal{A} \lor \mathcal{B}\) есть точная верхняя грань (введение дизъюнкции и конструктивная дилемма);
- (4)
\(\mathcal{A} \land (\mathcal{B} \lor \mathcal{C}) \preceq (\mathcal{A} \land \mathcal{B}) \lor (\mathcal{A} \land \mathcal{C})\) (конструктивная дилемма в контексте с гипотезой \(\mathcal{A}\));
- (5)
\(\mathcal{A} \land \neg\mathcal{A} \preceq \mathcal{B}\) (закон Дунса Скота), \(\mathcal{B} \preceq \mathcal{A} \lor \neg\mathcal{A}\) (закон исключённого третьего), а из \(\mathcal{A} \preceq \mathcal{B}\) следует \(\neg\mathcal{B} \preceq \neg\mathcal{A}\) (введение отрицания);
- (6)
\((\mathcal{A} \to \mathcal{B}) \sim (\neg\mathcal{A} \lor \mathcal{B})\) (закон исключённого третьего для \(\mathcal{A}\), конструктивная дилемма и закон Дунса Скота);
- (7)
\(\Gamma \vdash \mathcal{A}\) тогда и только тогда, когда \(\mathcal{B} \preceq \mathcal{A}\) для всякой формулы \(\mathcal{B}\).
В силу леммы \(\sim\) есть конгруэнтность, а классы \([\mathcal{A}]\) с операциями \([\mathcal{A}] \land [\mathcal{B}] = [\mathcal{A} \land \mathcal{B}]\), \([\mathcal{A}] \lor [\mathcal{B}] = [\mathcal{A} \lor \mathcal{B}]\), \(\neg[\mathcal{A}] = [\neg\mathcal{A}]\) образуют булеву алгебру \(\mathsf{LT}_\Gamma\) — алгебру Линденбаума–Тарского контекста \(\Gamma\); при пустом контексте она обозначается \(\mathsf{LT}\). По пункту (7) её единица есть класс выводимых в контексте формул. По пункту (6) выполнено \([\mathcal{A} \to \mathcal{B}] = [\mathcal{A}] \to [\mathcal{B}]\).
Словарь перевода. Конструкция \(\mathsf{LT}_\Gamma\) переводит исчисление на язык алгебры. Порядок булевой алгебры есть отношение \(\preceq\): неравенство \([\mathcal{A}] \leqslant [\mathcal{B}]\) означает \(\Gamma \vdash \mathcal{A} \to \mathcal{B}\), то есть по теореме о дедукции \(\Gamma, \mathcal{A} \vdash \mathcal{B}\). Поэтому при контексте из одной формулы знак выводимости переводится в знак неравенства. Для алгебры \(\mathsf{LT}\) перевод таков:
| исчисление | алгебра \(\mathsf{LT}\) |
|---|---|
| формула \(\mathcal{A}\) | элемент \([\mathcal{A}]\) |
| связки \(\neg, \land, \lor, \to\) | операции \(\neg, \land, \lor, \to\) |
| эквивалентность \(\mathcal{A} \sim \mathcal{B}\) | равенство \([\mathcal{A}] = [\mathcal{B}]\) |
| \(\vdash \mathcal{A}\) | \([\mathcal{A}] = 1\) |
| \(\vdash \neg\mathcal{A}\) | \([\mathcal{A}] = 0\) |
| \(\mathcal{A} \vdash \mathcal{B}\) | \([\mathcal{A}] \leqslant [\mathcal{B}]\) |
| \(\mathcal{C}_1, \dots, \mathcal{C}_k \vdash \mathcal{B}\) | \([\mathcal{C}_1] \land \dots \land [\mathcal{C}_k] \leqslant [\mathcal{B}]\) |
| \(\mathcal{C}, \mathcal{A} \vdash \mathcal{B}\) равносильно \(\mathcal{C} \vdash \mathcal{A} \to \mathcal{B}\) | \(z \land x \leqslant y\) равносильно \(z \leqslant x \to y\) |
| правило Modus Ponens | \(x \land (x \to y) \leqslant y\) |
| оценка \(\varepsilon\) | гомоморфизм \(\mathsf{LT} \to \mathbb{B}\) |
| перестановка атомов \(\pi\) | автоморфизм \([\mathcal{A}] \mapsto [\mathcal{A}^\pi]\) |
Теорема 9.2 (Полнота относительно класса булевых алгебр). \(\Gamma \vdash \mathcal{A}\) тогда и только тогда, когда \(\Gamma \models_{\mathsf{BA}} \mathcal{A}\).
Доказательство. Прямое утверждение есть предложение 8.2. Пусть \(\Gamma \nvdash \mathcal{A}\). Канонической оценкой \(\varepsilon(a)=[a]\) в \(\mathsf{LT}_\Gamma\) структурной индукцией получается \(\varepsilon(\mathcal{B})=[\mathcal{B}]\) для всех формул \(\mathcal{B}\). При \(\mathcal{C} \trianglelefteq \Gamma\) имеем \(\Gamma \vdash \mathcal{C}\), поэтому \(\varepsilon(\mathcal{C})=1\), тогда как \(\varepsilon(\mathcal{A}) = [\mathcal{A}] \neq 1\).
9.2. Сведение к одной модели
Теорема 9.3 (Э. Пост, 1921). \(\Gamma \vdash \mathcal{A}\) тогда и только тогда, когда \(\Gamma \models_{\mathbb{B}} \mathcal{A}\). В частности, \(\Thm\mo \mathcal{A}\mc \) тогда и только тогда, когда \(\mathcal{A}\) есть тавтология.
Доказательство. Прямое утверждение есть предложение 7.3. Пусть \(\Gamma \nvdash \mathcal{A}\). По лемме 9.1 (7) имеем \([\mathcal{A}] \neq 1\), поэтому \(\neg[\mathcal{A}] \neq 0\), и существует ультрафильтр \(U\) алгебры \(\mathsf{LT}_\Gamma\), содержащий \(\neg[\mathcal{A}]\).1 Отображение \(h \colon \mathsf{LT}_\Gamma \to \mathbb{B}\), где \(h(y)=1\) при \(y \in U\) и \(h(y)=0\) иначе, есть гомоморфизм. Действительно, по определению ультрафильтра \(\neg y \in U\) тогда и только тогда, когда \(y \notin U\), и \(y \land z \in U\) тогда и только тогда, когда \(y \in U\) и \(z \in U\); для дизъюнкции и импликации равенства следуют из этих двух, поскольку \(y \lor z = \neg(\neg y \land \neg z)\) и \(y \to z = \neg y \lor z\). Оценка с \(\varepsilon(a)=h([a])\) для всех атомов \(a\) даёт структурной индукцией \(\varepsilon(\mathcal{B})=h([\mathcal{B}])\) для всех формул \(\mathcal{B}\). При \(\mathcal{C} \trianglelefteq \Gamma\) имеем \([\mathcal{C}]=1 \in U\), откуда \(\varepsilon(\mathcal{C})=1\), а из \(\neg[\mathcal{A}] \in U\) следует \(\varepsilon(\mathcal{A})=0\). Следовательно, \(\Gamma \not\models_{\mathbb{B}} \mathcal{A}\).
Следствие 9.4. Формулы \(\mathcal{A}, \mathcal{B}\) с атомами из \(a_1, \dots, a_n\) эквивалентны в пустом контексте тогда и только тогда, когда \(f_{\mathcal{A}} = f_{\mathcal{B}}\). Отображение \([\mathcal{A}] \mapsto f_{\mathcal{A}}\) есть изоморфизм подалгебры \(\mathsf{LT}\), порождённой классами \([a_1], \dots, [a_n]\), на функциональную модель \(B_n\).
Доказательство. \(\mathcal{A} \sim \mathcal{B}\) означает \(\vdash \mathcal{A} \to \mathcal{B}\) и \(\vdash \mathcal{B} \to \mathcal{A}\); по теореме 9.3 это равносильно \(f_{\mathcal{A}} = f_{\mathcal{B}}\). Отсюда корректность и инъективность отображения. Сюръективность есть предложение 7.5.
Замечание 9.5 (Класс моделей и единственная модель). Теорема 9.2 получена прямой конструкцией: модель \(\mathsf{LT}_\Gamma\) построена из самой выводимости. Содержательный шаг составляет теорема 9.3: для ИВ достаточно одной конечной модели.
10. Вычисления в модели: полиномы Жегалкина
Перевод на язык алгебры даёт не только проверку выводимости перебором строк таблицы истинности, но и вычисления по правилам арифметики. Для этого булева алгебра перестраивается в кольцо.
В булевой алгебре полагается \(xy = x \land y\) и \(x + y = (x \land \neg y) \lor (\neg x \land y)\). На \(\mathbb{B}\) это умножение и сложение по модулю \(2\). Поэтому в \(\mathbb{B}\) выполнены законы коммутативного кольца с единицей, тождества \(x^2 = x\) и \(x + x = 0\), а также равенства \[\neg x = 1 + x, \qquad x \lor y = x + y + xy, \qquad x \to y = 1 + x + xy.\] По лемме 8.1 (b) всё это верно во всякой булевой алгебре: она есть коммутативное кольцо с единицей, в котором \(x^2 = x\) (булево кольцо; М. Стоун, 1936), а связки выражаются через кольцевые операции.
Определение 10.1 (Полином Жегалкина). Моном от атомов \(a_1, \dots, a_n\) есть произведение различных атомов; пустое произведение равно \(1\). Полином Жегалкина есть сумма различных мономов; пустая сумма равна \(0\). Формуле \(\mathcal{A}\) с атомами из \(a_1, \dots, a_n\) сопоставляется полином \(p_{\mathcal{A}}\): \(p_{a_i} = a_i\) и \[\begin{gather*} p_{\neg\mathcal{A}} = 1 + p_{\mathcal{A}}, \qquad p_{\mathcal{A} \land \mathcal{B}} = p_{\mathcal{A}} p_{\mathcal{B}},\\ p_{\mathcal{A} \lor \mathcal{B}} = p_{\mathcal{A}} + p_{\mathcal{B}} + p_{\mathcal{A}} p_{\mathcal{B}}, \qquad p_{\mathcal{A} \to \mathcal{B}} = 1 + p_{\mathcal{A}} + p_{\mathcal{A}} p_{\mathcal{B}}, \end{gather*}\] где скобки раскрываются и подобные приводятся по правилам \(x^2 = x\), \(x + x = 0\).
Теорема 10.2 (И. И. Жегалкин, 1927). При \(n \geqslant 1\) всякая функция из \(B_n\) записывается единственным полиномом Жегалкина от \(n\) переменных, и функция \(f_{\mathcal{A}}\) записывается полиномом \(p_{\mathcal{A}}\).
Доказательство. Второе утверждение проверяется структурной индукцией по приведённым равенствам. По предложению 7.5 всякая функция из \(B_n\) есть \(f_{\mathcal{A}}\), поэтому записывается полиномом. Мономов от \(n\) атомов \(2^n\), полиномов \(2^{2^n}\), то есть столько же, сколько функций в \(B_n\). Поэтому запись единственна.
Следствие 10.3. Для формул \(\mathcal{A}, \mathcal{B}\) с атомами из \(a_1, \dots, a_n\):
- (a)
\(\vdash \mathcal{A}\) тогда и только тогда, когда \(p_{\mathcal{A}} = 1\);
- (b)
\(\mathcal{A}\) и \(\mathcal{B}\) эквивалентны в пустом контексте тогда и только тогда, когда \(p_{\mathcal{A}} = p_{\mathcal{B}}\);
- (c)
\(\mathcal{A} \vdash \mathcal{B}\) тогда и только тогда, когда \(p_{\mathcal{A}} p_{\mathcal{B}} = p_{\mathcal{A}}\).
Доказательство. По теореме 9.3 и следствию 9.4 выводимость и эквивалентность сводятся к равенствам функций, а функции по теореме 10.2 однозначно записываются полиномами. Пункт (c) есть пункт (a) для формулы \(\mathcal{A} \to \mathcal{B}\).
Пример. Закон Пирса \(((a \to b) \to a) \to a\) проверяется в две строки. Имеем \(p_{a \to b} = 1 + a + ab\), откуда \[p_{(a \to b) \to a} = 1 + (1 + a + ab) + (1 + a + ab)a = a + ab + ab = a,\] то есть формула \((a \to b) \to a\) эквивалентна атому \(a\). Поэтому \(p_{((a \to b) \to a) \to a} = 1 + a + a \cdot a = 1\), и формула выводима; сам вывод из аксиом для этого не требуется.
Общие утверждения. Таблица истинности проверяет каждую формулу отдельно, а вычисление в кольце даёт утверждения о бесконечных семействах формул. Запись \(\mathcal{A} \leftrightarrow \mathcal{B}\) сокращает \((\mathcal{A} \to \mathcal{B}) \land (\mathcal{B} \to \mathcal{A})\). Её полином линеен: \(p_{\mathcal{A} \leftrightarrow \mathcal{B}} = 1 + p_{\mathcal{A}} + p_{\mathcal{B}}\).
Предложение 10.4 (С. Лесьневский, 1929). Формула, построенная из атомов с помощью одной лишь связки \(\leftrightarrow\), есть теорема тогда и только тогда, когда каждый атом входит в неё чётное число раз.
Доказательство. Индукцией по построению: полином формулы с \(m\) вхождениями атомов равен сумме этих вхождений и \(m-1\) единиц. Атом с чётным числом вхождений при сложении сокращается. Если таковы все атомы, то \(m\) чётно и полином равен \(1\). Иначе в полиноме остаётся атом, и он отличен от \(1\). Остаётся применить следствие 10.3 (a).
Контекст и идеал. В кольце контекст переводится в идеал: \(\mathcal{C}_1, \dots, \mathcal{C}_k \vdash \mathcal{B}\) тогда и только тогда, когда \(1 + p_{\mathcal{B}}\) лежит в идеале, порождённом полиномами \(1 + p_{\mathcal{C}_i}\). Если \(1 + p_{\mathcal{B}}\) лежит в этом идеале, то там, где все \(p_{\mathcal{C}_i}\) равны \(1\), полином \(p_{\mathcal{B}}\) также равен \(1\), и применяется теорема 9.3. Обратно, при \(q = p_{\mathcal{C}_1} \cdots p_{\mathcal{C}_k}\) выводимость означает \(q(1 + p_{\mathcal{B}}) = 0\), откуда \(1 + p_{\mathcal{B}} = (1 + q)(1 + p_{\mathcal{B}})\), а \(1 + q\) лежит в идеале. Гомоморфизм \(h\) из доказательства теоремы 9.3 есть эпиморфизм на \(\mathbb{F}_2\), а дополнение ультрафильтра \(U\) есть его ядро, максимальный идеал кольца \(\mathsf{LT}_\Gamma\).
11. Двойственность, единственность двузначной модели и полнота по Посту
Таблица истинности из § 7 не выбирается среди других: аксиомы и правило Modus Ponens определяют её однозначно с точностью до перестановки значений \(0\) и \(1\), а эта перестановка отвечает переходу к двойственным формулам. Расширить же исчисление с сохранением непротиворечивости и замкнутости относительно подстановки нельзя.
Определение 11.1 (Двойственная формула). Формула \(\mathcal{A}^*\) определяется рекурсией: \(a^* \equiv a\) для атомов, \((\neg\mathcal{A})^* \equiv \neg\mathcal{A}^*\), \((\mathcal{A} \land \mathcal{B})^* \equiv \mathcal{A}^* \lor \mathcal{B}^*\), \((\mathcal{A} \lor \mathcal{B})^* \equiv \mathcal{A}^* \land \mathcal{B}^*\), \((\mathcal{A} \to \mathcal{B})^* \equiv \neg\mathcal{A}^* \land \mathcal{B}^*\).
Теорема 11.2 (Принцип двойственности; Ч. Пирс, Э. Шрёдер). Если атомы формулы \(\mathcal{A}\) содержатся среди \(a_1, \dots, a_n\), то \(f_{\mathcal{A}^*}(x_1, \dots, x_n) = \neg f_{\mathcal{A}}(\neg x_1, \dots, \neg x_n)\). Следовательно:
- (a)
\(\mathcal{A} \vdash \mathcal{B}\) тогда и только тогда, когда \(\mathcal{B}^* \vdash \mathcal{A}^*\); в частности, формулы \(\mathcal{A}, \mathcal{B}\) эквивалентны в пустом контексте тогда и только тогда, когда эквивалентны \(\mathcal{A}^*, \mathcal{B}^*\);
- (b)
\(\vdash \mathcal{A}\) тогда и только тогда, когда \(\vdash \neg\mathcal{A}^*\).
Доказательство. Равенство проверяется структурной индукцией. Для атома оно есть \(x = \neg\neg x\), для отрицания следует из предположения индукции, для остальных связок есть закон де Моргана в \(\mathbb{B}\). Например, для импликации при \(\vec{y} = \langle \neg x_1, \dots, \neg x_n \rangle\) имеем \[f_{\neg\mathcal{A}^* \land \mathcal{B}^*}(\vec{x}) = f_{\mathcal{A}}(\vec{y}) \land \neg f_{\mathcal{B}}(\vec{y}) = \neg\bigl(\neg f_{\mathcal{A}}(\vec{y}) \lor f_{\mathcal{B}}(\vec{y})\bigr) = \neg f_{\mathcal{A} \to \mathcal{B}}(\vec{y}).\] По теореме 9.3 выводимость \(\mathcal{A} \vdash \mathcal{B}\) означает \(f_{\mathcal{A}} \leqslant f_{\mathcal{B}}\) поточечно, а это неравенство равносильно \(f_{\mathcal{B}^*} \leqslant f_{\mathcal{A}^*}\). Выводимость \(\vdash \mathcal{A}\) означает, что \(f_{\mathcal{A}}\) тождественно равна \(1\), а это равносильно тому, что \(f_{\mathcal{A}^*}\) тождественно равна \(0\).
В терминах словаря двойственность обращает порядок: отображение \(y \mapsto \neg y\) есть изоморфизм булевой алгебры на алгебру, в которой \(\land\) и \(\lor\), \(0\) и \(1\) меняются ролями. Поэтому вместе со всяким тождеством верно двойственное; так, дистрибутивность \(x \land (y \lor z) = (x \land y) \lor (x \land z)\) влечёт \(x \lor (y \land z) = (x \lor y) \land (x \lor z)\), а теореме \(a \lor \neg a\) отвечает теорема \(\neg(a \land \neg a)\).
Предложение 11.3 (Единственность двузначной модели). Пусть на двухэлементном множестве заданы операции \(\neg, \land, \lor, \to\), по которым оценки продолжаются на формулы, и выделен один элемент. Он обозначается \(1\), второй элемент — \(0\). Если из \(x = 1\) и \(x \to y = 1\) следует \(y = 1\), а все аксиомы получают значение \(1\) при всякой оценке, то это операции из § 7.
Доказательство. Условие на Modus Ponens даёт \(1 \to 0 = 0\). Утверждение консеквента при \(x=1\) даёт \(1 \to (y \to 1) = 1\), откуда \(y \to 1 = 1\); при \(x=y=0\) оно даёт \(0 \to (0 \to 0) = 1\), откуда \(0 \to 0 = 1\). Тем самым импликация совпадает с табличной, и \(x \to y = 1\) равносильно \(x \leqslant y\). Удаление конъюнкции даёт \(x \land y \leqslant \min(x,y)\), а введение конъюнкции при \(x=y=1\) даёт \(1 \land 1 = 1\). Введение дизъюнкции даёт \(x \lor y \geqslant \max(x,y)\), а конструктивная дилемма при \(x=y=z=0\) даёт \((0 \lor 0) \to 0 = 1\), то есть \(0 \lor 0 = 0\). Закон Дунса Скота при \(x=1\), \(y=0\) даёт \(\neg 1 \to 0 = 1\), то есть \(\neg 1 = 0\). Введение отрицания при \(x=y=0\) даёт \(1 \to (1 \to \neg 0) = 1\), то есть \(\neg 0 = 1\).
Число наборов операций на \(\{0,1\}\) равно \(4 \cdot 16^3 = 16384\), и при каждом из двух выделенных значений моделью ИВ является ровно один набор. При выделенном значении \(1\) это \(\mathbb{B}\). При выделенном значении \(0\) это перевёрнутая модель: \(\neg x = 1 - x\), \(x \land y = \max(x,y)\), \(x \lor y = \min(x,y)\), \(x \to y = \min(1-x, y)\). Перестановка значений есть изоморфизм этих двух моделей. Значение формулы \(\mathcal{A}\) в перевёрнутой модели равно значению \(\mathcal{A}^*\) в \(\mathbb{B}\) при той же оценке, поэтому вычисление в перевёрнутой модели есть вычисление двойственной формулы: формула \(\mathcal{A}\) есть теорема тогда и только тогда, когда \(f_{\mathcal{A}^*}\) тождественно равна \(0\).
По теореме 9.3 теоремы суть в точности тавтологии, поэтому всякое исчисление в том же языке, корректное относительно \(\mathbb{B}\), содержится в ИВ. Расширить ИВ с сохранением замкнутости относительно подстановки можно только до противоречивого исчисления.
Предложение 11.4 (Полнота по Посту). Если \(\mathcal{A}\) не является теоремой, то при добавлении к аксиомам всех формул, получаемых из \(\mathcal{A}\) подстановками вместо атомов, выводимой становится всякая формула.
Доказательство. По теореме 9.3 существует оценка \(\varepsilon\) с \(\varepsilon(\mathcal{A})=0\). Пусть \(c\) — атом, не входящий в \(\mathcal{A}\). Формула \(c \to c\) при всякой оценке имеет значение \(1\), формула \(\neg(c \to c)\) — значение \(0\). Подстановка вместо каждого атома \(a\) формулы \(\mathcal{A}\) первой из них при \(\varepsilon(a)=1\) и второй при \(\varepsilon(a)=0\) даёт формулу \(\mathcal{A}'\), значение которой при всякой оценке равно \(\varepsilon(\mathcal{A})=0\). Поэтому \(\neg\mathcal{A}'\) есть тавтология и по теореме 9.3 теорема. В расширенном исчислении выводимы \(\mathcal{A}'\) и \(\neg\mathcal{A}'\), откуда по закону Дунса Скота выводима всякая формула.
Этот результат получен Д. Гильбертом и П. Бернайсом (1918; см. Zach, 1999) и Э. Постом (1921). Следовательно, всякое непротиворечивое исчисление в том же языке, замкнутое относительно подстановки и Modus Ponens и отличное от ИВ, не содержит некоторых его теорем. Таково положение интуиционистской логики, релевантных логик и многозначных логик, лежащих между интуиционистской и классической: их теоремы составляют часть теорем ИВ.
Резюме
Построение части I состоит из следующих этапов.
- 1.
ИВ вводится как экспликат: формальная система, замещающая обыденное рассуждение в функциях, нужных математическому доказательству. Её соответствие обыденной логике теоремой не является и теоремой о полноте не устанавливается; область её применения есть математика, включая информатику.
- 2.
Зафиксирована финитарная база метаязыка: конечный список знаков, слова и приписывание, графическое тождество \(\equiv\), предикаты, обычная логика в простых формулировках, рекурсивное построение классов слов и метапеременные.
- 3.
Заданы алфавит \(\Alf\) и слова \(\Alf^*\) с метапеременными \(\xi, \eta, \zeta\); построены предикаты \(\Atom\) и \(\Form\) с метапеременными \(a, b, c\) и \(\mathcal{A}, \mathcal{B}, \mathcal{C}\); введена подстановка \(\mathcal{A}[\mathcal{B}/a]\), сохраняющая формулы; доказана однозначность разбора.
- 4.
Аксиомы заданы схемами, предикат теоремы \(\Thm\) — замыканием относительно Modus Ponens.
- 5.
Конечные списки формул определены как слова расширенного алфавита \(\Alf'\); выводимость \(\Gamma \vdash \mathcal{A}\) задана как предикат на формулах в контексте \(\Gamma\), который может быть пустым; она сохраняется при подстановке, согласованно проведённой в контексте и в заключении.
- 6.
Сохраняются понятие конечной итерации и содержательная арифметика (замечание 2.1); утверждения о произвольных бесконечных совокупностях гипотез в базе не формулируются.
Часть II переводит исчисление на язык алгебры: формулам сопоставляются значения, а главными требованиями к классу моделей служат корректность и полнота. Функциональная модель \(B_n\) сводит формулу с \(n\) атомами к булевой функции, и всякая такая функция задаётся формулой. Булевы алгебры образуют класс моделей, относительно которого ИВ полно в силу конструкции \(\mathsf{LT}_\Gamma\); эта конструкция даёт словарь перевода, в котором выводимости отвечает порядок алгебры. Теорема Поста сводит класс к одной модели \(\mathbb{B}\), а следствие 9.4 отождествляет \(B_n\) с фрагментом алгебры Линденбаума–Тарского. В булевом кольце формулы записываются полиномами Жегалкина, и логические вычисления сводятся к арифметике по модулю \(2\). Двузначная модель единственна с точностью до перестановки значений, а эта перестановка отвечает переходу к двойственным формулам. Расширить ИВ с сохранением непротиворечивости и замкнутости относительно подстановки нельзя.
Литература
- Гильберт Д., Бернайс П. Основания математики. Т. 1: Логические исчисления и формализация арифметики. М.: Наука, 1979.
- Жегалкин И. И. О технике вычислений предложений в символической логике // Математический сборник. 1927. Т. 34, вып. 1.
- Казимиров Н. И. Архитектура математических моделей: конспект курса, подраздел «Алгебра Линденбаума–Тарского».
- Казимиров Н. И. Математика как иностранный. mathem.at/Materials/maglish_index.html
- Клини С. К. Введение в метаматематику. М.: ИЛ, 1957.
- Куайн У. В. О. Слово и объект. М.: Логос; Праксис, 2000.
- Марков А. А. Теория алгорифмов // Труды МИАН. 1954. Т. 42.
- Расёва Е., Сикорский Р. Математика метаматематики. М.: Наука, 1972.
- Carnap R. Logical Foundations of Probability. Chicago: University of Chicago Press, 1950.
- Carroll L. What the Tortoise said to Achilles // Mind. 1895. Vol. 4.
- Kreisel G. Informal rigour and completeness proofs // Problems in the Philosophy of Mathematics / ed. I. Lakatos. Amsterdam: North-Holland, 1967.
- Post E. Introduction to a general theory of elementary propositions // American Journal of Mathematics. 1921. Vol. 43.
- Zach R. Completeness before Post: Bernays, Hilbert, and the development of propositional logic // Bulletin of Symbolic Logic. 1999. Vol. 5.