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

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

allora

${\displaystyle 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 ${\displaystyle 1+1=3}$" è dimostrabile in PA, allora ${\displaystyle 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.

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

Il teorema può quindi essere formalizzato dall'assioma:

${\displaystyle \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:

${\displaystyle P}$

da

${\displaystyle \Box P\rightarrow P.}$

La logica della dimostrabilità GL che risulta dall'assunzione del sistema modale K4 (o semplicemente K, dato che con ${\displaystyle \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.

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.

Si assuma la seguente grammatica per le formule:

1. Se X è una variabile proposizionale, allora X è una formula
2. Se K è una costante proposizionale, allora K è una formula
3. Se A è una formula, allora ${\displaystyle \Box A}$ è una formula
4. Se ${\displaystyle A}$ e ${\displaystyle B}$ sono formule, allora sono formule anche ${\displaystyle \neg A}$, ${\displaystyle A\rightarrow B}$, ${\displaystyle A\wedge B}$, ${\displaystyle A\vee B}$ e ${\displaystyle A\leftrightarrow B}$.

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

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

${\displaystyle \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 ${\displaystyle \Box }$ come dimostrabilità in un'aritmetica di Peano, allora l'esistenza di punti fissi modali segue dal lemma della diagonalizzazone.

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

1. (necessitazione) Da ${\displaystyle \vdash A}$ si conclude che ${\displaystyle \vdash \Box A}$: Informally, cioè se Aè un teorema, allora è dimostrabile..
2. (necesitazione interna) ${\displaystyle \vdash \Box A\rightarrow \Box \Box A}$: se A dimostrabile, allora è dimostrabile che A è dimostrabile
3. (distributività) ${\displaystyle \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.

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

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:

1. La proposizione "Se ${\displaystyle 1+1=3}$ è dimostrabile in PA, allora ${\displaystyle 1+1=3}$ (è vero)", non è dimostrabile in PA, dal momento che ${\displaystyle 1+1=3}$ non è dimostrabile in Pa (essendo falsa).
2. La proposizione "Se ${\displaystyle 1+1=2}$ è dimostrabile in PA, allora ${\displaystyle 1+1=2}$ (è vero)" è dimostrabile in PA, così come ogni proposizione del tipo "Se X, allora ${\displaystyle 1+1=2}$".
3. 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 ${\displaystyle \bot }$ per P.

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 ${\displaystyle 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.

• 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.

• (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 Teknopedia che trattano di matematica