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

-^в Если удастся построить контрпример к этой секвенции, то эта секвенция не выводима G' и S не является тавтологией. Система G' эквивалентна исчислению высказываний L в том смысле, что какова бы ни была формула А секвенция ^ А доказуема в G' тогда и только тогда, когда ^ выводима в L. Естественно возникает вопрос — чем уж так интересно исчисление секвенций? Какая, собственно говоря, разница — иметь дело с секвенциями или с формулами, раз всякую секвенцию можно представить формулой? Принципиальное различие тут в следующем. Правила вывода в исчислении секвенций таковы, что в их верхнюю часть входят только подформулы формул, встречающихся в нижней части. Поэтому в выводе какой-то секвенции не может встретиться ничего принципиально нового, чего не было в самой секвенции. В гильбертовском исчислении это далеко не так: мы можем вывести формулу В из формул А В и А, при этом формула А может быть совершенно произвольной. Это же различие объясняет, почему поиск вывода снизу вверх (как можно теперь называть то, что раньше называлось поиском контрпримера — мы находим либо контрпример, либо вывод) для исчисления секвенций происходит сравнительно однозначно (мы можем по- разному выбирать расчленяемую формулу, но и только), в то время как в гильбертовском исчислении, начав с интересуюш,ей нас формулы В трудно указать, из чего бы мы могли получить ее вывод (если только не перебирать все формулы подряд). Можно построить исчисление секвенций для логики предикатов. При этом естественно расширяется множество символов, формулы определяются как в логике предикатов и к правилам (4.27) добавляются правила работы с кванторами. Исходной мотивацией для рассмотрения такого рода исчислений было желание доказать непротиворечивость арифметики. Согласно знаменитой второй теореме Гёделя о неполноте без дополнительных аксиом этого сделать нельзя, но если принять схему аксиом для трансфинитной индукции, это удаётся сделать, как показал Генцен. § 19. Теория естественного вывода Теория естественного вывода называется по разному: исчислением естественного вывода или натуральной дедукцией. Естественный вывод является интересным подходом к заданию дедуктивной теории. Здесь, как и в любой дедуктивной теории, задаются алфавит, формулы (правильно построенные выражения), но нет аксиом, есть только правила вывода. Оказывается, что задание только правил выводов позволяет выделить из множества всех формул некоторое подмножество формул, элементы которого и называются теоремами. Следовательно, не имея ни одной аксиомы (!) можно получить теоремы. 137