Cтраница 4
Эта конструкция позволяет общий случай локально совместной системы формул свести к случаю локально совместной системы формул исчисления высказываний. Первоначальные доказательства теоремы 4.1 были основаны именно на этой идее. Следует еще заметить, что каждое доказательство локальной теоремы содержит некоторый намек относительно характера модели, на которой выполняются все формулы заданного набора. В связи с этим желательно иметь различные доказательства, приводящие к разным конструкциям подходящих моделей. [46]
Это определение применимо не только к исчислению предикатов, но и к любому другому логическому исчислению, в частности к исчислению высказываний. Поскольку в исчислении высказываний присоединение любой невыводимой формулы к числу аксиом делает выводимыми все формулы, то любые две невыводимые формулы исчисления высказываний оказываются дедуктивно эквивалентными. Ясно также, что любые выводимые формулы ( в любом исчислении) являются дедуктивно эквивалентными. В то же время дедуктивная эквивалентность выводимой и невыводимой формул невозможна, поскольку присоединение первой формулы к системе аксиом не сделает выводимой вторую формулу. [47]
В этом утверждении мы можем заменить схемы формул, соответствующие тождественно истинным формулам, самими этими формулами, считая, что используемые в выводах схемы применяются к формулам исчисления высказываний, не содержащим знака дизъюнкции. Это вытекает из упомянутого в конце предыдущего параграфа результата, утверждающего, что выводы, производимые с помощью схем, применяемых к формулам исчисления высказываний, протекают совершенно аналогично выводам, применяемым к схемам формул, получающимся из соответствующих формул в результате замены формульных переменных буквами, обозначающими произвольные формулы. [48]
По сравнению с определением § 17, пункт 1 прежнего определения заменен новым пунктом 1, а пункты 6 - 7 откинуты. Если будет желательно проводить различия между обоими понятиями формулы, мы будем называть формулы в смысле § 17 арифметическими формулами, а формулы в только что введенном смысле - формулами исчисления высказываний, или пропозициональными формулами. [49]
Теперь мы можем ответить на вопрос, поставленный выше: может ли формула исчисления высказываний, не являющаяся выводимой в исчислении высказываний, быть выводимой в исчислении предикатов. Докажем, что такой формулы не может быть. Пусть Я - формула исчисления высказываний, - выводимая в исчислении предикатов; тогда соответствующая ей формула 51 выводима в исчислении высказываний. Но так как 51 -сама формула исчисления высказываний, то 51 совпадает с 51 н, значит, 51 выводима в исчислении высказываний, что и требовалось доказать. [50]