Выберем - символы переменных которые различны между собой и не входят не в одну из формул , сделаем подстановку и последовательно применим и в новом слове делаем последовательную подстановку: , где - является формальным выводом.

3.1.3 Формальный вывод из гипотез.

Опр: Формальным выводом из гипотез (формулы), называется такая последовательность слов , каждая из которых удовлетворяет условию:

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

Лемма: ; : то тогда

Напишем список:

Лемма:

Док:

3.1.4 Теорема Дедукции.

Если из

1) и 2а) , где по правилу m.p. , ч.т.д.

2б) - уже выводили , ч.т.д.

Базис индукции: N=1 - формальный вывод из длинного списка

(только что доказано), осуществим переход по индукции:

по индукции

и по лемме 2

Пример:

по теореме дедукции

3.2 Критерий выводимости в ИВ.

3.2.1 Формулировка теоремы.

- тавтология

при любой интерпретации алфавита (символов переменных)

3.2.2 Понятие интерпретации.

символ переменной переменную поставим в соответствие.

, где - проекция на .

; - только символ

переменных, т.к.

это заглавное слово

формативной последо-

вательности вида:

Где:

3.2.3 Доказательство теоремы.

формальный

вывод

(1)

3.3 Непротиворечивость ИВ.

3.3.1 Определение.

1) ИВ противоречиво, если формула А выводима в нем. .

2) формула выводима в ИВ)ИВ противоречиво.

3) ИВ противоречиво.

ИВ непротиворечиво, если оно не является противоречивым.

Теорема: ИВ является непротиворечивым исчислением по отношению к любому из трех определений.

Док-во: (1) Если , то соответствующая ей булева функция будет тождественно равна 1.

(2) Если любая формула выводима, то выводима и А, что соответствует пункту 1.

(3) Пусть и - булева функция

- противоречие.

3.4 Формальные исчисления.

Алфавит – конечное или счетное множество символов, возможно, разбитых на группы. Алфавит должен быть упорядоченным множеством.

Слово – конечная упорядоченная последовательность символов алфавита, в т.ч. пустое слово.

V – множество всех слов.

Вычислимая функция от нескольких натуральных переменных