Teorema de Löb

En llògica matemàtica, la teorema de Löb establix que en una teoria en aritmètica de Peano, per a qualsevol fòrmula P, es pot demostrar que "si P és demostradora llavors P", llavors P és demostradora. O siga:

si $T⊢\text{Dem}(\mathrm{\#}P)\to P$, llavors $T⊢P$

a on Dem(#P) significa que la fòrmula en número de Gödel #P és demostradora en T.

La teorema de Löb deu el seu nom a Martin Hugo Löb.

La teorema de Löb en la llògica demostrativa

La llògica demostrativa s'abstrau dels detalls de les fòrmules utilisades en els teoremes de incompletitud de Gödel expressant la demostrabilidad de P en el sistema donat en el llenguage de la llògica modal, per mig de la modalitat $◻P$.

Es pot formalisar la teorema de Löb per mig de l'axioma:

$◻(◻P\to P)\to ◻P$,

Este axioma es coneix com l'axioma GL, per Gödel-Löb. El mateix a voltes és formalisat per mig de la següent regla d'inferència:

$\frac{◻P\to P}{◻P}$

La llògica demostrativa GL que resulta de prendre la llògica modal K4 i agregar-li l'axioma GL és el sistema investigat en major intensitat en la llògica demostrativa.

Referències

Hinman, P. (2005). Fundamentals of Mathematical Logic, A K Peters.