La logica della dimostrabilità

0.Introduzione Nel 1963 Richard Montague pubblicava il suo famoso articolo dal titolo “Syntactical Treatment of Modality, with Corollaries on Reflexion Principles and Finite Axiomatizability” 1 , in cui dimostrava l’impossibilità di definire all’interno di teorie sufficientemente potenti, un predicato che traducesse l’operatore di necessità del sistema S4. Se la modalità doveva essere espressa secondo gli assiomi e le regole di S4, il suo trattamento non poteva essere sintattico. Non era possibile, a parere di Montague, definire un sistema in cui si potesse utilizzare un predicato per l’espressione della necessità invece di un operatore. Se dal punto di vista sintattico il trattamento di un operatore è piuttosto semplice, basta infatti introdurre gli assiomi appropriati e le regole di trasformazione, sul piano interpretativo, invece, si rende necessario sviluppare una semantica che sia in grado di fornire modelli adeguati ai sistemi modali con operatori. Se, infatti, la modalità non può essere espressa con un predicato, bisogna definire semantiche differenti da quelle adatte ai linguaggi predicativi. Uno dei possibili metodi è quello presentato da Saul Kripke 2 in un articolo apparso sullo stesso numero degli Acta Philosophica Fennica in cui si trova il contributo di Montague. La strategia è quella di formalizzare l’idea intuitiva di ‘mondo possibile’ ed interpretare la necessità come verità in tutti i mondi possibili rispetto a quello dato. Tuttavia il concetto di mondo possibile non è fra i più chiari. Il trattamento sintattico della modalità, viceversa, 1 Montague [1963].