2 - Исчисление высказываний. Основные положения теории N. Правила естественного вывода. Глобальные свойства теории N (Конспект лекций), страница 4

выводимой в теории N . Указанная процедура выполняется за конечное число алгебраических операций и даетоднозначный ответ, выводима формула или нет. В этом смысле теория N является разрешимойтеорией.Еще один вопрос, связанный с построением формальной теории — независимость аксиом.Аксиома формальной теории не зависит от остальных аксиом этой теории, если эта аксиомане является выводимой формулой в теории, которая получается из исходной удалением указанной аксиомы. Если ни одна из аксиом формальной теории не является логическим следствиемостальных, то говорят о независимой системе аксиом.Система аксиом теории N является независимой в том смысле, что удалив одну из схемаксиом теории, мы не сможем вывести ни одну из формул, получаемой в рамках этой схемы аксиом.

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

Придание смысла символам формальной теории называют интерпретацией этой теории. В данном случаемножество всех высказываний как область изменения переменных и естественный логическийсмысл символов операций — это одна из возможных интерпретаций исчисления N .Интерпретация формальной теории строится в рамках какой-либо другой математическойтеории. Надежность интепретации определяется надежностью той теории, в которой интепретируется исчисление. Так, суждения о непротиворечивости, полноте и разрешимости исчисления N получены в рамках так называемой теории булевых функций, т.е. теории функций собластью изменения переменных и функций 0 и 1. В этом смысле подобные суждения носятотносительный характер.

В математике считают абсолютно надежными теории, связанные сконечными множествами. В этом смысле утверждения о непротиворечивости, полноте и разрешимости исчисления N являются абсолютными. Утверждение о независимости системы аксиомтоже будет абсолютным, если оно будет получено на базе какой-либо конечной интерпретации.ÌÃÒÓÌÃÒÓÌÃÒÓ24ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-122. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÔÍ-12ÌÃÒÓÔÍ-1234567Интерпретируемая №ИнтерпретируемаяСхема аксиомоперацияоперацияX ∧Y →Xx∧y =y8 X →Z →(Y →Z →(X ∨Y →Z))x∨y =1X ∧Y →Yx∧y =x9X → Y → (¬Y → ¬X)¬x = xX →Y →(X →Z →(X →Y ∧Z))x∧y =010¬¬X → X¬x = 1X →Y ∨Zx∨y =z11X → ¬¬X¬x = 0Y →Y ∨Zx∨y =yСхема аксиомÌÃÒÓ№ÔÍ-12ÔÍ-12Таблица 2.1ÌÃÒÓÌÃÒÓÌÃÒÓ25ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓимеют постоянное истинностное значение 1.

Изменение интерпретации не затрагивает правилаmodus ponens, так что при удалении указанной схемы аксиом мы получаем теорию, в которойвсе выводимые формулы — тавтологии, но некоторые формулы, получаемые из указанной схемы, выводимыми не являются. Это и означает, что указанная схема аксиом не зависит отостальных.Независимость первых двух схем доказать сложнее, поскольку они касаются импликации,затрагивающей все схемы. Ответ можно найти, рассмотрев в качестве области изменения переменных множество из трех целых чисел {0, 1, 2} и выбрав следующие интерпретации операций:x ∧ y = min {x, y}, x ∨ y = max {x, y}, ¬x = 2 − x. Для импликации потребуем выполненияусловия, что x → y = n тогда и только тогда, когда x 6 y.

При поставленных условиях схемы 3, 4, 6, 7, 10, 11 будут давать формулы с тождественным значением n, а в силу условия,наложенного на импликацию, значение Y будет тождественное n при X ≡ n и X → Y ≡ n.Недоопределенность импликации можно использовать для получения нужных значений первыхдвух схем аксиом и для обеспечения тождественного значения n схем 5, 8, 9.Положим x → y = 0 при x > y.

Тогда схема X → (Y → X) будет иметь значение 0 приX = 1, Y = 2, в то время как остальные аксиомы будут давать тождественное значение 2.Действительно, в схеме 2 исключаем случай X > Y или X 6 Z, так как тогда она имеет вид0→W или W →1. Значит, Z < X 6 Y и схема имеет вид 2→(X →0→0). Но X > Z > 0, значит,X → 0 = 0 и 2 → (X → 0 → 0) = 2 → (0 → 0) = 2 → 2 = 2.

В схеме 5 исключаем случай X > Yили X > Z, когда она имеет значение 2. Но тогда X 6 min {Y, Z} и X → Y ∨ Z = 2. ПоэтомуX → Y → (X → Z → (X → Y ∧ Z)) = X → Y → (X → Z → 2) = 2. В схеме 8 исключаем случайX > Z или Y > Z. Тогда max {X, Y } 6 Z, X ∨ Y → Z = 2 и схема 8 имеет тождественноезначение 2. В схеме 9 исключаем случай X > Y . Но тогда X 6 Y , ¬Y 6 ¬X и формула имеетвид 2 → 2.Положим x → y = 1 при x > y.

Тогда схема 8 будет иметь значение 1, например, при X = 1,Y = 2, Z = 0. В схеме 1 исключаем случай Y 6 X. Тогда X < Y 6 2, а значит, X 6 1 иX → (Y → X) = X → 1 = 2. Схемы 5, 8, 9 проверяются так же, как выше. IÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-122. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓ141416213. Алгебра предикатов3.1. Предикаты и кванторы . .

. . . . . . . . .3.2. Логико-математические языки . . . . . . .3.3. Переименования и подстановки . . . . . .3.4. Семантика логико-математического языка3.5. Логические законы . . . . . . . . . . . . .3.6. Замены . . . . . . . . . . . . . . . . . . .

.3.7. Упрощение формул . . . . . . . . . . . . ........26262730333538404. Исчисление предикатов4.1. Построение теории P . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.2. Правила естественного вывода . . . . . . . . . . . . . . . . . . . . . . . .

. . . . .4.3. Глобальные свойства теории P . . . . . . . . . . . . . . . . . . . . . . . . . . . . .424243455. Генценовские формальные системы5.1. Исчисление GV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5.2. Исчисление GP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . .5252566. Примеры формальных теорий6.1. Теория групп . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.2. Формальная арифметика . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5959617. Метод резолюций7.1. Скулемовские функции . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . .7.2. Метод резолюций для исчисления высказываний . . . . . . . . . . . . . . . . . . .7.3. Метод резолюций для исчисления предикатов . . . . . . . . . . . . . . . . . . . . .66666871......................................................................................................................................................................................................................................................ÌÃÒÓ2. Исчисление высказываний2.1. Основные положения теории N .

. . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2. Правила естественного вывода . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.3. Глобальные свойства теории N . . . . . . . . . . . . . . . . . . . . . . . . . . . . .....ÔÍ-12....11359ÔÍ-12ÔÍ-121. Алгебра высказываний1.1. Введение .

. . . . . . . . . . . . . . . .1.2. Алгебра логики . . . . . . . . . . . . .1.3. Тавтологии и эквивалентность формул1.4. Функции алгебры логики . . . . . . . .ÔÍ-1275ÌÃÒÓÔÍ-12ОГЛАВЛЕНИЕÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ.