Правила заключения

F(t)

F (t).

Правила введения и удаления кванторов

Подстановка некоторого терма t в формулу F(x) вместо ее свободной переменной x состоит в замещении всех свободных вхождений этой переменной данным термом t. Такая подстановка называется правильной. Подстановка будет неправильной если в результате подстановки сколемовской функции свободная переменная окажется в области действия квантора.

F(t).

Если в формулу F(х), содержащей свободную переменную x, выполнить всюду подстановку вместо x терма t , то получим формулу F(t).

Правила подстановки

Для организации вывода заключения из множества посылок используют правила подстановки и правила заключения.

B,

Отношение логического вывода эквивалентно теореме

|¾F₁;F₂;¼F_n®B.

Другая форма записи :

F₁; F₂;¼F_n

где над чертой записывают множество посылок и аксиом F₁;F₂;¼F_n, а под чертой заключение B.

Этот факт записывают так:

_x ò ^tF(x)

Наиболее распространенными правилами являются:

1) Введение квантора общности: “если F₁(t)® F₂(x) выводимая формула и F₁(t) не содержит свободной переменной x , то F₁(t)® "x(F₂(x)) также выводима”, т.е.

(F₁(t)® F₂(x))

(F₁(t)® "_x(F₂(x))).

2) Удаление квантора общности: "если "_x(F(x)) выводимая формула, то вместо x можно выполнить подстановку терма t, свободного от x , и получить также выводимую формулу F (t), т.е.

"_x(F(x))

3) Введение квантора существования: "если терм t вхо­дит в предикат F(t) , то существует, по крайней мере одна предмет­ная переменная x , удовлетворяющая требованиям $_x(F(x)) ”, т.е.

$_x(F(x)).

4) Смена квантора:

"_x(F(x)) $_x(F(x))

ù$_x(ùF(x)); ù"_x(ùF(x)).

5) Перенос квантора, если терм t не содержит переменной x:

a) Â_x(F₁(x))Ú F₂(t)

Â_x(F₁(x)Ú F₂(t));

b) Â_x(F₁(x))&F₂(t)

Â_x(F₁(x)& F₂(t);

c) F₁(t)® Â_x(F₂(x))

Â_x(F₁(t)®F₂(x));

d) "_x(P(x))®F(t)

$_x(P(x)®F(t));

e) $_x(P(x))®F(t)

"_x(P(x)®F(t)).

6) Введение новой переменной:

a) "_x(F₁(x))Ú"_x(F₂(x))

"_y"_x(F₁(y)Ú F₂(x));

b) $_x(F₁(x))&$_x( F₂(x))

$_y$_x(F₁(y)Ú F₂(x)).

Существует два основных правила определения истинности заключения:

а) если F₁ и (F₁®F₂) выводимые фор­мулы, то F₂ также выводима. Это - правило modus ponens (m.p).

F₁; (F₁®F₂)

F_2.

b) если ùF₂ и (F₁®F₂) выводимые формулы, то ùF₁ также. выводима. Это - правило modus tollens (m.t).

ùF₂; (F₁®F₂)

ùF_1.