Дискретно-непрерывная математика (стр. 60 )

(1) в каждой модели для Int:и

. (2) если то формула не выводима в Int

Метод доказательства состоит в конструировании для каждого натурального числа п > 1 недоказуемой в Int формулы А такой, что А общезначима во всех п-значных моделях Int. В качестве такой формулы Гёдель предлагает следующую конструкцию. Из пропо­зициональных переменных образуются всевозможные импликации вида , которые затем соединяются в произволь­ном порядке знаками дизъюнкции. Полученную формулу обозна­чим посредством Dп :

Допустим, что существует п-значная матрица которая, яв­ляется характеристической для Int. Заметим, что формула Dп+1 общезначима в Это следует из того, что в матрице только п элементов, а в Dп+1 имеется (п+1) переменных. Поэтому найдутся такие что Тогда (см.

выше свойство (1)). Таким образом, формула Dп+1 общезначима. Так как является по допущению характеристической матрицей, то тогда Dп+1 выводима в Int. Но поскольку Int обладает дизъюнк­тивным свойством, тогда в Dп+1 должна найтись и выводимая им­пликация где что противоречит (2).

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

Напомним, что С. Яськовский показал \Jaskowski 1936], что многозначной семантикой для Int является бесконечнозначная по­следовательность конечнозначных матриц (см. выше раздел 4.3.2). Отсюда следует разрешимость Int. Это является классическим

примером интересного феномена: бесконечнозначная логика фи­нитно аппроксимируется последовательностью конечнозначных логик. Развитие этого результата для других логик см. в [Baaz and Zach 1994] и [Gottwald 2001. Нельзя не отметить следую­щий результат А. Вроньского: никакая счетнозначная матрица не является адекватной для доказательства строгой полноты Int [Wronski 1974]. Таким образом, логика Int является существенно континуальной, в отличие от С2, которая является существенно двузначной.

В [McKinsey 1939] было доказано, что, в отличие от С2, опера­ции в Int невыразимы друг через друга. Таким образом, в отличие от в Int нельзя взять за исходные связки отрицание и импликацию. Однако для Int найдены аналоги штриха Шеффера (см. [Кузнецов 1965]). Также отметим, что один из законов Де Мор­гана не имеет места в Int, а именно:

Заметим, что предикатная Int в ряде случаев отличается от классической логики. Например, хотя оба исчисления неразреши­мы, интуиционистская логика одноместных предикатов тоже не­разрешима в отличие от классического одноместного исчисления предикатов.

8.2.2.1. Философская интерпретация Int (семантика возможных миров)

В 1954 г. появляется концепция реляционной модели у А. Прайора, а в 1957 г. в работах С. Кангера и Я. Хинтикки, пока С. Крипке не выразил эту идею в 1959 г., а затем в 1963 г. в наиболее ясной и за­конченной форме для модальных логик (см. [Крипке 1974]). Шка­лой Крипке (структурой, фреймом) называется пара <W, R>, где W — множество возможных миров (точки, моменты, вынуждающие условия), a R — бинарное отношение достижимости на мирах.

В [Grzegorchyk 1964] и [Kripke 1965] появилась семантика воз­можных миров для Int. Мы будем следовать работе М. Фиттинга {Fitting 1969]. Пусть дана некоторая модель Крипке где

W — непустое множество возможных миров; R — отношение час­тичного порядка (рефлексивно и транзитивно) на W, и е — функция оценки формул на подмножествах W. Определим отношение ме­жду элементамии формулами Int, где читается «в мире w имеет место формула А»:

1. т. т.т., когда для всех z таких, что

2. т. т.т., когда

3. т. т.т., когда

4. т. т.т., когда для всех z таких, что wRz, если

то

5. т. т.т., когда для всех z таких, что wRz, не имеет места

В модели Крипке имеет место т. т.т., когда для

всех Относительно этой семантики доказывается

полнота исчисления Int.

Основная философская проблема: что это за сущности такие -возможные миры! Первая философская работа по интерпретации Int (истинности в Int) принадлежит А. Гжегорчйку [Grzegorchyk 1964]. Конечно, такого рода интерпретации не лишёны элемента произвольности. В несколько общем виде философская интерпре­тация Int обсуждается в [ Щрагалин 1979]. Будем интерпре­тировать миры как возможные состояния знания некоторого по­знающего субъекта. Субъект видит, что в настоящий момент он находится в состоянии w - это его «реальный мир». Если то состояние z можно рассматривать как более позднее, как результат развития w. Соответственно, информация, приписанная z, является расширением информации w. Мы считаем, что со временем най­денная информация не теряется, а может лишь приобретаться. Это выражается семантической леммой, имеющей место в Int:

Для любой т. т.т., когда для всех z

таких, что

Индукцией по построению формулы А легко выяснить, если она истинна в каком-то мире, то истинна и во всех достижимых мирах (благодаря отношению R). М. Фиттинг, у которого миры тоже есть «состояния знания», интерпретирует данную лемму так: если в на­стоящее время мы знаем, что А истинно, то в любое позднее время мы все еще знаем, что А истинно [Fitting 1969]. [Dummett 1977] моменты из W есть «состояния информации» (в этой работе он дает интуиционистски приемлемое доказательст­во полноты Int, при этом по существу используя конечные деревья Крипке). Гораздо дальше пошли и А. Шень [Вере­щагин и Шенъ 2008]: W есть множество возможных состояний ци­вилизаций; означает, что мир z может получиться из мира w в результате развития цивилизации. Истинность в мире w озна­чает, что ни при каком развитии цивилизации из состояния w вы­сказывание А не станет истинным.

8.2.3. Суперинтуиционистские логики

Суперинтуиционистской логикой (si-логикой) называется логика, полученная посредством расширения Int аксиомами в этом же язы­ке. Члены последовательности конечнозначных логик Гёделя Gn являются si - логиками (см. раздел 5.1.7), самой известной из кото­рых является трехзначная логика Рейтинга G3. Добавление к Int слабого закона исключенного третьего образует si-логику КС (логика Янкова). Еще одной хорошо известной si - логикой является расширение Int посредством аксиомы

(логика Скотта SL). Имеют­ся обзоры по пропозициональным si - логикам [Hosoi and Ono 1973] и по предикатным si - логикам [Опо 1987].