Правила вывода

Вывод заключения из множества посылок записывается так же, как в исчислении высказываний

F ₁, F ₂,…, F_n ├─ B,

где слева от знака ├─ записывают множество формул посылок и необходимые аксиомы F ₁, F ₂,…, F_n, а справа – формулу заключения B. Тогда знак ├─ означает «верно, что B выводима из F ₁, F ₂,…, F_n».

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

├─ F ₁Ù F ₂Ù…Ù F_n ® B.

Другая форма записи: , где над чертой записывают множество посылок и аксиом F ₁, F ₂,…, F_n, а под чертой заключение B.

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

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

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

Например,

1. .

Это правильная подстановка, т. к. x ₁ – свободная переменная.

2. .

Это правильная подстановка, т. к. x ₁ – свободная переменная.

3. .

Это неправильная подстановка, т. к. x ₃ – связанная квантором $.

4. .

Это неправильная подстановка, т. к. предикат P ₂(x ₃) попадает в область действия квантора $.

Понятие правильной подстановки необходимо, например, для формулировки законов снятия квантора всеобщности

и введения квантора существования

.

Правила введения и удаления кванторов. Наиболее распространенными правилами являются:

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

.

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

.

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

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

; .

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

a) ;

b)

c)

d)

e)

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

a)

b)

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

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

;

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

.

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