Aritmetica delle funzioni elementari - Elementary function arithmetic

"Aritmetica ricorsiva elementare" reindirizza qui. Per la classe di complessità computazionale, vedere ELEMENTARY .

Nella teoria della dimostrazione , una branca della logica matematica , l'aritmetica delle funzioni elementari ( EFA ), chiamata anche aritmetica elementare e aritmetica delle funzioni esponenziali , è il sistema dell'aritmetica con le solite proprietà elementari di 0, 1, +, ×,  x y , insieme a induzione per formule con quantificatori limitati .

EFA è un sistema logico molto debole, il cui ordinale teorico della dimostrazione è ω 3 , ma sembra ancora in grado di dimostrare gran parte della matematica ordinaria che può essere enunciata nel linguaggio dell'aritmetica del primo ordine .

Definizione

EFA è un sistema in logica di prim'ordine (con uguaglianza). La sua lingua contiene:

  • due costanti 0, 1,
  • tre operazioni binarie +, ×, exp, con exp( x , y ) solitamente scritto come x y ,
  • un simbolo di relazione binaria < (Questo non è realmente necessario in quanto può essere scritto nei termini delle altre operazioni e talvolta viene omesso, ma è conveniente per definire quantificatori limitati).

I quantificatori limitati sono quelli della forma ∀(x<y) e ∃ (x<y) che sono abbreviazioni di ∀ x (x<y)→... e ∃x (x<y)∧... nel solito modo.

Gli assiomi di EFA sono

  • Gli assiomi dell'aritmetica di Robinson per 0, 1, +, ×, <
  • Gli assiomi per l'elevamento a potenza: x 0 = 1, x y +1 = x y × x .
  • Induzione per formule i cui quantificatori sono tutti limitati (ma che possono contenere variabili libere).

La grande congettura di Friedman

La grande congettura di Harvey Friedman implica che molti teoremi matematici, come l'ultimo teorema di Fermat , possono essere dimostrati in sistemi molto deboli come l'EFA.

L'affermazione originale della congettura di Friedman (1999) è:

"Ogni teorema pubblicato negli Annals of Mathematics la cui affermazione coinvolge solo oggetti matematici finitari (cioè ciò che i logici chiamano un'affermazione aritmetica) può essere dimostrato in EFA. EFA è il frammento debole di Peano Arithmetic basato sui soliti assiomi senza quantificatori per 0 , 1, +, ×, exp, insieme allo schema di induzione per tutte le formule nel linguaggio i cui quantificatori sono tutti limitati."

Sebbene sia facile costruire affermazioni aritmetiche artificiali che siano vere ma non dimostrabili in EFA, il punto della congettura di Friedman è che gli esempi naturali di tali affermazioni in matematica sembrano essere rari. Alcuni esempi naturali includono affermazioni di consistenza dalla logica, diverse affermazioni relative alla teoria di Ramsey come il lemma della regolarità di Szemerédi e il teorema del minore dei grafi .

Sistemi correlati

Diverse classi di complessità computazionale correlate hanno proprietà simili a EFA:

  • Si può omettere il simbolo della funzione binaria exp dal linguaggio, prendendo l'aritmetica di Robinson insieme all'induzione per tutte le formule con quantificatori limitati e un assioma che afferma approssimativamente che l'elevamento a potenza è una funzione definita ovunque. Questo è simile a EFA e ha la stessa forza teorica della dimostrazione, ma è più complicato con cui lavorare.
  • Ci sono frammenti deboli di aritmetica del secondo ordine chiamati RCA*
    0     e WKL*
    0     che hanno la stessa forza di consistenza di EFA e sono prudenti su di esso per Π0
    2    frasi, che a volte sono studiate in matematica inversa ( Simpson 2009 ).
  • L'aritmetica ricorsiva elementare ( ERA ) è un sottosistema dell'aritmetica ricorsiva primitiva (PRA) in cui la ricorsione è limitata a somme e prodotti limitati . Anche questo ha lo stesso Π0
    2    frasi come EFA, nel senso che ogni volta che EFA dimostra ∀x∃y P ( x , y ), con P privo di quantificatori, ERA dimostra la formula aperta P ( x , T ( x )), con T un termine definibile in ERA . Come PRA, ERA può essere definito in modo del tutto privo di logica, con le sole regole di sostituzione e induzione, e definendo equazioni per tutte le funzioni ricorsive elementari. A differenza del PRA, tuttavia, le funzioni ricorsive elementari possono essere caratterizzate dalla chiusura per composizione e proiezione di un numero finito di funzioni base, e quindi è necessario solo un numero finito di equazioni definenti.

Guarda anche

Riferimenti

  • Avigad, Jeremy (2003), "Teoria dei numeri e aritmetica elementare", Philosophia Mathematica , Serie III, 11 (3): 257–284, doi : 10.1093/philmat/11.3.257 , ISSN  0031-8019 , MR  2006194
  • Friedman, Harvey (1999), grandi congetture
  • Simpson, Stephen G. (2009), Sottosistemi dell'aritmetica del secondo ordine , Perspectives in Logic (2a ed.), Cambridge University Press , ISBN 978-0-521-88439-6, MR  1723993