Деревья в логике предикатов

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

Эти правила применяются к формуле еще до построения ее дерева.

Правила исключения кванторов

К1. Каждый квантор существования, не находящийся в области действия квантора общности, заменяется новой предметной константой, ранее не входившей в формулу.

К2. Каждый квантор существования, находящийся в области действия квантора общности, заменяется новой предметной функцией, ранее не входившей в формулу.

К3. Если формула содержит кванторы общности, то они исключаются с условием, что каждая связанная предметная переменная по-прежнему остается связанной, т.е. может быть при необходимости в дальнейшем заменена на любую предметную константу или предметную функцию, являющуюся элементом расширения предикатов формулы.

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

Дадим небольшие пояснения и приведем несколько примеров конструирования деревьев формул с предварительным исключением кванторов.

Правило К1 характеризует ситуации, когда исключаемый квантор существования не находится в области действия одного или нескольких кванторов общности. Это означает, что такой квантор существования указывает на вещь универсума, независимую от существующих кванторов общности. Поэтому, согласно правилу К1, выполняются следующие действия:

• формула (Ех) фх заменяется на фа, если константа а ранее не входила в ф;

• формула (Ех) фах - на фаЬ, если константа bранее не входила в ф;

• формула (Ех) (Еу) фаЬху - на формулу фаЬссІ,если константы cи d ранее не входили в формулу ф;

• формула (Ех) (Еу) (z) φхyz- на формулу (z) φаЬz, если константы а и bранее не входили в формулу ф.

Правило К2 характеризует ситуации, в которых исключаемый квантор существования находится в области действия по крайней мере одного из кванторов общности. Тем самым вещь, обозначаемая квантором существования, принадлежит области действия по крайней мере одного из кванторов общности. Ее подчинение символизируется введением новой предметной функции. Эта функция напоминает о том, что переменная квантора существования зависит каким-то образом от переменной квантора общности. Но при этом конкретный вид зависимости значения для дальнейших вычислений не имеет.

Значит, согласно правилу К2, выполняются следующие действия:

• формула (х) (Еу) фху заменяется на формулу (х) фх/(x);

• формула (x) (Ey) (Ez) φхyz- на формулу (х) фх/(x) g (x);

• формула (x) (y) (Ez) φхyz- на формулу (х) (у) фху/(xy);

• формула (Ех) (y) (z) (ѵ) (Ew) φхyzvw- на формулу (y) (z) (ѵ) φaуzvf (yzv), если константа а ранее не входила в рассматриваемую формулу.

Правило КЗ позволяет снимать кванторы общности без ограничений при условии, что их переменные остаются связанными и на их место могут подставляться любые, простые или сложные, термы.

Следовательно, согласно правилу К3:

• формула (х) (у) фху сначала заменяется на формулу фху и, допустим, в универсуме U = {a, b}может быть далее заменена на формулы φaa, или φab,или φbα, или φbb;

• формула (х) (Ey)фху сначала заменяется на формулу φxf (x)и, допустим, в универсуме U = {a, b} может быть далее заменена на формулы φaf (а) или φbf (b).

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

Поэтому, согласно правилу К4:

• формула (φx ⊃(Еу)φy) заменяется на формулу (φa ⊃ φb), если константы aи bне входили ранее в формулу φ;

• формула (φx ⊃ (y) φy) заменяется на формулу (φa ⊃ φy), если константа aранее не входила в формулу φ, где предметная переменная у остается связанной.