4. Определение доказательства.

Пусть Г - множество формул. Формула А выводима из множества гипотез Г, если существует конечная последовательность формул

Ai,Ai,...,An, (2.2)

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

Последовательность (2.2) - это вывод шш доказательство формулы А из множества гипотез Г. Используется обозначение для вывода:

Если Г = 0, то вывод называется доказательством формулы А, а сама формула А в (2.2) называется теоремой. Используется сим-вoJшчecкaя запись для теорем:

Имеет место

Теорема 2.1 (теорема дедукции). Если

Т,А\-В, тоТ\- (АВ).

Доказательство. См. [33, с.112].

2.2.2. Пример доказате-шьства теоремы

Приведем пример (формального) доказательства теоремы. Итак,

Прежде чем изложить доказательство, надо сделать некоторые разъяснения. Формальное доказательство - это просто цепочка «голых» формул. Чтобы воспринять ее, нужно прокомментировать то, как эта цепочка возникает. Иначе говоря, приходится прибегать к русскому языку, помимо языка формального. В противном случае будем иметь подобно тому, что приписывают мифическим античным грекам, чертеж на песке - рисунок к доказательству теоремы из геометрии и слово «Смотри!»

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

Доказательство.

Язык

Метаязык

{Л ((Л Л) Л))

1-я аксиома, подстановка В - (.Л = .Л)

2.2.3. Полнота и непротиворечивость исчисушения высказываний

Теорема 2.2. Ддя исчисления высказываний справедливо утверждение:

[= А тогда и только тогда, когда h А. Доказательство. См. [33, с.117].

Теорема 2.3. Исчисление высказываний - полная теория.

Доказательство. Следует из утверждения «[= Л влечет h А» теоремы 2.2.

Теорема 2.4. Исчисление высказываний - непротиворечивая теория.

Доказательство. Следует из утверждения «I- Л влечет = А» теоремы 2.2. Действительно, если бы была доказуема формула А = B&i~iB, то было бы истинно утверждение B&i~iB. Но последняя формула ложна.

2.3. Исчисление предикатов

2.3.1. Язык и правила вывода исчисления предикатов

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

1. Дополнения в алфавит.

• Знаки индивидуальных переменных

Xi,X2...,Xn,...

• Знаки индивидуальных констант

Ci,C2...,Cn,

• Знаки предикатов

«1 мест «2 мест

• Знаки оператлй

т мест п2 мест

• Логические знаки (кванторы) V, 3.

2. Термы.

1) переменные Xi,...,x„,... - это термы;

1) константы ci,...,Cn,... - это термы;

2) если (•,•) - гг-местный знак операции и ti,термы,

п мест то f\ti,...,tn) терм.

3. Формулы.

1) если Рт (•,•) - п-местный знак предиката и fi,f„ - тер-п мест

мы, то Pm\ti, ,t„) - (атомарная) формула;