Aritmetika základních funkcí - Elementary function arithmetic - Wikipedia

v teorie důkazů, pobočka matematická logika, aritmetika základních funkcí (EFA), také zvaný základní aritmetika a aritmetika exponenciální funkce, je systém aritmetiky s obvyklými elementárními vlastnostmi 0, 1, +, ×,X^y, dohromady s indukce pro vzorce s omezené kvantifikátory.

EFA je velmi slabý logický systém, jehož důkaz teoretický ordinál je ω³, ale stále se zdá být schopen dokázat hodně z běžné matematiky, kterou lze uvést v jazyce aritmetika prvního řádu.

Definice

EFA je systém v logice prvního řádu (s rovností). Jeho jazyk obsahuje:

dvě konstanty 0, 1,
tři binární operace +, ×, exp, s exp (X,y) obvykle psáno jako X^y,
symbol binární relace <(To není opravdu nutné, protože to může být napsáno z hlediska ostatních operací a je někdy vynecháno, ale je to vhodné pro definování omezených kvantifikátorů).

Omezené kvantifikátory jsou ty ve tvaru ∀ (x

Axiomy EFA jsou

Axiomy Robinsonova aritmetika pro 0, 1, +, ×, <
Axiomy pro umocňování: X⁰ = 1, X^y+1 = X^y × X.
Indukce pro vzorce, jejichž kvantifikátory jsou omezené (ale které mohou obsahovat volné proměnné).

Friedmanova velká domněnka

Harvey Friedman je velký dohad znamená, že mnoho matematických vět, jako např Fermatova poslední věta, lze prokázat ve velmi slabých systémech, jako je EFA.

Původní tvrzení domněnky z Friedman (1999) je:

"Každá věta publikovaná v Annals of Mathematics jehož prohlášení zahrnuje pouze konečné matematické objekty (tj. to, co logici nazývají aritmetické tvrzení) lze dokázat v EFA. EFA je slabý fragment Peano aritmetika na základě obvyklých axiomů bez kvantifikátoru pro 0, 1, +, ×, exp, společně se schématem indukce pro všechny vzorce v jazyce, jejichž kvantifikátory jsou omezené. “

I když je snadné vytvářet umělé aritmetické výroky, které jsou pravdivé, ale v EFA neprokazatelné^{[potřebný příklad ]}, jde o Friedmanovu domněnku, že přirozené příklady takových výroků v matematice se zdají být vzácné. Některé přirozené příklady zahrnují příkazy konzistence z logiky, několik příkazů souvisejících s Ramseyova teorie tak jako Szemerédiho pravidelnost lemma a věta o grafu.

Související systémy

Několik souvisejících tříd výpočetní složitosti má podobné vlastnosti jako EFA:

Jeden může vynechat binární funkční symbol exp z jazyka tím, že vezme Robinsonovu aritmetiku spolu s indukcí pro všechny vzorce s omezenými kvantifikátory a axiomem zhruba uvádějícím, že umocňování je funkce definovaná všude. Je to podobné jako EFA a má stejnou teoretickou sílu důkazu, ale je těžší s ním pracovat.

Existují slabé fragmenty aritmetiky druhého řádu zvané RCA^*
₀ a WKL^*
₀ které mají stejnou sílu konzistence jako EFA a jsou pro ni konzervativní⁰
₂ věty^{[je třeba další vysvětlení ]}, které jsou někdy studovány v reverzní matematika (Simpson 2009 ).

Elementární rekurzivní aritmetika (ÉRA) je subsystém z primitivní rekurzivní aritmetika (PRA), ve kterém je rekurze omezena na vázané částky a produkty. Toto má také stejný Π⁰
₂ věty jako EFA, v tom smyslu, že kdykoli se EFA ukáže ∀x∃y P(X,y), s P bez kvantifikátoru, ERA dokazuje otevřený vzorec P(X,T(X)), s T termín definovatelný v ERA. Stejně jako PRA lze ERA definovat zcela logicky^{[je zapotřebí objasnění ]} způsobem, pouze s pravidly substituce a indukce a definováním rovnic pro všechny základní rekurzivní funkce. Na rozdíl od PRA však lze elementární rekurzivní funkce charakterizovat uzavřením pod kompozicí a projekcí a konečný počet základních funkcí, a proto je zapotřebí pouze konečný počet definujících rovnic.

Viz také

Reference

Avigad, Jeremy (2003), „Teorie čísel a elementární aritmetika“, Philosophia Mathematica, Řada III, 11 (3): 257–284, doi:10.1093 / philmat / 11.3.257, ISSN 0031-8019, PAN 2006194
Friedman, Harvey (1999), velké domněnky
Simpson, Stephen G. (2009), Podsystémy aritmetiky druhého řádu, Perspectives in Logic (2. vyd.), Cambridge University Press, ISBN 978-0-521-88439-6, PAN 1723993