Скачать

Логика предикатов

Проблема разрешимости — эта проблема ставится для формул исчисления предикатов, лишённых символов постоянных предметов и символов индивидуальных предикатов. В последующем изложении предполагается, что рассматриваемые формулы таковы (если не сделано специальных оговорок).

Каждая такая формула представляет собой определённое утверждение, истинное или ложное, когда оно относится к определённому полю M.

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

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

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

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

Постановка проблемы разрешимости для логики предикатов аналогична постановке этой проблемы для алгебры высказываний. Её решение и является целью данной курсовой работы. Итак, проблема ставится следующим образом: дать эффективный способ для определения — является ли данная формула выполнимой или нет.

Умея решать вопрос о выполнимости, мы тем самым сможем решать и вопрос об истинности любой формулы. В самом деле, если формула U истинна, то формула Логика предикатов невыполнима, и обратно. Поэтому, доказав выполнимость или невыполнимость Логика предикатов, мы тем самым проверим истинность U. Проблема разрешимости для логики предикатов является усилением проблемы разрешимости для исчисления высказываний, так как все формулы исчисления высказываний входят в число формул логики предикатов. Однако в то время как решение проблемы разрешимости для исчисления высказываний никаких трудностей не представляет, проблема разрешимости для логики предикатов оказалась связанной с серьёзными трудностями.

Современные исследования пролили свет на природу этих затруднений. В настоящее время представляется достаточно ясным, что решение этой проблемы в указанном смысле вообще невозможно. Иначе говоря, не может существовать никакого конструктивного правила, которое позволяло бы определять для любой формулы логики предикатов, является ли она тождественно истинной или нет. Для некоторых частных типов формул, однако, проблема разрешимости решается. Мы рассмотрим наиболее важный тип формул, для которых решение проблемы разрешимости может быть осуществлено, это формулы логики предикатов, зависящие от одного переменного.

Логика предикатов


Основные понятия

Пусть M - некоторое множество предметов и a, b, c, d - какие-то определённые предметы из этого множества. Тогда высказывания об этих предметах мы будем обозначать в виде

P(a), Q(b), R(c, d) и т.д.

P(a) обозначает высказывание о предмете a, Q(b) - высказывание о предмете b, R(c, d) - высказывание о предметах c и d и т.д.

Такие высказывания могут быть как истинны, так и ложны, обозначаемые соответственно символами И и Л. Эти значения ставятся в соответствие определённым предметам или группам предметов.

Пусть M - произвольное непустое множество, а x представляет собой произвольный предмет из этого множества. Тогда выражение F(x) обозначает высказывание, которое становится определённым, когда x замещено определённым предметом из M. F(a), F(b), ... уже представляют собой вполне определённые высказывания. Например, если M натуральный ряд, то F(x) может обозначать: " x есть простое число".

Это неопределённое высказывание становится определённым, если x заменить некоторым числом, например: "3 простое число", "4 простое число" и т. д.

Пусть S(x,y) обозначает: " x меньше y".

Это высказывание становится определённым, если x и y заменить числами: "1 меньше 3", "5 меньше 2" и т. д.

Так как с нашей точки зрения каждое определённое высказывание представляет собой И или Л, то выражение F(x) означает, что каждому предмету из M поставлен в соответствие один из двух символов И или Л. Иначе говоря, F(x) представляет собой функцию, определённую на множестве M и принимающую только два значения И и Л. Таким же образом неопределённое высказывание о двух и более предметах H(x, y), G(x, y, z) и т. д. предвтавляет собой функцию двух, трёх и т. д. переменных. При этом переменные x, y, z пробегают множество M, а функция принимает значения И и Л. Эти неопределённые высказывания, или функции одного или нескольких переменных, мы будем называть логическими функциями или предикатами. Предикатом с одним переменным можно выразить свойство предмета, например " x есть простое число", " x - прямоугольный треугольник" и т.д.

Все понятия, которые мы будем вводить, относятся всегда к некоторому произвольному множеству M, которое мы будем называть полем. Элементы этого поля будем обозначать малыми латинскими буквами (иногда эти буквы мы будем снабжать индексами). Буквы конца латинского алфавита

x, y, z, u, v, x1, x2, ...

обозначают неопределённые предметы поля. Их мы будем называть предметными переменными. Буквы начала алфавита

a, b, c, a1, a2, ...

обозначают определённые предметы поля. Их мы будем называть индивидуальными предметами или предметными постоянными.

Большими латинскими буквами

A, B, ..., X, A1, A2, ...

мы будем обозначать переменные, принимающие значения И и Л. Их мы назовём переменными высказываниями. Мы будем также рассматривать и постоянные высказывания. Их мы будем также обозначать большими латинскими буквами, как-нибудь отмеченными или просто с дополнительной оговоркой.

Большие латинские буквы и символы предикатов как индивидуальных предметов, так и от предметных переменных мы будем называть элементарными формулами.

Мы будем говорить, что в формулах

("х) U(х) и ($х) U(х)

кванторы ("х) и ($х) относятся к переменному х или что переменное х связано соответствующим квантором.

Предметное переменное, не связанное никаким квантором, мы будем называть свободным переменным.

Формулы, в которых из операций алгебры высказываний имеются только операции Логика предикатов, Логика предикатов и Логика предикатов, а знаки отрицания относятся только к элементарным предикатам и высказываниям, будем называть приведёнными формулами.

Приведённая формула называется нормальной, если она не содержит кванторов или если при образовании её из элементарных формул операции связывания квантором следуют за всеми операциями алгебры высказываний.

Если две формулы U и B, отнесённые к некоторому полю M, при всех замещениях переменных предикатов, переменных высказываний и свободных предметных переменных соответственно индивидуальными предикатами, определёнными на M, индивидуальными высказываниями и индивидуальными предметами из M, принимают одинаковые значения И или Л, то мы будем говорить, что эти формулы равносильны на поле M.

Если две формулы равносильны на любых полях M, то мы будем их называть просто равносильными.

Нормальную формулу, равносильную некоторой формуле U, мы будем называть нормальной формой формулы U.

§1. Логика предикатов с одним переменным

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

Теорема. Если формула логики предикатов, содержащая только предикаты от одного переменного, выполнима на некотором поле M, то она выполнима на поле Логика предикатов, содержащем не более Логика предикатов элементов, где n - число предикатов, входящих в рассматриваемую формулу.

Пусть формула U(A1, ..., An), содержащая только символы предикатов A1, ..., An, каждый из которых зависит от одного переменного, выполнима на некотором поле M. эту формулу мы можем предполагать представленной в нормальной форме, а все предметные переменные в ней связанными. В самом деле, какова бы ни была формула U, мы можем, произведя над ней преобразования, привести её к виду, в котором все кванторы предшествуют остальным символам формулы, при этом состав её предикатов и предметных переменных не изменяется. Если в U есть свободные предметные переменные, то можно связать их квантором общности.

Итак, допустим, что U – нормальная формула. Тогда мы можем представить её следующим образом:

(s x1)(s x2)...(s xp) B(A1, ..., An, x1, ..., xp),

где каждый из символов (s xi) обозначает квантор ("xi) или ($xi), а формула

B(A1, ..., An, x1, ..., xp)

кванторов не содержит.

В формуле B(A1, ..., An, x1, ..., xp) все переменные x1, ..., xp входят в предикаты A1, ..., An, и её можно записать в виде

B(A1(Логика предикатов), ..., An(Логика предикатов)),

где i1, ..., in – числа от 1 до p. Однако, будет удобнее пользоваться выражением

B(A1, ..., An, x1, ..., xp),

если иметь в виду, что B является логической функцией предикатов Ak, а каждый предикат Ak зависит от какого-то одного переменного Логика предикатов.

Покажем, что если для некоторого поля M существуют индивидуальные предикаты

Логика предикатов,..., Логика предикатов,

для которых формула U(Логика предикатов,..., Логика предикатов) истинна, то эта формула истинна и на некотором подмножестве этого поля, содержащем не более Логика предикатов элементов, так как иначе наше утверждение тривиально. Разобьём элементы множества M на классы следующим образом. Для каждой последовательности, содержащей n символов И и Л в произвольном порядке (И, Л, Л, ..., И,), существует часть (может быть, пустая) множества M, содержащая те и только те элементы x, для которых последовательность значений предикатов Логика предикатов(x), Логика предикатов(x), ..., Логика предикатов(x) совпадает с данной последовательностью символов И и Л.

Обозначим через Логика предикатов1, Логика предикатов2, ...,Логика предикатовn

последовательность символов И и Л, где Логика предикатовi представляет собой И или Л, а соответствующий этой последовательности класс элементов x обозначим

Логика предикатовЛогика предикатов, Логика предикатов, ..., Логика предикатов.

Некоторые из этих классов могут оказаться пусты, так как может случиться, что для некоторой последовательности Логика предикатов1, Логика предикатов2, ...,Логика предикатовn не существует такого элемента, для которого предикаты Логика предикатов, Логика предикатов, ..., Логика предикатов принимают соответствующие значения Логика предикатов1, Логика предикатов2, ...,Логика предикатовn . Вместе с тем каждый элемент множества M принадлежит одному из классов Логика предикатов, и различные классы общих элементов не имеют. Число всех классов (пустых и непустых) равно числу последовательностей Логика предикатов1, Логика предикатов2, ...,Логика предикатовn, т. е. Логика предикатов. Следовательно, число q непустых классов Логика предикатов не превышает Логика предикатов. Выберем из каждого непустого класса по одному элементу и обозначим эти элементы

a1, a2, ..., aq.

Множество всех этих элементов обозначим Логика предикатов.докажем, что если формула U(Логика предикатов, ..., Логика предикатов) истинна на поле M, то она истинна и на поле Логика предикатов (так как Логика предикатов –­ часть поля M, то предикаты Логика предикатов определены на Логика предикатов). каждому элементу x поля M поставим в соответствие элемент из Логика предикатов, принадлежащий тому же классу, что и х. В Логика предикатов существует один и только один такой элемент. Элемент из Логика предикатов, поставленный в соответствие х, обозначим Логика предикатов(х). Можно сказать, что мы построили функцию, определённую на множестве M и принимающую значения из множества Логика предикатов.

Логика предикатовЛегко видеть, что имеет место следующая равносильность:

Логика предикатов(х) ~ Логика предикатов(Логика предикатов(х)).

Действительно, Логика предикатов(x) принадлежит тому же классу Логика предикатов, что и x. Но, по определению, для элементов одного и того же класса каждый предикат Логика предикатов принимает одно и то же значение. Отсюда следует, что если в формуле U(Логика предикатов, ..., Логика предикатов) для каждого предметного переменного t заменить каждое выражение Логика предикатов(t) через Логика предикатов(Логика предикатов(х)), то формула U(Логика предикатов, ..., Логика предикатов) перейдёт в формулу Логика предикатов(Логика предикатов, ..., Логика предикатов), равносильную первой. Написание формулы Логика предикатов отличается от U только тем, что все предметные переменные x, y, z, …, u формулы U замещены соответственно через Логика предикатов(х), Логика предикатов(y), ..., Логика предикатов(u). Это следует из того, что по условию формула U(Логика предикатов, ..., Логика предикатов) содержит только предикаты Логика предикатов, и поэтому всякое предметное переменное входит только под знаком одного из этих предикатов.

Пусть R (x, y, ..., u) – предикат, определённый на поле M. Введём обозначение

Логика предикатов R (x, y, ..., u).

Под этим выражением мы будем понимать предикат, зависящий от y, z, ..., u (или высказывание, если, y, z, ..., u отсутствуют) и принимающий значение И, когда R (y, z, ..., u) имеет значение И для данных y, z, ..., u и для всех x, принадлежащих полю Логика предикатов, и принимающий значение Л в противоположном случае. Введём также выражение

Логика предикатов R (x, y, ..., u),

которое представляет собой предикат от y, ..., u и принимает значение И, когда R (x, y, ..., u) имеет значение И для y, ..., u и по крайней мере для одного значения x из поля Логика предикатов, и значение Л в противоположном случае. Знаки Логика предикатов и Логика предикатов будем называть ограниченными кванторами. Если мы все переменные предиката R (x, y, ..., u) свяжем ограниченными кванторами, например

Логика предикатовЛогика предикатов...Логика предикатов R (x, y, ..., u),

то получим формулу, отнесённую к полю Логика предикатов. покажем, что выражение

("x) R (Логика предикатов(х), y, ..., u)

равносильно выражению

Логика предикатов R (x, y, ..., u).

Пусть ("x) R (Логика предикатов(х), y, ..., u) имеет значение И. В таком случае R (Логика предикатов(х), y, ..., u) имеет значение И для данных y, ..., u и для каждого x. Но так как функция Логика предикатов(х) пробегает всё поле Логика предикатов, когда x пробегает поле M, то R (x, y, ..., u) имеет значение И для данных y, ..., u и для всех x из Логика предикатов. В силу определения Логика предикатов R (x, y, ..., u) также принимает значение И. Обратно, если Логика предикатов R (x, y, ..., u) принимает значение И, то R (x, y, ..., u) имеет значение И для данных y, ..., u и для каждого x из Логика предикатов. В таком случае выражение R (Логика предикатов(х), y, ..., u) имеет значение И для данных y, ..., u и для каждого x из M, так как Логика предикатов(х) для любого x принадлежит Логика предикатов.

Аналогичным образом можно показать, что выражения

(Логика предикатов) R (Логика предикатов(х), y, ..., u) и (Логика предикатов) R (x, y, ..., u)

также равносильны.

Рассмотрим формулу U(Логика предикатов, ..., Логика предикатов), которую можно представить в форме

(s x1)(s x2)...(s xp) B(Логика предикатов, ..., Логика предикатов, x1, ..., xp).

B(Логика предикатов, ..., Логика предикатов, x1, ..., xp)

представляет собой предикат, определённый на поле M и зависящий от p переменных x1, ..., xp. Каждое из этих переменных входит в формулу B только через предикаты Логика предикатов, ..., Логика предикатов. С другой стороны, мы видели, что предикаты Логика предикатов(х) и Логика предикатов(Логика предикатов(х)) равносильны. Поэтому если в формуле B(Логика предикатов, ..., Логика предикатов, x1, ..., xp) мы заменим xi на Логика предикатов(хi), то получим равносильное выражение:

B(Логика предикатов, ..., Логика предикатов, x1, ..., xp) ~ B(Логика предикатов, ..., Логика предикатов,Логика предикатов(x1), ..., Логика предикатов(xp)).

Отсюда следует, что

(s xp) B(Логика предикатов, ..., Логика предикатов, x1, ..., xp) ~ (s xp) B(Логика предикатов, ..., Логика предикатов, Логика предикатов(x1), ..., Логика предикатов(xp)).

Далее можно заключить, что

(s xp) B(Логика предикатов, ..., Логика предикатов, Логика предикатов(x1), ..., Логика предикатов(xp)) ~

~ Логика предикатов B(Логика предикатов, ..., Логика предикатов, Логика предикатов(x1), ..., Логика предикатов(xp-1), xp).

Рассуждая аналогичным образом, мы получим

(s xp-1) (s xp) B(Логика предикатов, ..., Логика предикатов, x1, ..., xp-1 , xp) ~

~Логика предикатовЛогика предикатов B(Логика предикатов, ..., Логика предикатов, Логика предикатов(x1), ..., Логика предикатов(xp-2), xp-1, xp)

и, наконец, придём к следующему:

(s x1)(s x2)...(s xp) B(Логика предикатов, ..., Логика предикатов, x1, ..., xp) ~

~ Логика предикатовЛогика предикатов B(Логика предикатов, ..., Логика предикатов, x1, ..., xp).

Правая часть последней равносильности, согласно смыслу символа Логика предикатов, представляет не что иное, как формулу

(s x1)...(s xp) B(Логика предикатов, ..., Логика предикатов, x1, ..., xp),

отнесённую к полю Логика предикатов.

Таким образом, мы доказали, что формула U(Логика предикатов, ..., Логика предикатов) сохраняет своё значение, если её отнести к полю Логика предикатов, и теорема, таким образом, доказана.

С л е д с т в и е. Если формула U, содержащая только предикаты, зависящие от одного переменного, является тождественно истинной для всякого поля, не превышающего Логика предикатов элементов, где n – число предикатов в U, то формула U тождественно истинна (т. е. истинна для любого поля). В самом деле допустим, что U не является тождественно истинной формулой. В таком случае её отрицание Логика предикатов выполнимо на некотором поле. Так как Логика предикатов также удовлетворяет условиям теоремы, то найдётся поле, содержащее не более Логика предикатов элементов, на котором формула Логика предикатов выполнима. Следовательно, U не может быть истинной на этом поле, что противоречит условию. Итак, предположение, что U не является тождественно истинной, приводит к противоречию, что и требовалось доказать.

§2. Практика по решению проблемы разрешимости формул,

содержащих предикаты от одного переменного

Доказанная (в предыдущем параграфе) теорема позволяет решать проблему разрешимости для формул, содержащих только предикаты, зависящие от одного переменного. Из следствия видно, что для того, чтобы установить, является ли формула U тождественно истинной или нет, достаточно проверить, является ли она тождественно истинной для всякого поля, содержащего не более чем Логика предикатов элементов.

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

Рассмотрим произвольное поле, содержащее ровно Логика предикатов элементов: Логика предикатов, Логика предикатов, ..., Логика предикатов. Легко видеть, что всякая формула, имеющая вид:

("x) B(x),

отнесённая к данному полю, равносильна формуле

B(Логика предикатов) & B(Логика предикатов) & ... & B(Логика предикатов).

А формула, имеющая вид:

(Логика предикатовx) B(x),

равносильна формуле

B(Логика предикатов) Логика предикатов B(Логика предикатов)Логика предикатов ... Логика предикатов B(Логика предикатов).

В таком случае произвольная формула U, отнесённая к полю {Логика предикатов, ..., Логика предикатов}, равносильна формуле Логика предикатов, в которой все кванторы заменены операциями логического произведения и логической суммы. Если в U входили только предикаты A1, ..., An, зависящие от одного переменного, то Логика предикатов представляет собой формулу, образованную только операциями алгебры высказываний над выражениями Ai(xj), 1 ? i ? n, 1 ? j ? Логика предикатов. Так как предикаты Ai(x) совершенно произвольны, то выражения Ai(xj) представляют собой совершенно произвольные высказывания. Формулу Логика предикатов тогда можно рассматривать как формулу алгебры высказываний, у которой Ai(xj) являются элементарными переменными высказываниями. Тогда вопрос о тождественной истинности U на поле Логика предикатов, Логика предикатов, ..., Логика предикатов оказывается эквивалентным вопросу о тождественной истинности Логика предикатов, как формулы алгебры высказываний с переменными высказываниями Ai(xj).

Заметим, что формула алгебра высказываний Логика предикатов по существу не зависит от того, каковы элементы поля {Логика предикатов, ..., Логика предикатов}, а зависит только от их числа, так как если мы возьмём другое поле {Логика предикатов¢, ..., Логика предикатов¢}, то в Логика предикатов произойдёт только перемена обозначений переменных высказываний Ai(xj) на Ai(xj¢). В силу этого мы можем сказать, что если Логика предикатов тождественно истинна, как формула алгебры высказываний, то формула U тождественно истинна на любом поле из p элементов, и обратно. С другой стороны, был получен конструктивный способ определять – является произвольная формула алгебры высказываний тождественно истинной или нет. Применяя этот критерий, мы можем установить, будет ли произвольная формула U, содержащая только предикаты от одного переменного, тождественно истинной на любом поле, содержащем p = Логика предикатов элементов. В таком случае в силу высказанного выше положения мы можем решить также и вопрос о том, будет формула U тождественно истинной или нет.

Разберём это конкретно на примерах.

П Р И М Е Р 1: Итак, пусть дана формула U, имеющая вид:

("x)(P(x)Логика предикатов( Логика предикатовЛогика предикатовP(x))),

отнесённая к некоторому полю L. Для того, чтобы установить тождественную истинность этой формулы, нам достаточно проверить, является ли она тождественно истинной на поле, содержащем ровно Логика предикатов элементов (см. выше). В данном случае число предикатов (n) равно 2, т.е. L может быть представлено как { a1, a2, a3, a4 }.

Легко видеть, что формула 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 можно опять определить как { 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-символом и предикатом существования

Существуют два типа систем натурального вывода: с прямым и непрямым правилом удаления квантора существования. Прямое правило удаления квантора существования по существу формулируется с использованием языка с э