III. Правила вывода системы S. Фиксируется (обычно конечная) совокупность предикатов R1,…, Rk на множестве всех формул системы S. Пусть R1 (x1, ..., хni, хni+1) — какой-либо из этих предикатов, причем ni > 0. Если для данных формул F1, ..., Fni, Fni+1 утверждение Ri (Fl, ..., Fni, Fni+1) истинно, то говорят, что формула Fni+i непосредственно следует из формул F1( ..., F по правилу вывода Ri.
Заданием языка системы, ее аксиом и правил вывода формальная система S полностью определяется как математический объект. Понятие теоремы или выводимой формулы образуется для всех формальных систем единообразным способом. Выводом системы S называется всякая конечная последовательность формул этой системы, в которой каждая формула либо является аксиомой системы S, либо непосредственно следует из каких-либо предшествующих ей в этой последовательности формул по одному из правил вывода данной системы. Формула системы S называется теоремой, если существует вывод системы S, заканчивающийся этой формулой.
Всякую конкретную математическую теорию Т можно перевести на язык подходящей формальной системы S таким образом, что каждое осмысленное (ложное или истинное) предложение теории Т выражается формулой системы S.
Гильберт и его ученики надеялись путем изучения формальных систем получить доказательство непротиворечивости арифметики натуральных чисел, не использующее таких сильных методов, как абстракция актуальной бесконечности. Однако, эта программа потерпела крах, поскольку в начале 30-х годов XX в. К- Геделем были доказаны следующие утверждения:
1) Всякая естественная непротиворечивая формализация S арифметики натуральных чисел или другой математической теории, содержащей арифметику {например, теории множеств), неполна и непополнима в том смысле, что:
а) в S имеются содержательно истинные формулы F, такие, что они F, ни не являются водимыми в S (такие формулы называют неразрешимыми в S);
б) каким бы конечным множеством дополнительных аксиом ни расширить систему S, в новой системе неизбежно появятся свои неразрешимые формулы.
2) Если формализованная арифметика натуральных чисел в действительности непротиворечива, то хотя утверждение о ее непротиворечивости выразимо на ее собственном языке, однако доказательство этого утверждения, проведенное средствами, формализуемыми в ней самой, невозможно.
Таким образом, уже в арифметике натуральных чисел невозможно исчерпать весь объем содержательно истинных утверждений классом выводимых формул и нет надежды получить когда-либо формализованное доказательство непротиворечивости арифметики, не использующее понятие бесконечности. Все это ставит определенные границы аксиоматического метода в математике.
5.
Достарыңызбен бөлісу: |