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

Система арифметики в теории доказательств

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

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

Определение

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

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

Ограниченные квантификаторы — это квантификаторы формы и , которые являются сокращениями для и в обычном смысле. ${\displaystyle \forall (x<y)}$ ${\displaystyle \exists (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 <}$
• Аксиомы возведения в степень: , . ${\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 \Pi _{2}^{0}}$ ${\displaystyle \Pi _{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 \Pi _{2}^{0}}$

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

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

Ссылки

1. C. Smoryński, "Нестандартные модели и связанные с ними разработки" (стр. 217). Из книги Харви Фридмана "Исследования по основам математики" (1985), Исследования по логике и основам математики, т. 117.
2. SG Simpson, RL Smith, "Факторизация многочленов и Σ 1 0 {\displaystyle \Sigma _{1}^{0}} -индукция" (1986). Annals of Pure and Applied Logic, т. 31 (стр. 305)

• Авигад, Джереми (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