Гильберт, Бернайс - Основания математики. Теория доказательств (Гильберт Д. - Основания математики и прочие работы), страница 12

Остающееся утверждение о том, что всякая нумерическая формула, выводимая из аксиом системы (В*) среуГствами элементарного исчисления со свободными переменными, является истинной, получается просто (аналогично рассуждению из гл. у'1 т. 1) с уче~ом следующих фактов: 1. К любзму конкретному выводу нумерической формулы из аксиом системы (В*), проводимому средствами элементарного исчисления, могут быть применены операции разложения фигуры доказательства на нити, возвратного переноса подстановок в исходные формулы и исключения всех свободных переменных; в результате этого мы получим некоторую фигуру доказательства (в обобщенном смысле), в которой всякая исходная формула получается в результате подстановки либо из некоторой тождественно истинной формулы исчисления высказываний, либо из одной из аксиом системы (В*).

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

Всякая нумерическая формула, получающаяся из какой- либо аксиомы системы (5') в результате подстановки цифр вместо свободных переменных, является истинной. Если Е( и 21- 6 являются истинными нумерическими формулами, то 6 также является истинной формулой. Этот метод доказательства непротиворечивости системы (В*), а тем самым также и (В), имеет существенное преимущество по сравнению с методом редукции, который мы использовали при доказательстве непротиворечивости (5) в гл. Л1 т. 1. Преимущество это заключается в том, что применимость его носит более универсальный характер. Действительно, метод редукции существенным образом использует то обстоятельство, что каждое арифметическое отношение, выразимое в (В) с помощью связанных индивидных переменных (но все.таки без использования формульных переменных), выразимо и без связанных переменных; ') Это применение е-теоремы соотаететауег геореме об злементарном аыаоде; ем.

с, 37, ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ !ГЛ, 1 б9 ДОКАЗАТЕЛЬСТНА НЕПРОТИИОРЕЧИНОСТИ например, отношение :-)х (а ( х бе х - Ь) выразимо в виде а отношение в виде а'СЬ, »вех(а<к 1,( х<Ы/ х=с) (а -Ь) Ч'(а=Ьйа=с). ») См. т. 1, Тл. Ч!, с. 294'.— Этот термин выбран с учетом того, что при содержательном истолковании рассматриваемых формул нм соответствуют имеющие характер всеобщности математические предложения, ко»орые могут быть верифипнрованы (подтверждены) в каждом отдельном случае, хотя обще.

вначииость их может быть н не вернфнпирована. ') Авторы употребляют термин «чае!аЬ!еп!сам — Прим, перев. я) См. т, 1, гл, Ч11, с. 363. Такая возможность исключения связанных переменных имеется только у очень специальных систем, в то время как устранимость связанных переменных из вывода любой формулы, не содержащей связанных переменных, согласно нашей е-теореме, имеет место для всякой формализованной средствами исчисления предикатов системы, содержа!цей только собственные аксиомы беэ сниэанных переменных. В качестве специального (т. е. касающегося не только типов встречающихся переменных) свойства аксиом систем (В*) в последнем доказательстве использовалось лишь то, что каждая из этих аксиом при произвольной замене свободных переменных цифрами переходит в истинную нумерическую формулу, т. е.

то, что аксиомы эти, как мы говорим для краткости, являются вер и фицируемыми фор мулами'). Это понятие верифицируемости тоже пока еще обременено ненужными ограничениями. В самом деле, оно определено в расчете на такой формализм, в котором каждый терм, не содержащий свободных переменных, — или, как мы будем для кратности говорить, п о с т о я н н ы й *) т е р м — является цифрой. Некоторое обобщение этого понятия, учитывающее появление функциональных знаков для рекурсивных функций, мы уже произвели в гл. И! т.

1'). Но, взобце говоря, мы ие обязаны ограничиваться рассмотрением только арифметических формализмов, в которых имеется символ 0 и штрих-символ (или какие- нибудь другие аналогичные символы вместо них) в их специфической роли. Более того, можно дать общее определение понятия вер ифици р уемости, годящееся для любого формализма, содержащего постоянные термы. Такое определение будет опираться на распределение истинностных значений постоянных элементарных формул, причем под распределением значений мы будем понимать некоторый способ, позволяющий каждой конкретно заданной постоянной элементарной формуле рассматриваемого формализма однозначно сопоставлять одно из двух значений «истина» или «ложь». Всякое гакое распределение истинностных значений для постоянных элементарных формул, если связки исчисления высказываний истолковывать как истинносдные функции, естественным образом порождает распределение и для любых постоянных формул.

При этом всякая постоянная формула однозначным образом оказывается либо истинной, либо ложной, а всякая постоянная формула, являющаяся результатом подстановки в тождественно истинную формулу исчисления высказываний, оказывается истинной. Формулу, не содержащую никаких других переменных, кроме свободных индивидиых, мы будем называть в е р и ф и ц ир у е м ой, если при любой замене этих переменных постоянными термами оиа оказывается истинной. С помощью этого понятия мы можем сформулировать следующую общую теорему о непротиворечивости («нп-теорему»): Пусть Р— формализм, получающийся из исчисления предикатов путем добавления к нему некоторых индивидных, предикатных и функциональных символов, а пшкже некоторых сайго!венных аксиом. Пусгпь имеегпся способ, позволяющий однозначно соотнести истинностные значения постоянным элементарным формулам.

Пусть аксиомы не содержат связанных переменных и пусть при данном распределении истинностных значений они являются верифицируемыми формулами. Тогда формализм Р непротиворечив в том сильном смысле, что любая выводимая в нем постоянная формула яллягтся истинной. Доказательство этой теоремы получается совершенно аналогично доказательству непротиворечивости системы (За), проведенному нами с использованием первой в-теоремы.

Заслуживают внимания следующие добавления: !. Всякая выводимая в формализме Р формула, не содержащая других переменных, кроме свободных индивидных, является верифицируемой. В самом деле, любая замена в формуле такого рода свободных переменных какими-либо постоянными термами может рассматриваться как подстановка, и поэтому она дает нам формулу, выводимую в Р; согласно утверждению нашей теоремы эта формула является истинной.

2. По выводу всякой выводимой в Р формулы вида Зб,... -)б„й!(бя, ..., б„), не содержащей других переменных, кроме бм .., б„можно найти ДОКАЗАТЕЛЬСТВА НЕПРОТИВОРЕЧИВОСТИ е и ао )ГЛ 1 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ такие постоанные теРмы Ьм ..., Г„длл котоРых фоРмУла 6(1„..., 1„) будет истинной. Это вытекает из доказанного нами обобщения первой е-тео- ремы.

Будучи применено к нашему случаю, оно утверждает, что, исходя из вывода формулы Эуе.. --)у,6(«1, ", у„), с помощью нашей процедуры исключения связанных переменных можно получить некоторую формулу ) У 6 (1(е) 1(е)) которая выводится из аксиом формализма р средствами элемен- тарного исчисления и в которой 11", ..., 1(е) суть термы, не со- держащие е-символа и, следовательно, построенные из одних только свободных переменных, индивидных символов и функци- ональных знаков формализма г.

Если вместо всех встречающихся в этой формуле свободных индивидных переменных мы подставим один и тот же индивид- ный символ, то у нас снова получится выводимая в г формула, которая теперь будет постоянной, а потому и истинной. Значит, по крайней мере один из членов нашей дизъюнкцин будет истин- ной формулой и эта формула будет иметь вид 6(11 ° ° ° 1), где 1„..., 1,— некоторые постоянные термы. 3.

Если какая-нибудь формула вида Ууе... Уу„=)«1...--))),6(уе, ..., у„, «„..., «,), не содержаи(ая никаких переменных, кроме у„..., у„«„..., «, выводима в Р, то по выводу втой формулы для всякой системы постоянных термов а„..., а„можно будет найти такие посто- янные термы Ь1, ..., Ье для которых формула 6(а„..., а„, Ь,, ..., Ь,) является истинной. Это следует из добавления 2 с учетом того, что для каждой системы термов а,, ..., а„из формулы Ууе...))уу„'З«1...3«,«1(у1, .", у„«1, ", «,) с помощью основной формулы (а) исчисления предикатов может быть выведена формула =)«1...-)«,6(ам ., а„, «1,, «,), 4.

Утверждение сформулированной нами теоремы о непроепиворечивости вместе с добавлениями 1, 2 и 3 останется верным и в том случае, если мы к формализму Р добавим В-символ и е-формулу. В самом деле, при доказательстве первой е-теоремы мы с самого начала с целью исключения кванторов добавили к рассматриваемому формализму е-символ и е-формулу. Это замечание является очень важным, так как с помощью е.формулы мы можем дать общую формализацию всех способов определения, объединяемых )-правилом, и операции символьного решения экзистенциальных высказываний ').

Доказанную нами теорему о непротиворечивости, включая добавления 1 — 4, мы для краткости будем называтынп-теоремойы б) Приложение к геометрии. Установленная выше нп-теорема дает нам метод, позволяющий доказывать непро~иворечивость различных аксиоматических теорий, формализованных средствами исчисления предикатов, при условии, что для их аксиом мы располагаем каким-либо финитным арифметическим истолкованием.

При этом непротиворечивость получается и в том случае, когда к числу аксиом добавляется е-формула. Конечно, одного финитного истолкования какой-либо системы аксиом еще недостаточно для того, чтобы финитно убедиться в непротиворечивости этой системы, так как это истолкование не распространяется на доказательства. Формализованные посредством исчисления предикатов способы умозаклк)чений вносят в финитную интерпретацию некоторый нефинитный элемент. Однако с помощью нп-теоремы можно убедиться в приемлемости этих способов умозаключений. Все сказанное мы детально продемонстрируем на примере аксиоматики элементарной геометрии. Пример этот интересен и сам по О)бе. Под элементарной мы будем понимать здесь геометрию, основанную на аксиомах соединения, порядка, конгруэнтности и на аксиоме о параллельных (аксиомы непрерывности мы исключаем).

Ради простоты мы ограничимся геометрией плоскости. Перенос рассматриваемого метода на случай пространства никаких принципиальных трудностей не вызывает. Для того чтобы иметь возможность непосредственно воспользоваться нашей нп-теоремой, мы должны будем выписать рас- сматриваемую систему аксиом в разрешенном виде. Аксиомы соединения и порядка в том уже разрешенном виде, как они получаются иа основе редакции, приведенной в гл.