Элементарная функциональная арифметика

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

В теории доказательств , разделе математической логики , элементарная функциональная арифметика ( ЭФА ), также называемая элементарной арифметикой и арифметикой показательных функций , ^[1] представляет собой систему арифметики с обычными элементарными свойствами 0, 1, +, ×,  вместе с индукцией для формул с ограниченными кванторами .${\displaystyle x^{y}}$

EFA — очень слабая логическая система, доказательство которой — теоретико-ординальное число , но, тем не менее, она, по-видимому, способна доказать большую часть обычной математики, которую можно сформулировать на языке арифметики первого порядка .${\displaystyle \омега ^{3}}$

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

• две константы , ,${\displaystyle 0}$${\displaystyle 1}$
• три бинарные операции , , , обычно записываемые как ,${\displaystyle +}$${\displaystyle \times}$${\displaystyle {\textrm {exp}}}$${\displaystyle {\textrm {exp}}(x,y)}$${\displaystyle x^{y}}$
• символ бинарного отношения (на самом деле это не обязательно, так как его можно записать в терминах других операций и иногда его опускают, но он удобен для определения ограниченных квантификаторов).${\стиль_отображения <}$

Ограниченные квантификаторы — это квантификаторы формы и , которые являются сокращениями для и в обычном смысле.${\displaystyle \forall (x<y)}$${\displaystyle \существует (x<y)}$${\displaystyle \forall x(x<y)\rightarrow \ldots }$${\displaystyle \exists x(x<y)\land \ldots }$

Аксиомы EFA таковы:

• Аксиомы арифметики Робинсона для , , , ,${\displaystyle 0}$${\displaystyle 1}$${\displaystyle +}$${\displaystyle \times}$${\стиль_отображения <}$
• Аксиомы возведения в степень: , .${\displaystyle x^{0}=1}$${\displaystyle x^{y+1}=x^{y}\times x}$
• Индукция для формул, все кванторы которых ограничены (но которые могут содержать свободные переменные).

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

Первоначальное утверждение гипотезы Фридмана (1999) выглядит следующим образом:

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

Хотя легко построить искусственные арифметические утверждения, которые истинны, но недоказуемы в EFA, суть гипотезы Фридмана в том, что естественные примеры таких утверждений в математике, по-видимому, редки. Некоторые естественные примеры включают утверждения о согласованности из логики, несколько утверждений, связанных с теорией Рамсея, такие как лемма о регулярности Семереди и теорема о миноре графа .

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

• Можно исключить из языка символ бинарной функции exp, взяв арифметику Робинсона вместе с индукцией для всех формул с ограниченными кванторами и аксиомой, утверждающей, что возведение в степень — это функция, определенная везде. Это похоже на EFA и имеет ту же силу доказательства теории, но с этим сложнее работать.
• Существуют слабые фрагменты арифметики второго порядка, называемые и , которые консервативны по отношению к EFA для предложений (т. е. любые предложения, доказанные или уже доказанные EFA.) ^[2] В частности, они консервативны для утверждений о согласованности. Эти фрагменты иногда изучаются в обратной математике (Simpson 2009).${\displaystyle {\mathsf {RCA}}_{0}^{*}}$${\displaystyle {\mathsf {WKL}}_{0}^{*}}$${\displaystyle \Пи _{2}^{0}}$${\displaystyle \Пи _{2}^{0}}$${\displaystyle {\mathsf {RCA}}_{0}^{*}}$${\displaystyle {\mathsf {WKL}}_{0}^{*}}$
• Элементарная рекурсивная арифметика ( ERA ) — это подсистема примитивной рекурсивной арифметики (PRA), в которой рекурсия ограничена ограниченными суммами и произведениями . Она также имеет те же предложения, что и EFA, в том смысле, что всякий раз, когда EFA доказывает ∀x∃y P ( x , y ), с P без кванторов, ERA доказывает открытую формулу P ( x , T ( x )), с T — термином, определяемым в ERA. Как и PRA, ERA может быть определена полностью логически свободным ^{[ требуется разъяснение ]} образом, только с правилами подстановки и индукции и определяющими уравнениями для всех элементарных рекурсивных функций. Однако, в отличие от PRA, элементарные рекурсивные функции могут быть охарактеризованы замыканием относительно композиции и проекции конечного числа базисных функций, и, таким образом, требуется только конечное число определяющих уравнений.${\displaystyle \Пи _{2}^{0}}$

• Элементарная функция  – Математическая функция
• Иерархия Гжегорчика  – Функции в теории вычислимости
• Обратная математика  – Раздел математической логики
• Порядковый анализ  – математический метод, используемый в теории доказательств.
• Школьная задача по алгебре Тарского  - Математическая задача

• Авигад, Джереми (2003), «Теория чисел и элементарная арифметика», Philosophia Mathematica , Series III, 11 (3): 257–284 , doi : 10.1093/philmat/11.3.257, ISSN  0031-8019, MR  2006194
• Фридман, Харви (1999), Великие гипотезы
• Симпсон, Стивен Г. (2009), Подсистемы арифметики второго порядка, Перспективы в логике (2-е изд.), Cambridge University Press , ISBN 978-0-521-88439-6, г-н  1723993