# Aritmetica tipografica

In matematica, l'aritmetica tipografica, o AT (in inglese Typographical Number Theory, o TNT) è un sistema formale assiomatico che descrive i numeri naturali che compare nel libro di Douglas Hofstadter Gödel, Escher, Bach. È una implementazione dell'aritmetica di Peano.
Come ogni sistema che implementa gli assiomi di Peano, l'aritmetica tipografica è in grado di riferirsi a sé stessa (è autoreferenziale).
Viene utilizzato un sistema ristretto, che tratta solo di numeri interi e positivi, allo scopo di trovare la minima configurazione in cui appare possibile esprimere il Teorema di Gödel.
Nella sua versione minima, l'AT utilizza 20 simboli, più un simbolo di fine riga. È definita anche l'associazione di ciascun simbolo con un numero di Gödel nella quale vengono usati numeri a tre cifre (chiamati triplette per analogia con il DNA) composti dalle cifre 1, 2, 3 e 6.
Alcuni dei simboli e delle regole derivano da un sistema formale precedentemente definito, chiamato calcolo proposizionale che implementa il calcolo proposizionale comunemente utilizzato in logica matematica.
Traducendo le formule in numeri, Hofstadter mostra come il teorema di Gödel corrisponda ad un numero, e come quel numero sia parte dell'AT.
Viene anche definita una versione dell'AT che elimina alcuni simboli, chiamata versione frugale dell'AT.

## Numerali

Nell'aritmetica tipografica non si ha un simbolo che esprime ciascun numero naturale. Ad ogni naturale si associa invece una stringa composta dai soli due simboli S e 0:
    zero 0 uno S0 due SS0 tre SSS0 quattro SSSS0 cinque SSSSS0
e così via.
Il simbolo S può essere interpretato come "il Successore di".

## Variabili

Si ha anche la necessità di riferirsi a numeri non specificati a priori, o variabili. Nell'AT esistono cinque variabili:
    a, b, c, d, e.
Altre variabili possono essere costruite aggiungendo un apice alla loro destra, così
    a', b', c', a'', a'''
sono tutte variabili.
Nella versione frugale dell'AT, esistono solo i simboli
    a', a'', a''', eccetera.

## Operatori
### Addizione e moltiplicazione di numerali

Nell'aritmetica tipografica si utilizzano gli usuali simboli "+" per l'addizione e "·" per la moltiplicazione. Dunque per scrivere "b più c" si scrive
    (b+c)
e "a per d" si scrive
    (a·d).
Si noti che le parentesi sono necessarie affinché le stringhe siano ben formate. Inoltre le operazioni sono binarie, e quindi si può eseguire un'operazione solo tra due termini. Per scrivere "a più b più c" si deve scrivere
    ((a+b)+c)
oppure
    (a+(b+c)).

### Uguaglianza

Per indicare l'uguaglianza si usa il simbolo "=", avente lo stesso significato che ha solitamente in matematica. Per esempio,
    SSS0+SSS0=SSSSSS0
è un teorema dell'AT (corrispondente ad un enunciato vero nell'aritmetica), che significa che "3 più 3 è uguale a 6".

### Negazione

Nell'AT, la negazione, cioè il trasformare un'affermazione nel suo contrario, è denotata dal simbolo "¬". Per esempio,
    ¬(SSS0+SSS0)=SSSSSSS0
è un teorema dell'AT.

### Congiunzione

Per indicare la congiunzione ("e") si usano i simboli
    <, all'inizio della stringa;
    ∧, per indicare la "e";
    >, alla fine della stringa.
Perciò la proposizione "0 più uno è uguale a uno e uno più uno è uguale a due" viene scritta come:
    <(0+S0)=S0∧(S0+S0)=SS0>.

### Disgiunzione

Per indicare la disgiunzione ("o") si usano i simboli
    <, all'inizio della stringa;
    ∨, per indicare la "o";
    >, alla fine della stringa.
Perciò la frase "0 più uno è uguale a uno o uno più uno è uguale a due" viene scritta come:
    <(0+S0)=S0∨(S0+S0)=SS0>.

### Implicazione

Per indicare l'implicazione logica ("se... allora..."), si usano i seguenti simboli:
    <, all'inizio della stringa;
    ⊃, per separare premessa e conclusione;
    >, alla fine della stringa.
Perciò la proposizione "se uno è uguale a zero, allora zero è uguale a uno" viene scritta in questo modo:
    <S0=0⊃0=S0>.

## Atomi e simboli proposizionali

Tutti i simboli del calcolo proposizionale vengono usati nell'aritmetica tipografica, ed essi mantengono il loro significato.
Per atomi si intendono stringhe che attestano uguaglianze, come per esempio
    ¬S0=SS0.
Sono invece formule composte le seguenti:
    (SS0+SSS0)=SSSS0; 2 più 3 uguale a 4,
    ¬(SS0+SS0)=SSS0; 2 più 2 non è uguale a 3,
    <S0=0⊃0=S0>; se 1 è uguale a 0, allora 0 è uguale a 1.

## Quantificatori

Vengono usati due quantificatori: ∀ e ∃.
* ∃ significa "esiste", viene detto quantificatore esistenziale
* ∀ significa "per ogni", viene detto quantificatore universale
* Il simbolo ":" viene usato per separare un quantificatore da un altro quantificatore o dal resto della formula.
Per esempio
    ∀a:∀b:(a+b)=(b+a)
"per ogni numero a e per ogni numero b, a più b è uguale a b più a", ovvero "l'addizione è commutativa".
    ¬∃c:Sc=0
"non esiste un numero c tale che c più uno è uguale a zero", ovvero "zero non è il successore di nessun numero naturale".
Una variabile che sta nel campo di azione di un quantificatore si chiama variabile quantificata, altrimenti viene detta variabile libera. Una formula che contiene almeno una variabile libera viene detta aperta, altrimenti viene detta chiusa oppure enunciato.

## Regole di formazione
### Numerali

    0 è un numerale.
    Un numerale preceduto da S è anch'esso un numerale.
    Esempi: 0, S0, SS0.

### Variabili

    a, b, c, d, e sono variabili.
    Una variabile seguita da un apice è anch'essa una variabile.
    Esempi: a, b', c'''.

### Termini

    Tutti i numerali e tutte le variabili sono termini.
    Un termine preceduto da S è anch'esso un termine.
    Se s e t sono termini, allora lo sono anche (s+t) e (s·t).
    Esempi: 0, b, SSa', (S0·(SS0+c)), S(Sa·(Sb·Sc)).
    I termini si suddividono in due categorie:
* termini definiti (che non contengono variabili), per esempio: 0, (S0+S0).
* termini indefiniti (che contengono variabili), per esempio: b, (((S0+S0)+S0)+e).

### Atomi

    Se s e t sono termini, allora s=t è un atomo.
    Esempi: S0=0, S(b+c)=((c·d)·e).

### Negazioni

    Una formula ben formata preceduta da un simbolo di negazione (¬) è ben formata.
    Esempi: ¬S0=0, ¬<0=0⊃S0=0>.

### Composti

    Se x e y sono formule ben formate, e nessuna delle variabili libere dell'una si trova quantificata nell'altra, allora le seguenti formule sono ben formate:
    <x∧y>, <x∨y>, <x⊃y>.
    Esempi: <0=0∧¬0=0>, <S0=0⊃∀c:¬∃b:(b+b)=c>.

### Quantificazioni

    Se u è una variabile e x è una formula ben formata nella quale u è libera, allora le seguenti stringhe sono formule ben formate:
    ∃u:x, ∀u:x.
    Esempi: ∀a:<a=a∨¬∃c:c=a>, ~∃c:Sc=d.

### Formule aperte

    Contengono almeno una variabile libera.
    Esempi: ¬c=c, <∀b:b=b∧¬c=c>.

### Formule chiuse (enunciati)

    Non contengono variabili libere.
    Esempi: S0=0, ¬∀d:d=0.

## Assiomi

* ∀a:¬Sa=0
* ∀a:(a+0)=a
* ∀a:∀b:(a+Sb)=S(a+b)
* ∀a:(a·0)=0
* ∀a:∀b:(a·Sb)=((a·b)+a)

## Regole
### Regola di particolarizzazione

    Sia u una variabile che compare all'interno della stringa x. Se la stringa ∀u:x è un teorema, allora anche x lo è, e lo sono anche tutte le stringhe che si ottengono da x sostituendo u, in ogni sua occorrenza, con un qualunque fissato termine. Il termine che sostituisce u non deve contenere una variabile che risulti quantificata in x.
    Esempio: dall'assioma 1, sostituendo 0 al posto di a, si ottiene ¬S0=0.

### Regola di generalizzazione

    Sia x un teorema in cui compare la variabile libera u. Allora ∀u:x è un teorema.

### Regola di scambio

    Se u è una variabile, allora le stringhe ∀u:¬ e ¬∃u: sono interscambiabili all'interno di qualunque teorema.
    Esempio: applicando questa regola all'assioma 1, si ottiene ¬∃a:Sa=0 (ovvero: zero non è il successore di alcun numero naturale).

### Regola di esistenza

    Se un termine (che può contenere variabili, a patto che siano libere) compare in una o più volte in un teorema, allora si può sostituire quel termine in una, in alcune o in tutte le sue occorrenze con una variabile che non compare già nel teorema, facendo precedere il tutto dal corrispondente quantificatore esistenziale.
    Esempio: applicando questa regola all'assioma 1, si ottiene ∃b:∀a:¬Sa=b.

### Regola di simmetria per l'uguaglianza

    Se r=s è un teorema, allora lo è r=s.

### Regola di transitività per l'uguaglianza

    Se r=s e s=t sono teoremi, allora lo è r=t.

### Regola di introduzione per il successore

    Se r=t è un teorema, allora Sr=St è un teorema.

### Regola di eliminazione per il successore

    Se Sr=St è un teorema, allora r=t è un teorema.
Nella regola seguente si usa questa notazione: una formula ben formata nella quale la variabile a è libera viene abbreviata con il simbolo X{a}. Invece con il simbolo X{Sa/a} si indica la stessa stringa X nella quale però ogni occorrenza di a è stata sostituita con Sa. Analogamente, con X{0/a} si indica la stringa iniziale nella quale ogni occorrenza di a è stata sostituita con 0.

### Regola di induzione

    Sia u una variabile e X{u} una formula ben formata nella quale u compare libera. Se ∀u:<X{u}⊃X{Su/u}> e X{0/u} sono entrambe teoremi, allora anche ∀u:X{u} è un teorema.