Teorema di Löb

Nella logica matematica, il teorema di Löb stabilisce che nell'aritmetica di Peano (PA, o in qualsiasi sistema formale che la includa), per qualsiasi formula P, se è dimostrabile in PA che "se P è dimostrabile in PA allora P è vero", allora P è dimostrabile in PA. Se Prov( P) significa che la formula P è dimostrabile, possiamo esprimerla in modo più formale come segue:

Se

PA\,\vdash \,{{\rm {Prov}}(P)\rightarrow P}

,

allora

PA\,\vdash \,P

Un corollario immediato (la proposizione contrapposta) del teorema di Löb è che, se P non è dimostrabile in PA, allora la proposizione "se P è dimostrabile in PA, allora P è vero" non è dimostrabile in PA. Ad esempio, la proposizione "se $1+1=3$ " è dimostrabile in PA, allora $1+1=3$ è vero" non è dimostrabile in PA.^[1]

Il teorema di Löb è nominato in onore di Martin Löb che lo formulò nel 1955. Esso è correlato al paradosso di Curry.

Il teorema di Löb nella logica della dimostrabilità

La logica della dimostrabilità utilizza i teoremi di incompletezza di Gödel per esprimere la dimostrabilità di $\phi$ nel sistema dato all'interno della logicamodale in termini di $\Box \phi$ .

Il teorema può quindi essere formalizzato dall'assioma:

\Box (\Box P\rightarrow P)\rightarrow \Box P,

,

noto come assioma GL, abbreviazione di Gödel–Löb. Esso è talvolta formalizzato mediante una regola di inferenza secondo cui:

P

da

\Box P\rightarrow P.

La logica della dimostrabilità GL che risulta dall'assunzione del sistema modale K4 (o semplicemente K, dato che con $\Box A\rightarrow \Box \Box A$ l'assioma 4 diviene ridondante), con l'aggiunta dell'assioma GL sopra menzionato, nella logica della dimostrabilità è il sistema più utilizzato e oggetto di maggiore studio.

Dimostrazione modale del teorema di Löb

Il teorema di Löb può essere dimostrato all'interno della logica modale utilizzando solo alcune regole di base sull'operatore di dimostrabilità (il sistema K4), oltre all'esistenza di punti fissi modali.

Formule modali

Si assuma la seguente grammatica per le formule:

Se X è una variabile proposizionale, allora X è una formula
Se K è una costante proposizionale, allora K è una formula
Se A è una formula, allora $\Box A$ è una formula
Se $A$ e $B$ sono formule, allora sono formule anche $\neg A$ , $A\rightarrow B$ , $A\wedge B$ , $A\vee B$ e $A\leftrightarrow B$ .

Una proposizione modale è una formula modale che non contiene variabili proposizionali. Con $\vdash A$ si denota che $A$ è un teorema.

Punti fissi modali

Se $F(X)$ è una formula modal nella sola varibiele proposizionale $X$ , allora un punto fisso modale $F(X)$ è una proposizione $\Psi$ tale che

\vdash \Psi \leftrightarrow F(\Box \Psi )

Si assumerà l'esistenza di tali punti fissi modali per ogni formula con una variabile libera. non si tratta di un'ipotesi banale, ma se si interpreta $\Box$ come dimostrabilità in un'aritmetica di Peano, allora l'esistenza di punti fissi modali segue dal lemma della diagonalizzazone.

Regole di inferenza modali

Oltre all'esistenza di punti fissi modali, si assumono le seguenti regole di inferenza dell'operatore di dimostrabilità $\Box$ , note come condizioni di dimostrabilità di Hilbert–Bernays:

(necessitazione) Da $\vdash A$ si conclude che $\vdash \Box A$ : Informally, cioè se Aè un teorema, allora è dimostrabile..
(necesitazione interna) $\vdash \Box A\rightarrow \Box \Box A$ : se A dimostrabile, allora è dimostrabile che A è dimostrabile
(distributività) $\vdash \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)$ : questa regola permette di inferire col modus ponens all'interno dell'operatore di dimostrabilità. Se è dimostrabile che A implica B, ed A è dimostrabile, allora B è dimostrabile.

Dimostrazione del teorema di Löb

Si assuma che vi sia una proposizione modale $P$ tale che $\vdash \Box P\rightarrow P$ . Ciò significa che se $P$ è dimostrabile, allora $P$ è vera.
Dall'esistenza di punti fissi modali per ogni ofrmula (e in particolare per la formula $X\rightarrow P$ ) segue che esiste una proposizione $\Psi$ tale che $\vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)$ .
Dalla (2) segue che $\vdash \Psi \rightarrow (\Box \Psi \rightarrow P)$ .
Dalla regola di necessitazione segue che $\vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))$ .
Dalla (4) e dalla regola di distributività segue che $\vdash \Box \Psi \rightarrow \Box (\Box \Psi \rightarrow P)$ .
Applicando la regola di distributività a $A=\Box \Psi$ e a $B=P$ , si ottiene che $\vdash \Box (\Box \Psi \rightarrow P)\rightarrow (\Box \Box \Psi \rightarrow \Box P)$ .
Dalla (5) e dalla (6) segue che $\vdash \Box \Psi \rightarrow (\Box \Box \Psi \rightarrow \Box P)$ .
Dalla regola di necesitazione interna segue che $\vdash \Box \Psi \rightarrow \Box \Box \Psi$ .
Dalla (7) e dalla (8) segue che $\vdash \Box \Psi \rightarrow \Box P$ .
Dalla (1) e dalla (9) segue che $\vdash \Box \Psi \rightarrow P$ .
Dalla (2) segue che $\vdash (\Box \Psi \rightarrow P)\rightarrow \Psi$ .
Dalla (10) e dalla (11) segue che $\vdash \Psi$
Dalla (12) e dalla regola di necessitazione segue che $\vdash \Box \Psi$ .
Dalla (13) e dalla (10) segue che $\vdash P$ .

Esempi

Un corollario immediato del teorema di Löb è che, se P non è dimostrabile in PA, allora la proposizione "se P è dimostrabile in PA, allora P è vero" non è dimostrabile in PA. Sapendo noi che PA è coerente (mentre PA non è consapevole di questo), seguono alcuni semplici esempi:

La proposizione "Se $1+1=3$ è dimostrabile in PA, allora $1+1=3$ (è vero)", non è dimostrabile in PA, dal momento che $1+1=3$ non è dimostrabile in Pa (essendo falsa).
La proposizione "Se $1+1=2$ è dimostrabile in PA, allora $1+1=2$ (è vero)" è dimostrabile in PA, così come ogni proposizione del tipo "Se X, allora $1+1=2$ ".
La proposizione "Se il teorema finito forte di Ramsey è dimostrabile in PA, allora il teorema finito forte di Ramsey è vero" non è dimostrabile in PA, allora la proposizione "il teorema finito forte di Ramseyè vero" non è dimostrabile in PA (pur essendo vera).

Nella logica doxastica, il teorema di Löb mostra che ogni sistema classificato come ragionatore di tipo 4 deve anche essere "umile", nel senso che un tale ragionatore non può mai credere che "la mia fede in P implica che P sia vero", senza prima credere che P sia vero.^[2]

Il secondo teorema di incompletezza di Gödel deriva dal teorema di Löb mediante sostituzione della proposizione falsa $\bot$ per P.

Inverso: il teorema di Löb implica l'esistenza di punti modali fissi

Non soltanto l'esistenza di punti fissi modali implica il teorema di Löb, ma è vero anche il contrario. Quando il teorema di Löb è dato come un assioma, può essere derivata l'esistenza di punti fissi modali fin alla dimostrazione della formula $p\leftrightarrow A(p)$ per ogni formula A(p) modalizzata in p.^[3] Pertanto, nella logica modale normale, l'assioma di Löb è equivalente alla congiunzione dell'assioma 4 con l'esistenza di punti fissi modali.

Note

^ A meno che PA non sia coerente, caso in cui qualsiasi proposizione è dismotrabile in PA, incluso 1+1=3
^ Raymond Smullyan (1986) Logicians who reason about themselves, Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, Monterey (CA), Morgan Kaufmann Publishers Inc., San Francisco (CA), pp. 341-352
^ Per Lindström, Note on Some Fixed Point Constructions in Provability Logic, in Journal of Philosophical Logic, vol. 35, n. 3, giugno 2006, pp. 225–230, DOI:10.1007/s10992-005-9013-8.

Bibliografia

Boolos, George S., The Logic of Provability, Cambridge University Press, 1995, ISBN 978-0-521-48325-4.
Martin Löb, Solution of a Problem of Leon Henkin, in Journal of Symbolic Logic, vol. 20, n. 2, 1955, pp. 115–118, DOI:10.2307/2266895, JSTOR 2266895.
Hinman, P., Fundamentals of Mathematical Logic, A K Peters, 2005, ISBN 978-1-56881-262-5.
Rineke (L.C.) Verbrugge, Provability Logic, su Stanford Encyclopedia of Philosophy, 1º ° gennaio 2016.

Collegamenti esterni

(EN) Löb's theorem, su PlanetMath.
(EN) Eliezer Yudkowsky, The Cartoon Guide to Löb’s Theorem, su lesswrong.com.

Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica

[1] A meno che PA non sia coerente, caso in cui qualsiasi proposizione è dismotrabile in PA, incluso 1+1=3

[2] Raymond Smullyan (1986) Logicians who reason about themselves, Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, Monterey (CA), Morgan Kaufmann Publishers Inc., San Francisco (CA), pp. 341-352

[3] Per Lindström, Note on Some Fixed Point Constructions in Provability Logic, in Journal of Philosophical Logic, vol. 35, n. 3, giugno 2006, pp. 225–230, DOI:10.1007/s10992-005-9013-8.

[1]

[2]

[3]