 | Эта статья включает в себя список литературы , связанной литературы или внешних ссылок , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . ( Ноябрь 2017 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) |
В теории доказательства раздел математической логики , арифметика элементарных функций ( EFA ), также называемая элементарной арифметикой и арифметикой экспоненциальных функций , представляет собой систему арифметики с обычными элементарными свойствами 0, 1, +, ×, x y вместе с индукция для формул с ограниченными кванторами .
EFA - очень слабая логическая система, чей теоретический порядковый номер доказательства равен ω 3 , но все же кажется способным доказать большую часть обычной математики, которая может быть сформулирована на языке арифметики первого порядка .
Определение [ править ]
EFA - это система с логикой первого порядка (с равенством). Его язык содержит:
- две константы 0, 1,
- три бинарные операции +, ×, exp, где exp ( x , y ) обычно записывается как x y ,
- символ двоичного отношения <(в этом нет необходимости, поскольку он может быть записан в терминах других операций и иногда опускается, но удобен для определения ограниченных кванторов).
Ограниченные кванторы - это кванторы вида (x <y) и ∃ (x <y), которые являются сокращениями для ∀ x (x <y) →… и ∃x (x <y) ∧… обычным способом.
Аксиомы ОДВ таковы:
- Аксиомы арифметики Робинсона для 0, 1, +, ×, <
- Аксиомы возведения в степень: x 0 = 1, x y +1 = x y × x .
- Индукция для формул, все кванторы которых ограничены (но могут содержать свободные переменные).
Великая гипотеза Фридмана [ править ]
Харви Фридман «s великая гипотеза предполагает , что многие математические теоремы, такие как Великая теорема Ферма , можно доказать в очень слабых системах , такие как О.
Исходное утверждение гипотезы Фридмана (1999) таково:
- «Каждая теорема, опубликованная в Annals of Mathematics , утверждение которой включает только конечные математические объекты (то есть то, что логики называют арифметическим утверждением), может быть доказана в EFA. EFA - это слабый фрагмент арифметики Пеано, основанный на обычных бескванторных аксиомах для 0 , 1, +, ×, exp, вместе со схемой индукции для всех формул языка, все кванторы которых ограничены ».
Хотя легко построить искусственные арифметические утверждения, которые являются истинными, но не доказуемыми в EFA [ необходим пример ] , суть гипотезы Фридмана состоит в том, что естественные примеры таких утверждений в математике кажутся редкими. Некоторые естественные примеры включают утверждения о согласованности из логики, несколько утверждений, связанных с теорией Рамсея, такие как лемма Семереди о регулярности и теорема о миноре графа .
Связанные системы [ править ]
Несколько связанных классов вычислительной сложности имеют свойства, аналогичные EFA:
- Можно опустить символ двоичной функции exp из языка, взяв арифметику Робинсона вместе с индукцией для всех формул с ограниченными кванторами и аксиомой, грубо заявляющей, что возведение в степень - это функция, определенная всюду. Это похоже на EFA и имеет такую же теоретическую силу доказательства, но с ним более громоздко работать.
- Есть слабые фрагменты арифметики второго порядка, называемые RCA.*
0 и WKL*
0 которые имеют ту же прочность, что и EFA, и консервативны по сравнению с0
2предложения [ требуется дальнейшее объяснение ] , которые иногда изучаются в обратной математике ( Simpson 2009 ).
- Элементарная рекурсивная арифметика ( ERA ) - это подсистема примитивной рекурсивной арифметики (PRA), в которой рекурсия ограничена ограниченными суммами и произведениями . Это тоже есть Π0
2предложения как EFA, в том смысле, что всякий раз, когда EFA доказывает ∀x∃y P ( x , y ), с P без кванторов, ERA доказывает открытую формулу P ( x , T ( x )), с T термином, определяемым в ERA . Как и PRA, ERA может быть определено полностью без логики [ требуется пояснение ] способом, с использованием только правил подстановки и индукции и определения уравнений для всех элементарных рекурсивных функций. Однако, в отличие от PRA, элементарные рекурсивные функции можно охарактеризовать замыканием по композиции и проекции конечного количество базисных функций, и, следовательно, требуется только конечное число определяющих уравнений.
См. Также [ править ]
Ссылки [ править ]
- Avigad, Джереми (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, MR 1723993
