Heyting aritmetica - Heyting arithmetic
Nella logica matematica , Heyting arithmetic (a volte abbreviato HA ) è un'assiomatizzazione dell'aritmetica in accordo con la filosofia dell'intuizionismo . Prende il nome da Arend Heyting , che per primo lo propose.
introduzione
Heyting arithmetic adotta gli assiomi dell'aritmetica di Peano (PA), ma usa la logica intuizionistica come regole di inferenza. In particolare, la legge del centro escluso non vale in generale, sebbene l' assioma dell'induzione possa essere utilizzato per dimostrare molti casi specifici. Ad esempio, si può dimostrare che ∀ x , y ∈ N : x = y ∨ x ≠ y è un teorema (due numeri naturali qualsiasi sono uguali o non uguali tra loro). Infatti, poiché "=" è l'unico simbolo del predicato nell'aritmetica di Heyting, ne consegue che, per ogni formula senza quantificatore φ , ∀ x , y , z , ... ∈ N : φ ∨ ¬ φ è un teorema ( dove x , y , z ... sono le variabili libere in φ ).
Storia
Kurt Gödel ha studiato la relazione tra l'aritmetica di Heyting e l'aritmetica di Peano. Ha usato la traduzione negativa di Gödel-Gentzen per dimostrare nel 1933 che se HA è coerente, anche PA è coerente.
Concetti correlati
L'aritmetica di Heyting non deve essere confusa con le algebre di Heyting , che sono l'analogo intuizionistico delle algebre booleane .
Guarda anche
Riferimenti
- Ulrich Kohlenbach (2008), Teoria della dimostrazione applicata , Springer.
- Anne S. Troelstra , ed. (1973), Indagine metamatematica dell'aritmetica e dell'analisi intuizioniste , Springer, 1973.
link esterno
- Stanford Encyclopedia of Philosophy : " Intuitionistic Number Theory " di Joan Moschovakis .
- Frammenti di Heyting Arithmetic di Wolfgang Burr
 |
Questo articolo relativo alla logica matematica è uno stub . Puoi aiutare Wikipedia espandendolo . |