Арифметика элементарных функций - Elementary function arithmetic - Wikipedia

Эта статья включает Список ссылок, связанное чтение или внешняя ссылка, но его источники остаются неясными, потому что в нем отсутствует встроенные цитаты. Пожалуйста, помогите улучшать эта статья введение более точные цитаты. (Ноябрь 2017 г.) (Узнайте, как и когда удалить этот шаблон сообщения)

В теория доказательств, филиал математическая логика, арифметика элементарных функций (ОДВ), также называемый элементарная арифметика и арифметика с экспоненциальной функцией, - система арифметики с обычными элементарными свойствами 0, 1, +, ×,Икс^у, вместе с индукция для формул с ограниченные кванторы.

ОДВ - очень слабая логическая система, ординал теории доказательства это ω³, но все еще кажется способным доказать большую часть обычной математики, которую можно сформулировать на языке арифметика первого порядка.

Определение

EFA - это система логики первого порядка (с равенством). Его язык содержит:

• две константы 0, 1,
• три бинарные операции +, ×, exp, с exp (Икс,у) обычно записывается как Икс^у,
• символ двоичного отношения <(в этом нет необходимости, так как он может быть записан в терминах других операций и иногда опускается, но удобен для определения ограниченных кванторов).

Ограниченные кванторы имеют вид ∀ (x

Аксиомы ОДВ таковы:

• Аксиомы Арифметика Робинсона для 0, 1, +, ×, <
• Аксиомы возведения в степень: Икс⁰ = 1, Икс^у+1 = Икс^у × Икс.
• Индукция для формул, все кванторы которых ограничены (но могут содержать свободные переменные).

Грандиозная гипотеза Фридмана

Харви Фридман с великая догадка означает, что многие математические теоремы, такие как Последняя теорема Ферма, может быть доказано в очень слабых системах, таких как EFA.

Исходное утверждение гипотезы из Фридман (1999) является:

"Каждая теорема, опубликованная в Анналы математики утверждение которого включает только конечные математические объекты (то есть то, что логики называют арифметическим утверждением), может быть доказано в EFA. EFA - слабый фрагмент Арифметика Пеано на основе обычных бескванторных аксиом для 0, 1, +, ×, exp вместе со схемой индукция для всех формул языка, все кванторы которых ограничены ».

Хотя легко построить искусственные арифметические утверждения, которые верны, но не доказуемы в EFA^{[пример необходим ]}, суть гипотезы Фридмана в том, что естественные примеры таких утверждений в математике кажутся редкими. Некоторые естественные примеры включают утверждения последовательности из логики, несколько утверждений, связанных с Теория Рамсея такой как Лемма Семереди о регулярности и малая теорема о графике.

Связанные системы

Несколько связанных классов вычислительной сложности имеют свойства, аналогичные EFA:

• Можно опустить символ двоичной функции exp из языка, взяв арифметику Робинсона вместе с индукцией для всех формул с ограниченными кванторами и аксиомой, примерно утверждающей, что возведение в степень - это функция, определенная везде. Это похоже на EFA и имеет такую ​​же теоретическую силу доказательства, но с ним труднее работать.

• Есть слабые фрагменты арифметики второго порядка, называемые RCA.^*
  ₀ и WKL^*
  ₀ которые имеют такую ​​же стойкость, что и EFA, но консервативны по сравнению с⁰
  ₂ фразы^{[требуется дальнейшее объяснение ]}, которые иногда изучаются в обратная математика (Симпсон 2009 ).

• Элементарная рекурсивная арифметика (ЭРА) является подсистемой примитивная рекурсивная арифметика (PRA), в котором рекурсия ограничена ограниченные суммы и продукты. Это тоже есть Π⁰
  ₂ предложения как EFA, в том смысле, что всякий раз, когда EFA доказывает ∀x∃y п(Икс,у), с п без кванторов, ERA доказывает открытую формулу п(Икс,Т(Икс)), с Т термин, определяемый в ERA. Как и PRA, ERA может быть определено в полностью лишенном логики^{[требуется разъяснение ]} таким образом, используя только правила подстановки и индукции, и определяя уравнения для всех элементарных рекурсивных функций. Однако, в отличие от PRA, элементарные рекурсивные функции могут быть охарактеризованы замыканием по композиции и проекции конечный количество базисных функций, и, следовательно, требуется только конечное число определяющих уравнений.

Смотрите также

• Иерархия Гжегорчика
• Обратная математика
• Порядковый анализ
• Проблема алгебры средней школы Тарского

Рекомендации

• Авигад, Джереми (2003), "Теория чисел и элементарная арифметика", Философия Математики, Серия III, 11 (3): 257–284, Дои:10.1093 / philmat / 11.3.257, ISSN  0031-8019, МИСТЕР  2006194
• Фридман, Харви (1999), грандиозные догадки
• Симпсон, Стивен Г. (2009), Подсистемы арифметики второго порядка, Перспективы в логике (2-е изд.), Издательство Кембриджского университета, ISBN  978-0-521-88439-6, МИСТЕР  1723993