Cтраница 3
Гедель в своей теореме о неполноте формальной арифметики фактически установил ее омега-неполноту. Мели и качестве аксиом взять множество всех формул, истинных в стандартной модели арифметики, то получится омега-полная аксноматич. Наоборот, но всяком омега-полном расширении арифметики Пеано выводима всякая истинная в стандарт ной модели формула. [31]
Отсюда следует, что теория Th ( N, , , х) не является конечно аксиоматизируемой. Более того, это же рассуждение показывает, что не существует разрешимого множества теорем этой теории, из которых бы выводились все другие теоремы. Отсюда следует, что классическая система аксиом формальной арифметики, называемая также арифметикой Пеано ( свойства арифметических операций плюс аксиомы индукции), не может быть полной: существуют истинные формулы, невыводимые в формальной арифметике. [32]
А, что ни А, ни - А не являются теоремами этой системы. А можно взять формулу, к-рая естественным образом выражает непротиворечивость формальной арифметики. [33]
Можно было бы подумать, что результат Геделя вскрывает лишь недостаточную полноту выбранной нами системы аксиом формальной арифметики и что при разумном пополнении этой системы аксиом новыми аксиомами неполнота арифметики ( при сохранении ее непротиворечивости) уже не будет иметь места. В действительности дело обстоит далеко не так просто. Как показывает подробный анализ, проведенный Геделем, при любом непротиворечивом расширении системы аксиом формальная арифметика продолжает оставаться неполной и в ней по-прежнему будут существовать неразрешимые замкнутые формулы. Более того, всякая формальная система, удовлетворяющая некоторым довольно общим условиям ( наличие достаточно богатого набора формул и объектов), в случае ее непротиворечивости будет обязательно неполной. [34]
Формализация, Метод аксиоматический), становится в ряде случаев предметом точного ( пользующегося матем. Следует, впрочем, отметить, что не всякое понятие II. С др. стороны, ряд результатов, важнейшим из к-рых безусловно является теорема Геделя о неполноте ( и непополнимости) формальной арифметики ( в этой связи весьма важны также результаты Черча и Тарского), послужили одним из стимулов к поискам более широких средств формализации науч. Изоморфизм, Категоричность системы аксиом), имеют разнообразные приложения, чем и определяется их науч. [35]
Допущение более широких ( но корректных с точки зрения брауэровского интуициониз ма) средств пришло позднее, особенно под влиянием результатов Геделя о неполноте. Генценовское доказательство непротиворечивости арифметики [10] показало, как можно примирить ограничения, налагаемые теоремой Геделя, с требованием фи-нитности: привлеченный Генценом принцип ( бескванторная индукция до е0), выходящий за рамки формальной арифметики первого порядка, формулируется в языке финитных предложений. [36]
Отсюда следует, что теория Th ( N, , , х) не является конечно аксиоматизируемой. Более того, это же рассуждение показывает, что не существует разрешимого множества теорем этой теории, из которых бы выводились все другие теоремы. Отсюда следует, что классическая система аксиом формальной арифметики, называемая также арифметикой Пеано ( свойства арифметических операций плюс аксиомы индукции), не может быть полной: существуют истинные формулы, невыводимые в формальной арифметике. [37]
Если всякая замкнутая формула данной формальной системы разрешима в ней, то такая система наз. Следует заметить, что нельзя требовать, чтобы в системе были разрешимы все формулы, а не только замкнутые. Так, формула х - 0, где х - переменная для натуральных чисел, не выражает ни истинное, ни ложное суждение, и поэтому ни она, ни ее отрицание не являются теоремами формальной арифметики. [38]
Секвенциальные методы имеют более широкую область применимости, чем теорема Эрбрана. Можно сказать, что генцено-эрбрановские методы знаменуют собой первый этап теории поиска логического вывода. При этом чаще всего удается построить исчисления со следующим свойством подформульности: в дереве вывода каждой формулы участвуют лишь ее подформулы. При устранении сечений из исчислений второго порядка и формальной арифметики можно получить существенную информацию о структуре выводов, хотя свойство подформульности не может быть обеспечено и реальный поиск вывода чрезвычайно затруднен. [39]
Теорема Тарского о неорпеделимости и связанные с ней вопросы приводятся в гл. Аддисона о неопределимости самого класса определимых множеств. Эта логика дает описание широкого класса независимых в формальной арифметике предложений, полученных комбинацией булевых связок и оператора доказуемости. [40]
Мостоеским н самим Тарским, играет важную роль в семантике. Тарского об истинности, согласно к-рой для широкого класса непротиворечивых формальных систем ( во всяком случае-включающего формальную арифметику и аксиоматич. [41]
Поясним смысл этих аксиом. Аксиомы Пеано Р1 и Р2 не нуждаются в специальной записи: их выполнимость обусловлена наличием в языке константы 0 и функционального символа S. Аксиомы A3 А6 естественным образом задают индуктивные определения операций сложения и умножения. Выражение А7 представляет собой схему аксиом: какова бы ни была формула А ( х) языка формальной арифметики, формула вида А7 является аксиомой. Таким образом, А7 представляет бесконечное множество аксиом. Заметим, однако, что схема аксиом А7 не вполне соответствует аксиоме Пеано Р5, поскольку последняя распространяется на любое из 2 свойств натуральных чисел, в то время как схема аксиом А7 имеет дело лишь со счетным числом свойств, записываемых формулами. Тем не менее, схему аксиом А7 принято называть принципом математической индукции. [42]
ГЕДЕЛЯ ИНТЕРПРЕТАЦИЯ интуиционистской арифметики - специальная операция, переводящая формулы интуиционистской арифметики в формулы вида jxyy А ( х, у, z), где х, у я z - наборы переменных по вычислимым функциям специального вида. При этом выводимые формулы переводятся в истинные формулы в смысле нек-рой четко описанной семантики. Эта интерпретация, к-рая была использована К. Godel) для нового доказательства непротиворечивости арифметики формальной, представляет также значительный интерес как нек-рая семантика для языка формальной арифметики. [43]
Применение этих логических законов сводится к К. Здесь следует указать следующий основополагающий результат П. С. Новикова, полученный в 1943 ( см. [5]): пусть для формулы А ( х) с одной переменной в конструктивной формальной арифметике выводимо A ( re) V 1 4 ( re) для каждого п и в классической арифметике выводимо ЗхА ( х); тогда формула ЗхА ( х) выводима и в конструктивной арифметике. В работе [6] было получено обоснование К. [44]
Россер показал [71], что можно построить пример формулы, неразрешимость которой устанавливается без предположения об со-непротиворечивости формальной арифметики. Для этого достаточно ее простой непротиворечивости. Формула, о которой здесь идет речь, строится следующим способом. Если обозначить эту формулу через Pq ( x) ( q - ее геделевский номер), то формула Pq ( q) представляет собой искомый пример формулы, неразрешимость которой устанавливается с помощью предположения о простой непротиворечивости формальной арифметики. [45]