5 - Генценовские формальные системы. Исчисление GV. Исчисление GP (Конспект лекций), страница 2

Если в исчислении GVсеквенция Γ > ∆ выводима, то существует вывод этой секвенции, в котором не используетсяправило сечения.ÌÃÒÓÌÃÒÓПосле этого все восемь логических правил исчисления GV окажутся сбаланисрованными: выводимость секвенций в числителе правила будет равносильна выводимости секвенции в знаменателе (речь пока не идет о том, как строится такой вывод).С введением этих усиленных правил вывод превращается в простую разборку формул антецедента и сукцедента. Если, например, в антецеденте стоит формула X = U → W , X = U ∧ W ,X = U ∨ W или X = ¬U , то применением соответствующего правила в антецеденте формула X заменяется подформулами U и W .

Повторяя этот процесс, мы в результате придем кдереву, у которого в листьях имеются лишь элементарные формулы, т.е. пропозициональныепеременные. Секвенция Γ > ∆, у которой все формулы элементарные является истинной в томи только в том случае, когда списки Γ и ∆ имеют общую переменную. Выводимость исходнойсеквенции в свете вышесказанного означает выводимость всех таких элементарных секвенций,т.е. во всех элементарных секвенциях есть одинаковые переменные и слева, и справа. Но такиесеквенции — простейшее следствие соответствующей аксиомы, получаемое с помощью правилаутончения. Описанный вывод не использует, как видно правила сечения — только три первыепары структурных правил.Итак, нами, по существу доказан следующий факт.ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ58ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ59ÔÍ-12Пример 5.5.

Построим в GP вывод секвенции > ∀x∀y(X(x) ∧ Y (y)) → Yxy :> ∀x∀y(X(x) ∧ Y (y)) → Yxy∀x∀y(X(x) ∧ Y (y)) > Yxy∀x∀y(X(x) ∧ Y (y)) > ∀yY (y)∀yY (y) > Yxy∀x∀y(X(x) ∧ Y (y)) > Y (y)Yxy > YxyÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-125. Генценовские формальныесистемы∀y(X(x) ∧ Y (y)) > Y (y)X(x) ∧ Y (y) > Y (y)В этом выводе использовано правило сечения. Однако вспомним исчисление GV , в которомправило сечения можно не использовать. Покажем, как можно построить вывод той же секвенции без правила сечения. Первый шаг, как и в предыдущем выводе (введение импликациив сукцеденте), а затем последовательно разбираем формулы (использована чистая“ перемен”ная z):> ∀x∀y(X(x) ∧ Y (y)) → YxyÔÍ-12ÔÍ-12Y (y) > Y (y)Остановимся на связи между теориями P и GP .

Естественно рассчитывать, что установленная связь между двумя исчислениями высказываний в каком-то виде сохранится и дляисчисления предикатов.Теорема 5.4. Пусть Γ — список формул, а X — формула в логико-математическом языке.Тогда если Γ ` X в исчислении P , то ` (Γ > X) в исчислении GP . В частности, если ` X висчислении P , то ` ( > X) в исчислении GP .Γ > ∀xX∀xX > XtxXtx > XtxÔÍ-12J Это утверждение доказывается так же, как и аналогичное утверждение для исчислений высказываний.

Более того, высказывательное“ утверждение — составная часть предикатного.”Нам необходимо дать интерпретацию правил естественного вывода в рамках правил выводагенценовского исчисления. Для правил исчисления высказываний такая интерпретация уже дана. Остается разобраться с четырьмя дополнительными правилами, связанными с кванторами.Три из этих правил — очевидные следствия трех правил вывода генценовской формальной сиΓ ` ∀xXстемы. Остановимся на последнем правиле. Для него строим дерево вывода на основеΓ ` Xtxправила сечения:Γ > XtxÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12Yxy > YxyКак видим, что действует в основном тот же принцип, что и в исчислении высказываний, но несколько усложненный сменой переменных при снятии кванторов.

Здесь использовано свойство(Xzx )zx = X(x) (обратимость правильной подстановки переменной вместо переменной).ÌÃÒÓÌÃÒÓXzx ∧ Yxy > YxyÔÍ-12ÔÍ-12∀y(Xzx ∧ Y (y)) > YxyÌÃÒÓÌÃÒÓ∀x∀y(X(x) ∧ Y (y)) > YxyÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.Учитывая, что все правила естественного вывода могут быть реализованы в рамках правилвывода исчисления GP , делаем заключение о верности утверждения теоремы. IТеорема 5.5.

Пусть Γ — список формул, а X — формула в логико-математическом языке.Тогда если ` (Γ > X) в исчислении GP , то Γ ` X в исчислении P . В частности, если ` ( > X)в исчислении GP , то ` X в исчислении P .1Но здесь есть один изъян: надо еще доказать, что выводимость любой тавтологии можно обосновать средствами правил естественного вывода.ÔÍ-12ÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12J Доказательство можно построить на тех же принципах, что и доказательство аналогичнойтеоремы1 5.2.

Можно показать, что если в исчислении GP выводима секвенция Γ > ∆, гдеΓ = X1 , X2 , . . . , Xn , ∆ = Y1 , Y2 , . . . , Ym , то формула X1 ∧ X2 ∧ . . . ∧ Xn → Y1 ∧ Y2 ∧ . . . ∧ Ym являетсятавтологией. В частности, при m = 1 из выводимости в GP секвенции Γ > Y следует, чтоX1 ∧ X2 ∧ . . . ∧ Xn → Y есть тавтология и, значит, выводима в P . Но тогда имеет местовыводимость X1 ∧ X2 ∧ . . .

∧ Xn ` Y , откуда получаем выводимость Γ ` Y . IÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ60ÌÃÒÓÌÃÒÓ151517223. Алгебра предикатов3.1. Предикаты и кванторы . . . . . . . . . . .3.2. Логико-математические языки . . . . . . .3.3. Переименования и подстановки . . . . . .3.4. Семантика логико-математического языка3.5. Логические законы . . .

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

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

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

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

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

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