Sul primo teorema di Gödel

Domande di teoria, mini-dispense degli utenti, richieste di riferimenti ad articoli, ...

Moderatore: Moderatori

Sul primo teorema di Gödel

Messaggioda hydro il ven 16 nov 2012, 16:34

Premetto che non so davvero nulla di logica quindi cerco, se esiste, una risposta molto poco tecnica.
Il fatto e' che capita piuttosto spesso di leggere la seguente parafrasi di uno dei teoremi di incompletezza di Gödel (ad esempio citando wikipedia):

Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory.

Ora, da profano io mi chiedo quale sia il significato della parola "true" in questo contesto (in effetti c'e' una nota a pie' di pagina ma non e' per nulla esplicativa). Io pensavo, probabilmente in modo erroneo, che all'interno di un certo "sistema formale" un enunciato si definisse "vero" se ne esiste una dimostrazione all'interno del sistema. E' chiaro che qui il significato della parola "vero" non puo' essere questo, altrimenti l'enunciato del teorema sarebbe contraddittorio. C'e' qualche buon'anima in giro che mi possa spiegare qual e' il senso di questa parafrasi del teorema in termini non tecnici? Oppure non e' possibile? Qual e' la vera definizione del concetto di "enunciato vero"?
hydro
 
Messaggi: 435
Iscritto il: mer 1 apr 2009, 9:40

Messaggioda shinigami87 il ven 16 nov 2012, 19:07

shinigami87
 
Messaggi: 285
Iscritto il: mer 6 gen 2010, 22:06
Località: Caserta

Messaggioda maurer il ven 16 nov 2012, 20:08

Dunque, qui trovi un'esposizione elementare ma incompiuta della teoria dei modelli di base. Manca effettivamente la parte che serve a te, perché non l'ho mai completata. Metto uno sketch dei dettagli della parte che ti interessa da vicino, ma lo nascondo.

L'idea è questa: a partire da un linguaggio \mathcal L, hai un modo di definire dei termini (vedi link) e delle formule (le cosiddette formule ben formate). Nello stesso modo in cui definisci l'interpretazione dei termini (fatto nel link) puoi definire l'interpretazione delle formule . Per il momento mi limito alle formule chiuse (se poi vuoi possiamo approfondire). Per definizione, se \varphi è una formula chiusa e M è un modello di \mathcal L, l'interpretazione di \varphi è un elemento \varphi^M \in \{\emptyset,\{\emptyset\}\}. La definizione di questo elemento si fa per induzione sulla complessità della formula:
  1. se t,s sono termini (necessariamente chiusi), allora
    (t = s)^M = \begin{cases}
\{\emptyset\} & \text{se } t^M = s^M \\
\emptyset & \text{altrimenti}
\end{cases}
  2. se \sigma è un simbolo di relazione n-aria e t_1,\ldots,t_n sono termini (chiusi) allora
    (r(t_1,\ldots,t_n))^M = \begin{cases}
\{\emptyset\} & \text{se } <t_1^M,\ldots,t_n^M> \in r^M \\
\emptyset & \text{altrimenti}
\end{cases}
  3. \bot^M = \emptyset;
  4. (\lnot \xi)^M = \{\emptyset\} \setminus \xi^M;
  5. (\xi \vel \psi)^M = \xi^M \cup \psi^M;
  6. (\exists u \: \varphi)^M = \bigcup_{a \in M} (\varphi[u/a])^M
(ci sono problemi di buona definizione, per cui bisognerebbe dimostrare risultati sintattici preliminari, ma per adesso sorvolo).

Ora, una teoria su un linguaggio \mathcal L è un insieme di formule ben formate e chiuse (tutte le variabili sono quantificate). Per definizione, quindi, in un modello ogni formula chiusa del linguaggio è vera o falsa (cioè, la sua interpretazione è \emptyset o \{\emptyset\}). Ora, un modello di una teoria \mathbb T è un modello del linguaggio in cui tutti gli asserti della teoria sono veri. Una teoria si dice consistente se ammette almeno un modello. Si dirà poi che una teoria dimostra un asserto \varphi se per ogni modello della teoria l'interpretazione di \varphi è vera.

Venendo alla tua domanda: quello che ti trae in inganno è che usa "true" in due modi diversi: vero in una teoria e vero in un modello. Credo, se non mi sbaglio, che l'inghippo sia questo: esiste un enunciato vero per il modello (solito) \mathbb N degli assiomi di Peano che non è provabile nella teoria costituita dagli assiomi di Peano, ossia esiste un altro modello degli assiomi in cui l'enunciato è falso (pur rimanendo un enunciato aritmetico vero, nel senso che la sua interpretazione in \mathbb N è vera). Trovi qualcosa di interessante in questo post di Baez.

This statement has no proof in Peano arithmetic that contains fewer than 10^{1000} symbols.


Visto che ci sono persone su questo forum che conoscono molta più logica di me, li pregherei di correggermi se ho commesso imprecisioni (o, peggio, se ho detto qualcosa di gravemente sbagliato). Mi sono attenuto ai ricordi di 2 anni fa.
Je n'ai jamais compris qu'on se rassasiât d'un être...
maurer
 
Messaggi: 1040
Iscritto il: mar 28 lug 2009, 12:14
Località: A metà strada per il Paradiso...!

Messaggioda maurer il ven 16 nov 2012, 21:32


Senza offesa, lo trovo piuttosto confusionario. Molto meglio la pagina inglese.

wiki.en ha scritto:A logical truth (also called an analytic truth or a necessary truth) is a statement which is true in all possible worlds[42] or under all possible interpretations, as contrasted to a fact (also called a synthetic claim or a contingency) which is only true in this world as it has historically unfolded. A proposition such as "If p and q, then p." is considered to be logical truth because it is true because of the meaning of the symbols and words in it and not because of any facts of any particular world. They are such that they could not be untrue.

Se non altro si intravede il significato formale che ho provato a spiegare prima.
Je n'ai jamais compris qu'on se rassasiât d'un être...
maurer
 
Messaggi: 1040
Iscritto il: mar 28 lug 2009, 12:14
Località: A metà strada per il Paradiso...!

Messaggioda Feanor il ven 16 nov 2012, 22:05

È come dice Mauro. Credo che ora si esprima in termini molto puri e tecnici, ma ciò che fece Goedel fu

to provide a counterexample to completeness by exhibiting an arithmetic statement which is neither provable nor refutable in Peano arithmetic, though true in the standard model. (cit.)

La potenza di questo fatto diviene molto più chiara se ci si ricorda del soundness (soprattutto qui).

P.S.: Ah! È notevole ricordare che questi teoremi furono da stimolo per l'ultimo atto eroico della scuola di Hilbert: l'invenzione del calcolo sequenziale (di Gentzen) e la dimostrazione della completezza dell'aritmetica tramite l'induzione trasfinita.
Feanor
 
Messaggi: 738
Iscritto il: lun 29 set 2008, 20:58

Messaggioda maurer il ven 16 nov 2012, 23:19

Feanor ha scritto:P.S.: Ah! È notevole ricordare che questi teoremi furono da stimolo per l'ultimo atto eroico della scuola di Hilbert: l'invenzione del calcolo sequenziale (di Gentzen) e la dimostrazione della completezza dell'aritmetica tramite l'induzione trasfinita.

Quindi se ammettiamo dimostrazioni che non terminano in tempo finito l'aritmetica è completa? Figo! Purtroppo non conosco il calcolo sequenziale di Gentzen...

P.S. Ho aggiunto un pezzo alla dispensa sulla logica formale. In realtà l'ho scritto più di un anno fa, ma non ho mai più finito di completarlo.
Je n'ai jamais compris qu'on se rassasiât d'un être...
maurer
 
Messaggi: 1040
Iscritto il: mar 28 lug 2009, 12:14
Località: A metà strada per il Paradiso...!


Torna a Teoria

Chi c’è in linea

Visitano il forum: Nessuno e 1 ospite