Языки и исчисления

Интуиционистская пропозициональная логика


Исключим из числа аксиом закон исключенного третьего . Полученное исчисление называется интуиционистским исчислением высказываний. (Обычное исчисление высказываний называют классическим, чтобы избежать путаницы при его сравнении с интуиционистским. Вообще математические рассуждения, опирающиеся на аксиому исключенного третьего, называют "классическими", а избегающие ее — "интуиционистскими".)

Конечно, сразу же возникают естественные вопросы. Почему именно эта аксиома вызывает сомнения? Вообще-то аксиом много, и можно было бы исключить любую и смотреть, что получится без нее — но ясно, что скорее всего получится что-то странное. Как понять, какие формулы останутся теоремами без закона исключенного третьего? Раньше у исчисления высказываний была "сверхзадача" — вывести все тавтологии и только их, а теперь?

Интуиционистская логика возникла как попытка (сделанная Гейтингом) формализовать (пусть частично) методы рассуждений, практикуемые в "интуиционистской математике". Голландский математик Брауэр широко известен как автор классической (во всех смыслах) теоремы Брауэра о неподвижной точке (она утверждает, что любое непрерывное отображение многомерного шара в себя имеет неподвижную точку). Но одновременно он создал целую школу в области оснований математики — математический интуиционизм. Отчего, спрашивал Брауэр, в теории множеств возникли парадоксы? Можно считать, что это оттого, что мы стали рассуждать о каких-то уж очень абстрактных объектах, которые существуют лишь в нашей (порой противоречивой) фантазии, так что следует проявлять осторожность и не подходить к опасной черте. Но Брауэр пошел дальше, говоря, что противоречия лишь симптом болезни, а надо устранить ее причину. Причину он видел в том, что математические рассуждения и понятия утратили интуитивный смысл, и нужно вернуться к основам и пересмотреть смысл самих логических связок.

Что мы имеем в виду (или должны иметь в виду), говоря о том, что мы установили, что " или "? Это значит, по Брауэру, что либо мы установили , либо установили . Когда мы устанавливаем, что " и ", это значит, что мы установили и , и . "Если , то " означает, что мы располагаем каким-то общим рассуждением, которое позволит нам установить , как только кто-то установит нам . Отрицание означает, что мы располагаем рассуждением, которое приводит к противоречию предположение, что установлено. (Как с точки зрения интуиционизма, так и с классической точки зрения, во всех смыслах эквивалентно , где — заведомо ложное утверждение. Можно было бы вообще не использовать отрицания, а иметь константу — это не очень привычно, но технически удобно.)

Интуиционизм отвергает идею о том, что все высказывания делятся на истинные и ложные (пусть неизвестным нам образом). С этой точки зрения закон исключенного третьего совершенно безоснователен: означает, что для произвольного утверждения мы можем установить либо , либо его отрицание (то есть объяснить, почему в принципе не может быть установлено) — а почему, собственно?

Обычно, говоря об интуиционизме, приводят следующий пример рассуждения, неприемлемого с точки зрения интуиционизма. Докажем, что существуют иррациональные числа и , для которых рационально. В самом деле, рассмотрим два случая. Если рационально, то можно положить . Если же иррационально, то положим и ; легко проверить, что . Интуиционист скажет, что это рассуждение некорректно: доказать существование чего-то означает построить этот объект, а мы так и не построили чисел и , поскольку не установили, какой из двух случаев имеет место. (Заметим в скобках, что специалисты по алгебраической теории чисел знают, что

иррационально и даже трансцендентно. Кроме того, не нужно быть специалистом, чтобы заметить, что можно положить и .) Этот пример можно критиковать и с другой точки зрения, говоря, что само понятие действительного числа не является интуитивно ясным и требует обоснования.

Вообще интуиция — дело тонкое: если долго рассуждать, скажем, о действительных числах, то начинает казаться, что они в каком-то смысле существуют независимо от наших рассуждений. Именно поэтому психологически оправдан вопрос о том, скажем, как обстоят дела с континуум-гипотезой "на самом деле": существует ли несчетное множество действительных чисел, не равномощное всем действительным числам, или не существует?

Мы не будем говорить о философских предпосылках интуиционизма подробно. Вкратце упрощенная история вопроса такова. Брауэр наметил планы переустройства математики на интуиционистских принципах и отстаивал их настолько горячо, что однажды Гильберт в раздражении заметил: отменить закон исключенного третьего — это все равно что отнять у астрономов телескоп или запретить боксерам пользоваться кулаками. Но, продолжал он, никто не может изгнать математиков из рая, который создал Кантор.

В планы Брауэра не входила формализация интуиционистской логики и математики, скорее наоборот. Тем не менее анализ принципов интуиционизма пошел именно по этому пути, когда Гейтинг стал изучать пропозициональную логику без закона исключенного третьего. Различные спорные интуиционистские принципы стали предметом изучения с точки зрения формальной логики; были построены интуиционистские варианты формальной арифметики, теории множеств, логики предикатов, а также генценовские варианты интуиционистских систем. Были предложены различные интерпретации интуиционистской логики. Колмогоров предложил трактовать ее как "логику задач", Клини предложил понятие "реализуемости", использующее теорию алгоритмов для толкования формул; были предложены топологические модели для интуиционистской логики и т. д. В СССР знамя Брауэра подхватила школа Маркова, написав на нем, впрочем, "конструктивизм" вместо идеологически сомнительного "интуиционионизма" и более последовательно ограничиваясь конечными объектами. Крипке в 1960-е годы предложил некоторую семантику (определение истинности), согласованную с интуиционистским исчислением высказываний и весьма естественную (даже странно, что ее не придумали раньше); замечательным образом оказалось, что она в некотором смысле близка к методу форсинга, который примерно в это же время придумал Коэн, чтобы доказать независимость аксиомы выбора и континуум-гипотезы в теории множеств.

Возвращаясь к интуиционистскому исчислению высказываний, приведем несколько выводимых формул.

  • Чтобы понять смысл формулы , вспомним, что отрицание можно толковать как , где — заведомо ложное утверждение. Эта формула говорит, что если из следует , а из следует заведомо ложное утверждение, то из следует заведомо ложное утверждение (частный случай транзитивности отношения следования). Вывод ее не использует закона исключенного третьего. В самом деле, по лемме о дедукции (доказательство которой остается тем же и для интуиционистского исчисления высказываний) достаточно доказать, что из и выводится . Для этого, в свою очередь, достаточно доказать, что из , и

    выводятся две противоречащие друг другу формулы (что очевидно: это формулы

    и ).

  • Чтобы вывести формулу , надо показать, что из

    выводится , для чего достаточно из и

    вывести две противоречащие друг другу формулы (что тривиально — годятся сами формулы и ).

  • Формула получается из двух предыдущих: положим равным в первой из них.
  • Формула , с другой стороны, есть частный случай второй формулы, так что три отрицания равносильны одному.
  • Коммутативность и ассоциативность операций

    и , так же как и два свойства дистрибутивности, не опирались на закон исключенного третьего.

  • По-прежнему равносильно (импликации в обе стороны, связывающие эти формулы, выводимы в интуиционистском исчислении высказываний).
  • Взяв в качестве в предыдущих формулах, мы видим, что один из законов Де Моргана (а именно, закон ) не опирается на закон исключенного третьего (что легко проверить и непосредственно).
  • Формулу сохранившийся закон де Моргана позволяет переписать в виде , и нужно лишь вывести из две противоположные формулы, что очевидно.

31. Провести подробно доказательство выводимости в интуиционистском исчислении высказываний всех перечисленных формул.

С другой стороны, многие законы классической логики перестают быть выводимыми без закона исключенного третьего. Таковы, например, формулы

Мы пишем здесь переменные и , а не произвольные формулы, поскольку результат подстановки некоторых формул вместо и может быть выводимой формулой. Например, если вместо в первую из перечисленных формул подставить формулу , то получится выводимая формула .

Довольно ясно, что эти формулы не согласуются с интуиционистским подходом. Например, в предпоследней формуле говорится, что если мы опровергли предположение , то мы можем указать на одно из предположений и и предъявить его опровержение. Вряд ли такой переход можно считать обоснованным с интуиционистской точки зрения. Но, разумеется, формальный вопрос о выводимости требует формального ответа.

Начнем с закона исключенного третьего.

Теорема 24.Формула не выводима в интуиционистской логике.

В классической логике каждая пропозициональная переменная может принимать два значения — истина (И) и ложь (Л). В зависимости от значений переменных каждой формуле также приписывается значение И или Л. Расширим множество истинностных значений, добавив новое значение Н (если угодно, можно считать это сокращением слова "неизвестно"). Мы отождествляли И с единицей, а Л — с нулем, так что логично отождествить Н с числом .

Мы докажем, что интуиционистски выводимые формулы всегда принимают значение И, а формула не такова, и потому не выводима.

Чтобы определить значения формул в трехзначной логике, необходимо задать таблицы истинности для всех пропозициональных связок. Конъюнкцию определим как минимум из двух значений (так что, например, , а ), а дизъюнкцию — как максимум. Отрицание действует так: , , . (Последнее может показаться странным: почему бы не считать, что ? Оказывается, так нельзя — например, потому, что тогда формула , которая выводима в интуиционистской логике, будет иметь значение при .)

Сложнее всего определение истинности для импликации. Мы полагаем, что

для любого истинностного значения , а также что

Назовем формулу -тавтологией, если она принимает значение И при любых значениях переменных из множества . Теперь надо проверить две вещи: (1) все аксиомы интуиционистского исчисления являются -тавтологиями; (2) если посылка импликации и вся импликация являются - тавтологиями, то и заключение тоже является -тавтологией. Второе сразу ясно из определения импликации, а первое надо аккуратно проверять, составив таблицы для всех аксиом. Мы не будем этого подробно делать, поскольку это чисто механическая проверка и поскольку чуть позже мы сможем вывести это из более общего утверждения.

Следовательно, всякая интуиционистски выводимая формула является -тавтологией. Теперь заметим, что формула



принимает значение Н при и потому не является -тавтологией — значит, невыводима.

32. Покажите, что всякая -тавтология является тавтологией в обычном смысле.

Использованный нами прием годится не всегда. Например, интуиционистски невыводимая формула

является -тавтологией, поскольку (согласно нашему определению) формула может принимать только значения И и Л.

33. Какие из перечисленных нами интуиционистски невыводимых формул являются -тавтологиями?

Более общий способ установления недоказуемости (невыводимости) различных формул доставляют шкалы Крипке (или модели Крипке, как еще говорят).

Чтобы задать шкалу Крипке, нужно:

  • указать частично упорядоченное множество , называемое множеством миров;
  • для каждого мира указать, какие из пропозициональных переменных считаются истинными в этом мире (остальные переменные считаются ложными в этом мире). Если переменная истинна в мире , мы пишем .

При этом требуется, чтобы было выполнено следующее: если и , то (область истинности любой переменной наследственна вверх).

Когда шкала задана, можно определить истинность любой формулы (в данном мире) индукцией по построению формулы. Мы пишем , если в мире истинна формула . Вот индуктивное определение:

  • , если и ;
  • , если или ;
  • , если в любом мире , в котором истинна формула , истинна также и формула ;
  • , если ни в каком мире

    формула не является истинной.

Формула, не являющаяся истинной (в данном мире), называется ложной (в нем).

Определение истинности для отрицания, как легко проверить, согласовано с пониманием как , где — тождественно ложная (во всех мирах) формула.

Именно определение импликации (и отрицания) использует порядок на множестве миров. Если формула содержит лишь конъюнкции и дизъюнкции, то ее истинность по существу определяется отдельно в каждом мире.

Индукцией по построению формулы легко проверить, что если она истинна в каком-то мире, то истинна и во всех больших мирах. В самом деле, пересечение и объединение двух наследственных вверх множеств также обладает этим свойством, так что для случая конъюнкции и дизъюнкции можно сослаться на предположение индукции. А для импликации даже и этого не нужно, достаточно посмотреть на определение.

Философский смысл шкал Крипке иногда объясняют так. Пусть

есть множество возможных состояний цивилизации (миров);

означает, что мир может получиться из мира в результате развития цивилизации. Утверждение означает, что в мире установлено, что высказывание истинно. (При этом оно останется истинным и при дальнейшем развитии цивилизации.) Истинность в мире означает, что ни при каком развитии цивилизации из состояния высказывание

не станет истинным.

Определение истинности отрицания в шкалах Крипке предвосхитил Пушкин, когда писал "нет правды на земле. Но правды нет и выше," (Моцарт и Сальери).

34.Во что превращается определение истинности в шкале Крипке, если в ней только один мир? если в ней никакие два мира не сравнимы?

Теорема 25 (корректность интуиционистского исчисления высказываний относительно шкал Крипке).

Формула, выводимая в интуиционистском исчислении высказываний, истинна во всех мирах всех шкал Крипке.

Надо проверить, что все аксиомы истинны во всех мирах, а также что правило modus ponens сохраняет это свойство. Второе очевидно: если истинна во всех мирах и истинна во всех мирах, то по определению истинности импликации будет истинна во всех мирах.

Осталось проверить истинность всех аксиом. Чтобы установить, что импликация истинна во всех мирах, надо проверить, что в тех мирах, где истинна формула , истинна и формула . Для первой аксиомы : если формула истинна в некотором мире, то в силу монотонности она истинна и выше, так что также истинна.

Проверим вторую аксиому . Пусть . Надо убедиться, что . Это означает, что если и , то . Последнее, в свою очередь, значит, что если и , то . Но в силу монотонности мы знаем, что и . Поэтому из следует , , и, наконец, , что и требовалось.

Остальные аксиомы проверяются еще проще.

Таким образом, чтобы доказать, что некоторая формула не выводима в интуиционистском исчислении высказываний, достаточно предъявить шкалу Крипке, в одном из миров которой она ложна.

35. Покажите, что в этом случае есть шкала, в которой среди миров есть наименьший и в нем формула ложна.

Для формулы такая шкала строится легко. Возьмем два мира, первый меньше второго. Пусть истинна только во втором мире. Тогда не будет истинна нигде, а будет истинна только во втором мире.

На самом деле это доказательство в сущности совпадает с приведенным выше (с трехзначной логикой). В самом деле, в этой шкале для формулы есть три возможности: она истинна в обоих мирах, она истинна только во втором мире, или она не истинна ни в одном из миров. Эти три возможности соответствуют трем значениям И, Н и Л в рассмотренной нами трехзначной интерпретации. Легко проверить, что таблицы операций как раз соответствуют определению истинности в модели Крипке.

Теперь мы можем установить, что все перечисленные выше формулы невыводимы в интуиционистском исчислении высказываний. Для формулы годится та же самая шкала ( истинно только в большем мире). Она же годится для формулы , если истинно в обоих мирах, а — только в большем. Для трех оставшихся формул можно рассмотреть шкалы с тремя мирами: начальным миром , из которого можно попасть в и в ; миры и не сравнимы. Если формула истинна только в мире , то формула истинна только в мире , a истинна только в мире , так что в мире обе формулы и ложны и дизъюнкция ложна. Чтобы построить контрмодель для формулы , будем считать, что истинна только в мире , а истинна только в мире . Та же шкала годится и для формулы .

Оказывается, что этот прием универсален, как показывает следующая теорема.

Теорема 26 (полноты интуиционистского исчисления высказываний относительно шкал Крипке).

Для любой невыводимой в интуиционистском исчислении формулы можно подобрать шкалу Крипке, в которой ложна в некотором мире.

Напомним схему доказательства полноты классического исчисления высказываний, приведенного в разделе "Второе доказательство теоремы о полноте". Пусть формула невыводима. Мы хотим найти значения переменных, при которых формула ложна, то есть формула

истинна. Само по себе требование истинности не определяет значения переменных однозначно. Чтобы избавиться от произвола, мы расширяем непротиворечивое множество до полного множества и объявляем истинными те переменные, которые входят в .

Для интуиционистского случая в этой схеме требуются некоторые изменения. Раньше ложность формулы была равносильна истинности формулы . В шкалах Крипке это уже не так, и мы будем отдельно говорить об истинных и ложных (не истинных) формулах.

Пусть и — конечные множества пропозициональных формул. Будем говорить, что пара совместна, если существует шкала Крипке и ее мир, в котором все формулы из

истинны, а все формулы из ложны. Будем говорить, что пара противоречива, если в интуиционистском исчислении высказываний выводима формула

где — формулы множества , а — формулы множества . (Без ограничения общности можно считать, что перечислены все формулы множеств и , поскольку пропущенные формулы можно добавить, не нарушив выводимость.)

Пример: если одна и та же формула входит в обе части пары, то такая пара противоречива.

Легко проверить, что противоречивая пара не может быть совместна. В самом деле, если в некотором мире все формулы из истинны, а все формулы из ложны, то посылка импликации в этом мире истинна, а заключение ложно. Поэтому импликация ложна, что противоречит ее выводимости (теорема о корректности).

Мы докажем, что верно и обратное: всякая непротиворечивая пара совместна. В частности, когда состоит из единственной формулы, получается утверждение теоремы о полноте. (Мы предполагаем, как это обычно делается, что конъюнкция пустого множества формул есть тождественно истинная формула, а дизъюнкция — тождественно ложная. Поэтому противоречивость пары означает выводимость формулы . Заметим кстати, что противоречивость пары означает выводимость формулы .)

Итак, пусть имеется непротиворечивая пара . Как доказать ее совместность? Как и в классическом случае, мы устраним произвол, расширив и . Основным средством здесь является такая лемма.

Лемма 1. Пусть — непротиворечивая пара, а — произвольная формула. Тогда хотя бы одна из пар и непротиворечива.

Доказательство леммы 1. Пусть обе пары с добавленным

противоречивы. Надо доказать, что противоречива исходная пара. Другими словами, надо показать, что если в интуиционистском исчислении высказываний выводимы формулы

то выводима и формула (для простоты мы отождествляем множества и с конъюнкцией и дизъюнкцией их элементов и считаем и формулами).

В самом деле, по лемме о дедукции достаточно доказать, что . Для этого достаточно установить, что

поскольку в предположении у нас уже есть. Для этого, в свою очередь, достаточно установить, что и . Первое очевидно (и посылка не нужна), второе равносильно выводимости формулы , которая нам дана по условию леммы. Лемма 1 доказана.

Проведенное рассуждение, как говорят, устанавливает допустимость (в интуиционистской логике) правила сечения, позволяющего "иссечь" формулу из формул и и получить формулу .

Возвращаясь к доказательству теоремы, рассмотрим произвольную непротиворечивую пару . Рассматривая по очереди различные формулы , мы будем добавлять их к левой или правой части. Чтобы этот процесс ("пополнение") был конечным, мы ограничимся формулами из некоторого множества.

Фиксируем некоторое конечное множество формул , которое содержит все формулы из и замкнуто относительно перехода к подформулам (если формула входит в , то все ее подформулы входят в ). Например, можно включить в все подформулы всех формул из и из .

Пару , у которой , будем называть полной, если она непротиворечива и любая формула из

входит либо в , либо в (то есть ). Заметим, что из непротиворечивости следует, что , так что полная пара задает разбиение на две части. (Более точно полные пары следовало бы называть "полными относительно ", но у нас множество

фиксировано.)

Лемма 2. Исходная пара может быть расширена до полной: существует полная пара , для которой , .

Доказательство очевидно: применяем по очереди лемму 1 ко всем формулам из .

Точно так же любую непротиворечивую пару, составленную из формул множества , можно расширить до полной. (Это замечание нам впоследствии понадобится.)

Для завершения доказательства теоремы 26. нам осталось показать, что всякая полная пара совместна (существует шкала и мир, в котором формулы из истинны, а формулы из ложны). В отличие от классического случая построение будет использовать не только пару , но и все полные пары.

Шкала Крипке строится так. Мирами будут полные пары (то есть всевозможные непротиворечивые разбиения множества на левую и правую части). Истинность переменных определяется естественным образом: всякая переменная , входящая в одну из формул множества , сама принадлежит множеству

(замкнутость относительно подформул); если входит в левую часть полной пары , то истинна в мире , если в правую — то ложна. (Впоследствии это свойство мы распространим на все формулы: любая формула из окажется истинной в мире , а любая формула из — ложной.)

Осталось определить порядок на множестве пар. Считаем, что , если . (Такое определение не удивительно, если вспомнить, что истинность формул наследуется вверх.)

Лемма 3. В построенной шкале в мире истинны все формулы из и ложны все формулы из .

Доказательство леммы 3 проводится индукцией по построению формул. Для переменных она верна по определению истинности. Пусть некоторая формула из не является переменной. Тогда она есть конъюнкция, дизъюнкция, импликация или отрицание и для ее частей утверждение леммы верно по предположению индукции. Рассмотрим все случаи по очереди, начав с конъюнкции и дизъюнкции (истинность которых не зависит от других миров).

() Пусть формула входит в . Тогда формулы и не могут входить в , иначе пара была бы противоречивой (из выводится и ). Значит, и входят в (полнота), поэтому они истинны (предположение индукции), и потому истинна (определение истинности).

() Пусть формула входит в . Могут ли обе формулы и входить в ? Нет, так как в этом случае пара была бы противоречивой. Значит, хотя бы одна из формул входит в , тогда по предположению индукции она ложна, и потому формула ложна в мире .

() Если формула входит в , то формулы и не могут одновременно входить в , и потому хотя бы одна из них истинна, так что и вся формула истинна.

() Если формула входит в , то формулы и не могут входить в , поэтому обе они ложны и формула ложна.

() Пусть формула входит в . Проверим, что она истинна в . Это значит, что в любом мире , который выше нашего (то есть ) и в котором истинна формула , должна быть истинна и формула . В самом деле, если истинна в , то она входит в (предположение индукции). С другой стороны, и входит в , поскольку . Теперь ясно, что формула не может входить в , так как в этом случае пара была бы противоречивой (из и выводится ). Значит,

входит в и потому истинна в по предположению индукции.

() Это наиболее интересный случай, где нам снова потребуется пополнение. Пусть формула входит в . Мы должны доказать, что она ложна в мире . Согласно определению, это означает, что найдется мир , для которого и в котором формула

истинна, а формула ложна (то есть и , согласно предположению индукции). Как найти такой мир? Рассмотрим пару . Эта пара непротиворечива. В самом деле, если бы формула была бы выводима, то и формула была бы выводима (лемма о дедукции), и потому пара была бы противоречива. Теперь можно расширить непротиворечивую пару

до полной пары , которая и будет искомым миром.

Отрицание рассматривается аналогично импликации (как мы уже говорили, можно вместо отрицания ввести тождественную ложь и вообще его не рассматривать).

() Пусть формула входит в . Надо доказать, что формула ложна в любом мире

выше мира . Формула не может входить в , так как в входит формула (напомним, что ), а из

выводится любая формула. Значит, входит в и по индуктивному предположению формула ложна в .

( Пусть формула входит в . В этом случае пара непротиворечива (если из и выводится противоречие, то из выводится ). Расширив ее до полной, получаем высший мир , в котором формула истинна (по индуктивному предположению). Следовательно, формула ложна в мире .

Лемма 3 доказана. Она завершает доказательство теоремы 26. Напомним еще раз его схему. Пусть формула не выводима в интуиционистском исчислении высказываний. Тогда пара

непротиворечива. Фиксируем множество всех подформул формулы . Расширим нашу непротиворечивую пару до полной (относительно ). Эта полная пара будет одним из миров шкалы Крипке (в которой мирами являются полные пары). Именно в этом мире и будет ложной формула .

36. Покажите, что если формулы и ложны в некоторых мирах некоторых шкал Крипке, то можно построить шкалу Крипке и мир в ней, для которого формула будет ложной. (Указание: соединим шкалы, в которых ложны формулы

и , в одну, добавив новый мир, который меньше миров, где и ложны.)

Из этой задачи и из теоремы о полноте вытекает такое следствие: если дизъюнкция двух формул выводима в интуиционистском исчислении высказываний, то хотя бы одна из формул тоже выводима. Это свойство выполнено для многих интуиционистских исчислений и соответствует начальной идее: доказать

означает доказать одну из формул или . Подобные свойства можно доказывать и синтаксически, используя генценовские варианты интуиционистских исчислений.

37. (а) Покажите, что формула

выводима в интуиционистском исчислении высказываний. (б) Покажите, что если формулы и

выводимы в интуиционистском исчислении высказываний, то и формула выводима в интуиционистском исчислении высказываний. (в) Докажите, что если формула выводима в классическом исчислении высказываний, то формула выводима в интуиционистском исчислении высказываний (теорема Гливенко) (г) Покажите, что для формул, содержащих лишь конъюнкцию и отрицание, разницы между классическим и интуиционистским исчислениями нет: из классической выводимости следует интуиционистская (теорема Геделя).

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


Содержание раздела