Logica dimostrativa

La logica dimostrativa è una logica modale nella quale l'operatore di necessità è interpretato come "è dimostrabile che". Il punto è quello di catturare il predicato di prova di una teoria formale ragionevolmente ricca, quale è l'aritmetica di Peano.

Descrizione

Il sistema fondamentale è in genere chiamato GL (dalle iniziali di Gödel e Löb) o anche L o K4W (dove W sta per ben fondato). Esso può essere ottenuto associando la versione modale del teorema di Löb alla logica K (K4).

Indicativamente, gli assiomi di GL sono tutte tautologie di una logica proposizionale classica in aggiunta a tutte le formule di una delle seguenti forme:

• assioma di distribuzione: □(p → q) → (□p → □q);
• assioma di Löb: □(□p → p) → □p.

Le regole di inferenza sono:

• modus ponens: dato p e p → q, si conclude che q
• necessitazione: dato $\vdash$ e p, si conclude che $\vdash$ □p.

Storia

Il modello GL fu elaborato per la prima volta da Robert M. Solovay nel 1976. Da allora fino alla sua morte nel 1996, il principale ispiratore fu George Boolos.

Significativi contributi alla materia arrivarono da Sergei N. Artemov, Lev Beklemishev, Giorgi Japaridze, Dick de Jongh, Franco Montagna, Giovanni Sambin, Vladimir Shavrukov, Albert Visser.

Esempi

Esistono molteplici logiche dimostrative. Ad esempio la logica interpretativa e la logica polimodale di Japaridze presentano estensioni naturali della logica dimostrativa.

Bibliografia

• George Boolos, The Logic of Provability. Cambridge University Press, 1993.
• Giorgi Japaridze and Dick de Jongh, The logic of provability. In: Handbook of Proof Theory, S. Buss, (ed.) Elsevier, 1998, pp. 475–546.
• Sergei N. Artemov and Lev Beklemishev, Provability logic. In: Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, (eds.), vol. 13, 2nd ed., pp. 189–360. Springer, 2005.
• Per Lindström, Provability logic—a short introduction. Theoria 62 (1996), pp. 19–61.
• Craig Smoryński, Self-reference and modal logic. Springer, Berlino, 1985.
• Robert M. Solovay, Provability Interpretations of Modal Logic, Israel Journal of Mathematics, Vol. 25 (1976): 287–304.

Collegamenti esterni

• (EN) ineke Verbrugge, Provability logic, in Edward N. Zalta (a cura di), Stanford Encyclopedia of Philosophy, Center for the Study of Language and Information (CSLI), Università di Stanford.