Cтраница 2
Можно было бы подумать, что результат Геделя вскрывает лишь недостаточную полноту выбранной нами системы аксиом формальной арифметики и что при разумном пополнении этой системы аксиом новыми аксиомами неполнота арифметики ( при сохранении ее непротиворечивости) уже не будет иметь места. В действительности дело обстоит далеко не так просто. Как показывает подробный анализ, проведенный Геделем, при любом непротиворечивом расширении системы аксиом формальная арифметика продолжает оставаться неполной и в ней по-прежнему будут существовать неразрешимые замкнутые формулы. Более того, всякая формальная система, удовлетворяющая некоторым довольно общим условиям ( наличие достаточно богатого набора формул и объектов), в случае ее непротиворечивости будет обязательно неполной. [16]
Эта теорема впоследствии была наполнена следующим более общим смыслом: какова бы ни была система аксиом формальной арифметики, удовлетворяющая некоторым разумным ( см. ниже) требованиям, существует истинная в стандартной интерпретации замкнутая формула, не выводимая из этой системы аксиом. Разумные требования состоят в следующем: 1) каждая аксиома истинна в стандартной интерпретации; 2) существует алгоритм, распознающий по любой замкнутой формуле рассматриваемой сигнатуры, является ли она аксиомой или нет. [17]
Россер показал [71], что можно построить пример формулы, неразрешимость которой устанавливается без предположения об со-непротиворечивости формальной арифметики. Для этого достаточно ее простой непротиворечивости. Формула, о которой здесь идет речь, строится следующим способом. Если обозначить эту формулу через Pq ( x) ( q - ее геделевский номер), то формула Pq ( q) представляет собой искомый пример формулы, неразрешимость которой устанавливается с помощью предположения о простой непротиворечивости формальной арифметики. [18]
ЭД уУ, , , , , 0), где N - множество натуральных чисел, является стандартной моделью формальной арифметики. [19]
Изданной в Брауншвейге в 1888 г. Следует отметить, что после обнаружения парадоксов теории множеств, а особенно после установленной Геделем неполноты формальной арифметики надежды Дедекинда и Гильберта о решении проблемы непротиворечивости арифметики натуральных чисел не оправдались: непротиворечивость формальной системы, включающей формальную арифметику, может быть установлена лишь более сильными средствами, чем ге, которые формализованы в данной системе. [20]
Обратите внимание, что этот метод не гарантирует решения, так как внутри системы может не существовать способа установить, что Principia Mathematica - формальная арифметика. Это, однако, означает не то, что задача или подзадача являются ложными утверждениями, а лишь то, что они не могут быть получены на основании сведений, имеющихся в распоряжении системы в данный момент. Тот факт, что некоторые вопросы остаются открытыми, разумеется, подобен неполноте, от которой страдают некоторые хорошо известные формальные системы. [21]
Зм ( иеу) Л V ( иеу - uez)) - y z, допускающей много пустых множеств, а аксиомы свертывания NF оставить без изменения, то получится довольно слабая теория, именно: уже в формальной арифметике можно доказать непротиворечивость полученной системы. [22]
Под квантором Зу стоит нумерически разрешимая формула ( § 41, ( D)), следовательно, в силу результата Новикова, - 3y ( R ( w, у) V 5 ( я, у)) в интуиционистской формальной арифметике - и более того, из доказательства этого результата видно, что - R ( я, /) V S ( n, /) для некоторой цифры /, которая находится по я эффективно. [23]
Изданной в Брауншвейге в 1888 г. Следует отметить, что после обнаружения парадоксов теории множеств, а особенно после установленной Геделем неполноты формальной арифметики надежды Дедекинда и Гильберта о решении проблемы непротиворечивости арифметики натуральных чисел не оправдались: непротиворечивость формальной системы, включающей формальную арифметику, может быть установлена лишь более сильными средствами, чем ге, которые формализованы в данной системе. [24]
В результате отбора в книгу включены следующие основные разделы: теория алгоритмов ( включая программирование для универсальных электронных цифровых машин и универсальные алгоритмические языки для программирования), теория дискретных автоматов ( включая теорию булевых функций и понятие о принципах построения универсальных электронных цифровых машин), теория дискретных самоорганизующихся систем ( включая элементы теории оптимальных решений) и, наконец, математическая логика ( исчисление высказываний, узкое исчисление предикатов и формальная арифметика), рассматриваемая как база для автоматизации процесса построения дедуктивных ( основанных на той или иной системе аксиом) теорий. [25]
Докажем, что любое конечное подмножество множества Т имеет модель. Дополним стандартную интерпретацию ОТ языка формальной арифметики до интерпретации расширенной сигнатуры, положив с га. Очевидно, эта интерпретация является моделью множества А. Значит, каждое конечное подмножество ACT имеет модель. По теореме 13 множество Т имеет модель, следовательно, имеет счетную модель. Докажем, что модели ШТ и ОТ не изоморфны. Рассмотрим элемент с Е М, являющийся интерпретацией константы с в модели ШТ. [26]
А может быть, любая теория неразрешима. На первый вопрос ответ положительный - формальная арифметика неразрешима, а множество ее аксиом, очевидно, разрешимо. [27]
Соединив два терма знаком равенства, получим некоторое высказывание, истинное или ложное в зависимости от того, верно или неверно указанное равенство. Все подобные высказывания составляют набор так называемых элементарных формул формальной арифметики. Если в составляющих высказывание термах содержатся переменные, то оно ( это высказывание) будет представлять собой некоторый предикат, который естественно назвать элементарным арифметическим предикатом. Из подобных элементарных предикатов с помощью операций ( узкого) исчисления предикатов ( включая операции связывания кванторами) строятся более сложные арифметические предикаты. Все предикаты, которые можно построить таким способом, называются арифметическими по Геделю. [28]
Оказывается, что при некоторых дополнительных пред-положениях из указанного свойства формулы Vy iA p, у) вытекает ее неразрешимость, что и доказывает неполноту построенной нами формальной арифметической системы. Дополнительное предположение, о котором здесь идет речь, сводится к тому, что формальная арифметика предполагается со-непротиворечивой. [29]
Формулы являются аналогами повествовательных предложений естественного языка, однако не все они выражают В. Так, формула языка формальной арифметики я 24 не выражает истинное или ложное В. [30]