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

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

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

Определение [ править ]

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

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

Ограниченные кванторы имеют вид $\forall (x<y)$ и $\exists (x<y)$ которые являются аббревиатурами $\forall x(x<y)\rightarrow \ldots$ и $\exists x(x<y)\land \ldots$ обычным способом.

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

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

Великая гипотеза Фридмана [ править ]

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

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

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

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

Связанные системы [ править ]

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

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

См. также [ править ]

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

Ссылки [ править ]

^ К. Смориньский, «Нестандартные модели и связанные с ними разработки» (стр. 217). Из исследования Харви Фридмана по основам математики (1985), « Исследования по логике и основам математики», том. 117.
^ С.Г. Симпсон, Р.Л. Смит, « Факторизация полиномов и $\Sigma _{1}^{0}$ -индукция » (1986). Анналы чистой и прикладной логики, т. 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

[1] К. Смориньский, «Нестандартные модели и связанные с ними разработки» (стр. 217). Из исследования Харви Фридмана по основам математики (1985), « Исследования по логике и основам математики», том. 117.

[2] С.Г. Симпсон, Р.Л. Смит, « Факторизация полиномов и $\Sigma _{1}^{0}$ -индукция » (1986). Анналы чистой и прикладной логики, т. 31 (с.305)

[1]

[2]