Arytmetyka funkcji elementarnych

„Elementarna arytmetyka rekurencyjna” przekierowuje tutaj. Aby zapoznać się z klasą złożoności obliczeniowej, zobacz ELEMENTARY .

W teorii dowodu , gałąź logiki matematycznej , elementarna arytmetyka funkcji ( EFA ), zwana także elementarną arytmetyką i arytmetyką funkcji wykładniczych , to system arytmetyczny ze zwykłymi elementarnymi właściwościami 0, 1, +, ×, x ^y , wraz z indukcja dla wzorów z kwantyfikatorami ograniczonymi .

EFA jest bardzo słabym systemem logicznym, którego teoretyczna liczba porządkowa dowodu wynosi ω ³ , ale nadal wydaje się być w stanie udowodnić wiele ze zwykłej matematyki, którą można wyrazić językiem arytmetyki pierwszego rzędu .

Definicja

EFA to system w logice pierwszego rzędu (z równością). Jego język zawiera:

• dwie stałe 0, 1,
• trzy operacje binarne +, ×, exp, z exp( x , y ) zwykle zapisywane jako x ^y ,
• symbol relacji binarnej < (Nie jest to tak naprawdę konieczne, ponieważ można to zapisać w kategoriach innych operacji i czasami jest pomijane, ale jest wygodne do definiowania kwantyfikatorów ograniczonych).

Ograniczone kwantyfikatory to kwantyfikatory postaci ∀ (x < y) i ∃ (x < y) , które są skrótami dla ∀ x (x < y) → ... i ∃ x ( x < y) ∧ ... w zwykłym sposób.

Aksjomatami EFA są

• Aksjomaty arytmetyki Robinsona dla 0, 1, +, ×, <
• ⁰ Aksjomaty potęgowania: x = 1, x ^{y +1} = x ^y × x .
• Indukcja dla formuł, których wszystkie kwantyfikatory są ograniczone (ale które mogą zawierać zmienne wolne).

Wielkie przypuszczenie Friedmana

Wielka hipoteza Harveya Friedmana implikuje, że wiele twierdzeń matematycznych, takich jak ostatnie twierdzenie Fermata , można udowodnić w bardzo słabych systemach, takich jak EFA.

Oryginalne stwierdzenie hipotezy Friedmana (1999) brzmi:

„Każde twierdzenie opublikowane w Annals of Mathematics , którego twierdzenie dotyczy tylko skończonych obiektów matematycznych (tj. tego, co logicy nazywają twierdzeniem arytmetycznym), można udowodnić w EFA. EFA jest słabym fragmentem arytmetyki Peano , opartej na zwykłych aksjomatach wolnych od kwantyfikatorów dla 0 , 1, +, ×, exp, wraz ze schematem indukcji dla wszystkich formuł w języku, którego wszystkie kwantyfikatory są ograniczone”.

Chociaż łatwo jest skonstruować sztuczne zdania arytmetyczne, które są prawdziwe, ale nie do udowodnienia w EFA, celem przypuszczenia Friedmana jest to, że naturalne przykłady takich zdań w matematyce wydają się rzadkie. Niektóre naturalne przykłady obejmują twierdzenia o spójności z logiki, kilka stwierdzeń związanych z teorią Ramseya , takich jak lemat o regularności Szemerédiego i twierdzenie o grafie minor .

Powiązane systemy

Kilka powiązanych klas złożoności obliczeniowej ma podobne właściwości do EFA:

• Można pominąć symbol funkcji binarnej exp z języka, biorąc arytmetykę Robinsona razem z indukcją dla wszystkich formuł z kwantyfikatorami ograniczonymi i aksjomatem stwierdzającym z grubsza, że ​​potęgowanie jest funkcją definiowaną wszędzie. Jest to podobne do EFA i ma taką samą teoretyczną siłę dowodu, ale jest bardziej kłopotliwe w pracy.
• Istnieją słabe fragmenty arytmetyki drugiego rzędu zwane RCA ^*
  ₀ i WKL ^*
  ₀ , które mają taką samą siłę spójności jak EFA i są konserwatywne w stosunku do niej dla zdań Π ⁰
  ₂ , które są czasami badane w matematyce odwrotnej ( Simpson 2009 ).
• Elementarna arytmetyka rekurencyjna ( ERA ) to podsystem prymitywnej arytmetyki rekurencyjnej (PRA), w którym rekurencja jest ograniczona do ograniczonych sum i produktów . Ma to również takie same zdania Π ⁰
  ₂ jak EFA, w tym sensie, że ilekroć EFA dowodzi ∀x∃y P ( x , y ), z wolnym od kwantyfikatora P , ERA dowodzi formuły otwartej P ( x , T ( x )), gdzie T jest terminem definiowanym w ERA. Podobnie jak PRA, ERA można zdefiniować w sposób całkowicie wolny od logiki , stosując tylko zasady podstawienia i indukcji oraz definiując równania dla wszystkich elementarnych funkcji rekurencyjnych. Jednak w przeciwieństwie do PRA, elementarne funkcje rekurencyjne można scharakteryzować przez zamknięcie pod składem i rzutowanie skończonej liczby funkcji bazowych, a zatem potrzebna jest tylko skończona liczba równań definiujących.

Zobacz też

• Funkcja elementarna – Funkcja matematyczna
• Hierarchia Grzegorczyka – Funkcje w teorii obliczalności
• Matematyka odwrotna - Gałąź logiki matematycznej
• Analiza porządkowa - technika matematyczna stosowana w teorii dowodów
• Zadanie algebry Tarskiego w szkole średniej – zadanie matematyczne

•    Avigad, Jeremy (2003), „Teoria liczb i elementarna arytmetyka”, Philosophia Mathematica , seria III, 11 (3): 257–284, doi : 10.1093/philmat/11.3.257 , ISSN 0031-8019 , MR 2006194
• Friedman, Harvey (1999), wielkie przypuszczenia
•    Simpson, Stephen G. (2009), Podsystemy arytmetyki drugiego rzędu , Perspectives in Logic (wyd. 2), Cambridge University Press , ISBN 978-0-521-88439-6 , MR 1723993