Логика предикатов (стр. 5 из 7)
Таким образом,
представляет собой формулу, образованную только операциями алгебры высказываний над выражениями P( 
) и Q( ), где i= 
, т.е. её можно рассматривать как формулу алгебры высказываний, у которой P( ) и Q( ) являются элементарными переменными высказываниями. Значит, ответив на вопрос о тождественной истинности , мы сможем сказать, является ли формула U тождественно истинной или нет. является тождественно истинной в алгебре высказываний 
U также тождественно истинная формула на поле, содержащем 
элементов. Это оэначает, что U тождественно истинна.П Р И М Е Р 2: Доказать, что формула U, отнесённая к некоторому полю L, представленная как
[("х)(
Q(x)) P(x)],является тождественно истинной.
Для этого она должна быть тождественно истинной на поле, содержащем ровно
элементов. В данном случае n = 2, т.е. L можно опять определить как { a1, a2, a3, a4 }.Применяя равносильные преобразования над U, можем заключить её равносильность формуле: ($х)[(
Q(x)) P(x)], которая, отнесённая к полю L, равносильна : [( 
Q( 
)) P( )] 
[( 
Q( 
)) P( )] [( 
Q( 
)) P( )] [( 
Q( 
)) P( )].Легко видеть, что
, как и в предыдущем примере, представляет собой формулу, образованную только операциями алгебры высказываний над выражениями P( ) и Q( ), где i= , а поэтому её можно отнести к формулам алгебры высказываний, у которой P( ) и Q( ) являются элементарными переменными высказываниями. Является ли формула тождественно истинной?Формула
представляет собой дизъюнкции некоторых формул. Поэтому всякий раз, когда одна из них истинна, сама (по определению дизъюнкции) будет тождественно истинной. Составим таблицу истинности: | P | Q |  |  Q | ( Q) P |
| 0 | 0 | 1 | 0 | 1 |
| 0 | 1 | 1 | 1 | 0 |
| 1 | 0 | 0 | 1 | 1 |
| 1 | 1 | 0 | 1 | 1 |
Таким образом, формула (
Q) P является выполнимой, следовательно, является тождественно истинной формулой в алгебре высказываний U также тождественно истинная формула на поле, содержащем элементов. Это означает, что U тождественно истинна.§3. Поиск доказательств в натуральном интуиционистском исчислении предикатов с e-символом и предикатом существования
Существуют два типа систем натурального вывода: с прямым и непрямым правилом удаления квантора существования. Прямое правило удаления квантора существования по существу формулируется с использованием языка с эпсилон-символом. Классическое исчисление предикатов с прямым правилом удаления квантора существования элегантно и является хорошей основой для организации систематической процедуры поиска доказательств. Мною была предложена процедура поиска доказательств для классического исчисления предикатов с прямым правилом удаления квантора существования [7]. А.В. Смирнов и А.Е. Новодворский [3] реализовали ее на компьютере. Хотелось бы построить интуиционистское исчисление предикатов с прямым правилом удаления квантора существования и на этой основе сформулировать алгоритм поиска доказательств. Однако на этом пути мы встречаемся с определенными трудностями. Если мы заменим классические пропозициональные правила интуиционистскими, то в результате получим логическую систему, более богатую, нежели интуиционистское исчисление предикатов. Действительно, допустим, что имеет место $xA(x). По правилу удаления квантора существования получим A(exA(x)). По правилу введения импликации будем иметь $xA(x)ÉA(exA(x)). Из последней формулы по правилу введения квантора существования получаем $y($xA(x)ÉA(y)). Запишем этот вывод формально