25988-1 (Логика предикатов), страница 3

Легко видеть, что формула U равносильна: (x)[P(x) (Q(x) P(x))], которая, отнесённая к полю L, равносильна : [P( ) (Q( ) P( ))] [P( ) (Q( ) P( ))] [P( ) (Q( ) P( ))] [P( ) (Q( ) P( ))].

Таким образом, представляет собой формулу, образованную только операциями алгебры высказываний над выражениями P( ) и Q( ), где i= , т.е. её можно рассматривать как формулу алгебры высказываний, у которой P( ) и Q( ) являются элементарными переменными высказываниями. Значит, ответив на вопрос о тождественной истинности , мы сможем сказать, является ли формула U тождественно истинной или нет.

является тождественно истинной в алгебре высказываний U также тождественно истинная формула на поле, содержащем элементов. Это оэначает, что U тождественно истинна.

П Р И М Е Р 2: Доказать, что формула U, отнесённая к некоторому полю L, представленная как

[(х)( Q(x)) P(x)],

является тождественно истинной.

Для этого она должна быть тождественно истинной на поле, содержащем ровно элементов. В данном случае n = 2, т.е. L можно опять определить как { a₁, a₂, a₃, a₄ }.

Применяя равносильные преобразования над U, можем заключить её равносильность формуле: (х)[( Q(x)) P(x)], которая, отнесённая к полю L, равносильна : [( Q( )) P( )] [( Q( )) P( )] [( Q( )) P( )] [( Q( )) P( )].

Легко видеть, что , как и в предыдущем примере, представляет собой формулу, образованную только операциями алгебры высказываний над выражениями P( ) и Q( ), где i= , а поэтому её можно отнести к формулам алгебры высказываний, у которой P( ) и Q( ) являются элементарными переменными высказываниями. Является ли формула тождественно истинной?

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

Таким образом, формула ( Q) P является выполнимой, следовательно, является тождественно истинной формулой в алгебре высказываний U также тождественно истинная формула на поле, содержащем элементов. Это означает, что U тождественно истинна.

§3. Поиск доказательств в натуральном интуиционистском исчислении предикатов с -символом и предикатом существования

Существуют два типа систем натурального вывода: с прямым и непрямым правилом удаления квантора существования. Прямое правило удаления квантора существования по существу формулируется с использованием языка с эпсилон-символом. Классическое исчисление предикатов с прямым правилом удаления квантора существования элегантно и является хорошей основой для организации систематической процедуры поиска доказательств. Мною была предложена процедура поиска доказательств для классического исчисления предикатов с прямым правилом удаления квантора существования [7]. А.В. Смирнов и А.Е. Новодворский [3] реализовали ее на компьютере. Хотелось бы построить интуиционистское исчисление предикатов с прямым правилом удаления квантора существования и на этой основе сформулировать алгоритм поиска доказательств. Однако на этом пути мы встречаемся с определенными трудностями. Если мы заменим классические пропозициональные правила интуиционистскими, то в результате получим логическую систему, более богатую, нежели интуиционистское исчисление предикатов. Действительно, допустим, что имеет место xA(x). По правилу удаления квантора существования получим A(xA(x)). По правилу введения импликации будем иметь xA(x)A(xA(x)). Из последней формулы по правилу введения квантора существования получаем y(xA(x)A(y)). Запишем этот вывод формально

1 xA(x) допущение

2 A(xA(x)) у; 1

3 xA(x) A(xA(x)) в; 1-2

4 y(xA(x) A(y) в; 3

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

Где в этих доказательствах неинтуиционистские шаги? Ответ, видимо, неоднозначен. В книге [5] я предлагал наложить ограничения на непрямые правила вывода: потребовать, чтобы -термы не входили в устраняемые допущения и заключение. Однако это ограничение слишком стеснительно и неэлегантно. А.Г. Драгалин [1], а затем Д. Скотт ввели другое ограничение: в правилах введения квантора существования и удаления квантора общности мы должны потребовать, чтобы вводимый или исключаемый терм был не пуст. Это более изящное решение проблемы. В настоящей статье я предлагаю формулировку интуиционистского исчисления предикатов с -символом и предикатом существования в виде субординатного вывода. Затем обсуждается проблема систематического поиска выводов в этом исчислении.

Язык интуиционистского натурального исчисления с -символом NI строится с помощью двух типов индивидных переменных: свободных - v,v1,v2,... и связанных - x,y,z,. . ., x1, x2, . . ., предикатных знаков, логических связок &,,,, знака абсурдности , предиката существования , кванторов и , -символа, скобок и запятой. Одновременной индукцией определяем понятия квазитерма и квазиформулы. Термами и формулами являются квазитермы и кваиформулы, не содержащие свободных вхождений связанных переменных. Под подстановкой вместо свободной переменной v квазитерма t в квазиформулу или квазитерм имеется в виду замещение каждого вхождения свободной переменной v в квазитерм или квазиформулу квазитермом t. Подстановку будем обозначать Fv/t A и Fv/t t1. Подстановка правильна, если ни одна связанная переменная, имеющая свободные вхождения в t не находится в области действия кванторов или -оператора по этой переменной. Ниже мы будем иметь дело только с правильными подстановками. Отметим, что каждая подстановка терма правильна. Каждую формулу, начинающуюся с квантора мы можем представить в виде xFv/xA и xFv/xA. Следуя Гильберту и Бернайсу, будем говорить, что терм t1 вложен в терм t2, если t2 имеет вид Fv/t1 t3, где подстановка, естественно, правильна. Например, терм xD(x) вложен в терм yA(xD(x), y). Квазитерм xB(x,y) подчинен квазитерму yA(y,xB(x,y)),т.е. первый квазитерм имеет свободные вхождения связанной переменной, по которой образован второй терм. В дальнейшем мы будем иметь дело с выводами, посылки и заключение которых не будут содержать -термов. Поэтому в NI в выводы не будут входить формулы с подчиненными друг другу квазитермами.

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

1. Пустая последовательность есть с-последовательность, она не имеет последней формулы и ни одна формула не входит в нее.

2. Если A формула, то A есть последовательность формул, A есть последняя формула и формула A входит в нее.

3. Если есть с-последовательность и A формула, то

A есть с-последовательность, A её последняя формула и формула B входит в нее, если она входит в или графически равна A.

4. Если , и суть с-последовательности формул и A формула, то

и суть с-последовательности, A их

A

A

последняя формула и формула B входит в них, если она входит в или графически равна A.

Будем говорить, что формула C непосредственно выводима из формулы A (A и B), если

есть одно из правил прямого вывода; формула C непосредственно выводима из пустого множества формул, если C есть аксиома, т.е. имеет место правило .

Теперь введем понятие натурального вывода для системы NI.

1. A есть вывод из последовательности посылок A, A входит в A и A есть его последняя формула.

2. Если A есть аксиома, то A есть вывод из пустой последовательности посылок, A есть его последняя формула и входит в вывод.

3. Если есть вывод из последовательности посылок и A посылка, то

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

4. Если есть вывод из последовательности посылок , формула C непосредственно выводима из формул, входящих в ( или является аксиомой), то