Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Исчисление секвенций для высказываний обозначают как систему G 1. Символами системы G' являются: -п,&, V, ^, ),( И буквы Ai с целыми положительными числами в качестве индексов: Aj, А2, As,... Символы -п, &, v, ^ считаются пропозициональными связками, sl A], А2,А з ,... - пропозициональными буквами. Пропозициональные буквы считаются атомами или атомарными формулами. 2. Формулы системы G': 1) каждая пропозициональная буква (т.е. каждый атом) является формулой; 2) если^ и В формулы, то {А&В), {А vB) и {А^В) тоже формулы; 3) выражение системы G' является формулой только тогда, когда это следует из 1) и 2). Выражение (А= В) считаем сокращенной записью формулы (А^В)& (В^А). Для формул системы G' будем придерживаться тех же правил опускания скобок, что и в логике высказываний. В каждой неатомарной формуле, пропозициональную связку, которая применяется последней (в этой формуле) называем главной связкой. Например, в формуле А&(—А^В) главной связкой будет &, а в формуле (AvB)^(B&C) главной связкой будет 3. В системе G' аксиомами считаются те, и только те секвенции, в левой и правой частях которых формулами являются только атомарные формулы, причем некоторый атом встречается в обеих частях секвенции. Пример аксиомы: А, В ^ А. Очевидно, что аксиома не имеет контрпримера. 4. Правила вывода задаются в форме: секвенция секвенция секвенция секвенция секвенция Верхние секвенции считаются посылками, а нижние - заключениями. Справа от правил могут записываться связки —i, &, v, которые исключаются по этим правилам. В каждом правиле считается, что нижняя секвенция имеет контрпример тогда и только тогда, когда хотя бы одна из верхних секвенций имеет контрпример. Пусть Г я Л — некоторые конечные множества формул системы G', а А и В произвольные формулы из G'. Правилами построения контрпримеров (правилами выводов) в системе G' считаются следующие: . Г^А,Л Г^В,Л А,В,Г^Л а) ^ . б) Г^А&В,Л А&В,Г^Л Г -^А,В,А А, Г А В, Г ^ А в) г) (4.27) r^AvB,A AvB,r^A 132