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

Формальная арифметика
        формулировка арифметики в виде формальной (аксиоматической) системы (см. Аксиоматический метод). Язык Ф. а. содержит константу 0, числовые переменные, символ равенства, функциональные символы +, •, ' (прибавление 1) и логические связки (см. Логические операции). Постулатами Ф. а. являются аксиомы (См. Аксиома) и правила вывода (См. Правило вывода) исчисления предикатов (классического или интуиционистского в зависимости от того, какая Ф. а. рассматривается), определяющие равенства для арифметических операций:
         а + 0 = а, а + b’ = (а + b),
         а •0 = 0, аb’ = (аb) + а,
        аксиомы Пеано:
         ⌉(а’ = 0), a’= b’а = b,
         (a = b & а = с) → b = с, а = ba' = b'
        и схема аксиом индукции:
         А (0) & x (А (х) → А (x')) → xa (x).
         Средства Ф. а. достаточны для вывода теорем элементарной теории чисел. В настоящее время, по-видимому, неизвестно ни одной содержательной теоретико-числовой теоремы, доказанной без привлечения средств анализа, которая не была бы выводима в Ф. а. В Ф. а. изобразимы Рекурсивные функции и доказуемы их определяющие равенства. Это позволяет, в частности, формулировать суждения о конечных множествах. Более того, Ф. а. эквивалентна аксиоматической теории множеств (См. Аксиоматическая теория множеств) Цермело – Френкеля без аксиомы бесконечности: в каждой из этих систем может быть построена модель другой.
         Ф. а. удовлетворяет условиям обеих теорем Гёделя о неполноте. В частности, имеются такие полиномы Р, Q от 9 переменных, что формула x1... x9 (PQ) невыводима, хотя и выражает истинное суждение, а именно непротиворечивость Ф. а. Поэтому неразрешимость диофантова уравнения Р - Q = 0 недоказуема в Ф. а. Непротиворечивость Ф. а. доказана с помощью трасфинитной индукции до ординала ε0 (наименьшее решение уравнения ωε = ε). Поэтому схема индукции до ε0 недоказуема в Ф. а., хотя там доказуема схема индукции до любого ординала α < ε0. Класс доказуемо рекурсивных функций Ф. а. (т. е. частично рекурсивных функций, общерекурсивность которых может быть установлена средствами Ф. а.) совпадает с классом ординально рекурсивных функций с ординалами < ε0.
         Не все теоретико-числовые предикаты выразимы в Ф. а.: примером является такой предикат T, что для любой замкнутой арифметической формулы А имеет место Т (⌈А⌉) ↔ А, где ⌈А⌉ – номер формулы А в некоторой фиксированной нумерации, удовлетворяющей естественным условиям. Присоединение к Ф. а. символа Т с аксиомами типа
         Т (⌈А & B⌉) ↔ Т (⌈А⌉) & Т (⌈B⌉),
        выражающими его перестановочность с логическими связками, позволяет доказать непротиворечивость Ф. а. Похожая конструкция (но уже внутри Ф. а.) доказывает, что схему индукции нельзя заменить никаким конечным множеством аксиом. Ф. а. корректна и полна относительно формул вида ∃x1... ∃xk (P = Q); замкнутая формула из этого класса доказуема тогда и только тогда, когда она истинна. Так как этот класс содержит алгоритмически неразрешимый предикат, отсюда следует, что проблема выводимости в Ф. а. алгоритмически неразрешима.
         При задании Ф. а. в виде генценовской системы осуществима нормализация выводов, причём нормальный вывод числового равенства состоит только из числовых равенств. На этом пути было получено первое доказательство непротиворечивости Ф. а. Нормальный вывод формулы с кванторами может содержать сколь угодно сложные формулы. Полная подформульность достигается после замены схемы индукции на со-правило, позволяющее вывести В → ∀xA (x) из ВA (0), B A (1),... Понятие ω-вывода (т. е. вывода с ω-правилом) высоты < ε0 выразимо в Ф. а., поэтому переход к ω-выводам позволяет устанавливать в Ф. а. многие метаматематические теоремы, в частности полноту относительно формул вида ∃x1... xk (P = Q) и ординальную характеристику доказуемо рекурсивных функций.
         Лит.: Клини С. К., Введение в метаматематику, пер. с англ., М., 1957; Hilbert D., Bernays P., Grundlagen der Mathematik, 2 Aufl., Bd 1–2, В., 1968–70.
         Г. Е. Минц.

Большая советская энциклопедия. — М.: Советская энциклопедия. 1969—1978.

Смотреть что такое "Формальная арифметика" в других словарях:

  • Формальная арифметика — Аксиомы Пеано одна из систем аксиом для натуральных чисел. Аксиомы Пеано позволили формализовать арифметику. После введения аксиом стали возможны доказательства многих свойств натуральных и целых чисел, а также использование целых чисел для… …   Википедия

  • Арифметика — Ганс Себальд Бехам. Арифметика. XVI век Арифметика (др. греч. ἀ …   Википедия

  • Формальная система — (формальная теория, аксиоматическая теория)  результат строгой формализации теории, предполагающей полную абстракцию от смысла слов используемого языка, причем все условия, регулирующие употребление этих слов в теории, явно высказаны… …   Википедия

  • ФОРМАЛЬНАЯ ФИЛОСОФИЯ — существующая в течение тысячелетий тенденция философии к фундаментальному обобщению понятий и законов, присущих формальным аспектам частных философских наук: формальной логики, формальной онтологии, формальной этики (см. в наст. словаре ст. с… …   Современный философский словарь

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

  • АРИФМЕТИКА ФОРМАЛЬНАЯ — арифметическое исчисление, логико математич. исчисление, формализующее элементарную теорию чисел. Язык наиболее употребительного варианта А. ф. содержит константу 0, числовые переменные, символ равенства, функциональные символы (прибавление 1) и… …   Математическая энциклопедия

  • ГЕЙТИНГА ФОРМАЛЬНАЯ СИСТЕМА — Гейтипга исчисление, название трех формальных систем конструктивной логики, предложенных А. Рейтингом [1]. Первая из них гейтинговское, или интуиционистское, исчисление высказываний формализация принципов конструктивной логики высказываний;… …   Математическая энциклопедия

  • ЭЛЕМЕНТАРНАЯ АРИФМЕТИКА — тоже, что арифметика формальная …   Математическая энциклопедия

  • Теорема Гёделя о неполноте — У этого термина существуют и другие значения, см. Теорема Гёделя. Теорема Гёделя о неполноте и вторая теорема Гёделя[ 1]  две теоремы математической логики о принципиальных ограничениях формальной арифметики и, как следствие, всякой… …   Википедия

  • Теоремы Гёделя о неполноте — Теоремы Гёделя о неполноте  две теоремы математической логики о принципиальных ограничениях формальной арифметики и, как следствие, всякой достаточно сильной[1] теории первого порядка. Первая теорема утверждает, что если формальная… …   Википедия

Книги



Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»