Формальная арифметика

Большая Советская Энциклопедия. Статьи для написания рефератов, курсовых работ, научные статьи, биографии, очерки, аннотации, описания.


А Б В Г Д Е Ё Ж З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Ъ Ы Ь Э Ю Я 1 2 3 4 8 A L M P S T X
ФА ФБ ФЕ ФЁ ФЗ ФИ ФЛ ФО ФР ФТ ФУ ФЫ ФЬ ФЭ ФЮ
ФОБ
ФОВ
ФОГ
ФОД
ФОЙ
ФОК
ФОЛ
ФОМ
ФОН
ФОР
ФОС
ФОТ
ФОФ
ФОХ
ФОШ

Формальная арифметика, формулировка арифметики в виде формальной (аксиоматической) системы (см. Аксиоматический метод). Язык Формальная арифметика содержит константу 0, числовые переменные, символ равенства, функциональные символы +, •, ' (прибавление 1) и логические связки (см. Логические операции). Постулатами Формальная арифметика являются аксиомы и правила вывода исчисления предикатов (классического или интуиционистского в зависимости от того, какая Формальная арифметика рассматривается), определяющие равенства для арифметических операций: а + 0 = а, а + b’ = (а + b), а •0 = 0, а •b’ = (а•b) + а,

аксиомы Пеано: ù(а’ = 0), a’= b’®а = b, (a = b & а = с) ®b = с, а = b®a' = b'

и схема аксиом индукции: А (0) & "x (А (х) ®А (x')) ®"xa (x).

  Средства Формальная арифметика достаточны для вывода теорем элементарной теории чисел. В настоящее время, по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, которая не была бы выводима в Формальная арифметика В Формальная арифметика изобразимы рекурсивные функции и доказуемы их определяющие равенства. Это позволяет, в частности, формулировать суждения о конечных множествах. Более того, Формальная арифметика эквивалентна аксиоматической теории множеств Цермело – Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой.

  Формальная арифметика удовлетворяет условиям обеих теорем Гёделя о неполноте. В частности, имеются такие полиномы Р, Q от 9 переменных, что формула "x1..."x9 (P¹Q) невыводима, хотя и выражает истинное суждение, а именно непротиворечивость Формальная арифметика Поэтому неразрешимость диофантова уравнения Р Q = 0 недоказуема в Формальная арифметика Непротиворечивость Формальная арифметика доказана с помощью трасфинитной индукции до ординала e0 (наименьшее решение уравнения we = e). Поэтому схема индукции до e0 недоказуема в Формальная арифметика, хотя там доказуема схема индукции до любого ординала a < e0. Класс доказуемо рекурсивных функций Формальная арифметика (т. е. частично рекурсивных функций, общерекурсивность которых может быть установлена средствами Формальная арифметика) совпадает с классом ординально рекурсивных функций с ординалами < e0.

  Не все теоретико-числовые предикаты выразимы в Формальная арифметика: примером является такой предикат T, что для любой замкнутой арифметической формулы А имеет место Т (éАù) «А, где éАù – номер формулы А в некоторой фиксированной нумерации, удовлетворяющей естественным условиям. Присоединение к Формальная арифметика символа Т с аксиомами типа Т (éА & Bù) «Т (éАù) & Т (éBù),

выражающими его перестановочность с логическими связками, позволяет доказать непротиворечивость Формальная арифметика Похожая конструкция (но уже внутри Формальная арифметика) доказывает, что схему индукции нельзя заменить никаким конечным множеством аксиом. Формальная арифметика корректна и полна относительно формул вида $x1... $xk(P = Q); замкнутая формула из этого класса доказуема тогда и только тогда, когда она истинна. Так как этот класс содержит алгоритмически неразрешимый предикат, отсюда следует, что проблема выводимости в Формальная арифметика алгоритмически неразрешима.

  При задании Формальная арифметика в виде генценовской системы осуществима нормализация выводов, причём нормальный вывод числового равенства состоит только из числовых равенств. На этом пути было получено первое доказательство непротиворечивости Формальная арифметика Нормальный вывод формулы с кванторами может содержать сколь угодно сложные формулы. Полная подформульность достигается после замены схемы индукции на со-правило, позволяющее вывести В ®"xA (x) из В®A (0), B ®A (1),... Понятие w-вывода (т. е. вывода с w-правилом) высоты < e0 выразимо в Формальная арифметика, поэтому переход к w-выводам позволяет устанавливать в Формальная арифметика многие метаматематические теоремы, в частности полноту относительно формул вида $x1... $xk (P = Q) и ординальную характеристику доказуемо рекурсивных функций.

 

  Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; Hilbert D., Bernays P., Grundlagen der Mathematik, 2 Aufl., Bd 1–2, В., 1968–70.

  Г. Е. Минц.

 

Так же Вы можете узнать о...


Таллахасси (Tallahassee), город на юго-востоке США, административный центр штата Флорида.
Цинхофен, атофан, лекарственный препарат, способствующий переходу мочевой кислоты из тканей в кровь и выведению её почками; усиливает секрецию жёлчи и желудочного сока; оказывает аналгезирующее действие.
Ариана (Arianc), введённое древнегреческим учёным Эратосфеном в античную литературу обозначение восточной части Иранского плато.
Восточно-Африканская зона разломов земной коры, система крупных разломов (сбросов) и грабенов (рифтов), развитых на фоне новейших поднятий Восточной Африки.
Женевская конференция 1927, конференция министров иностранных дел Бельгии, Великобритании, Германии, Италии, Франции и Японии; состоялась в Женеве 14—16 июня по инициативе английского министра иностранных дел О.
Координатно-измерительная машина в астрономии, прибор для измерения прямоугольных координат небесных объектов на астрофотографиях.
Минс Гардинер Минс (Means) Гардинер (р. 8.6.1896, Уиндем), американский экономист.
Пинакотека (греч. pinakotéke, от pinax — доска, картина и théke — хранилище), хранилище живописных произведений, картинная галерея.
Сергиев (прежнее назв. г. Загорска) Сергиев, с 1919 до 1930 название г. Загорска Московской области РСФСР.
Улики, см. Доказательства.
Элпидин Михаил Константинович (1835, с. Никольское Лаишевского у.
Бластоидеи (Blastoidea), морские бутоны, класс вымерших беспозвоночных животных типа иглокожих.
Горячегорск, посёлок городского типа в Шарыповском районе Красноярского края РСФСР.
Кабельные оконечные устройства, устройства для вывода токопроводящих жил кабелей связи на контакты, к которым подключаются соответствующие цепи аппаратуры связи.
Леньяно (Legnano), город в Италии (около 30 км северо-западнее Милана), в районе которого 29 мая 1176 произошло сражение между 12-тыс.