A modal logic $\varepsilon$-calculus.
Melvin Fitting · Notre Dame Journal of Formal Logic · 1975
Introduction* First-order modal logics have been formulated in conventional axiom systems, Gentzen systems, natural deduction systems and tableau systems.In this paper we give a formulation based on the classical €-calculus of Hubert [4].We deal only with S4 but a similar treatment of other modal logics is straightforward.Our proof of the analog of Hubert's second e-theorem is non-constructive and uses Kripke's model theory [3].A straightforward attempt at producing an e-calculus S4 by adding S4 axioms and rules to a classical logic e -calculus does not work.A look at Kripke's model theory for S4 makes clear the reason for this failure.If X is a formula with one free variable, x, exX classically is intended to be the name of a constant making X(x) true, if any constant does (see [4] for a fuller classical discussion).However, in a Kripke S4 model [2,3,5] there are many possible worlds, and a constant making X(x) true in one such world need not make it true in another.Thus in an e-calculus S4, exX would have to be a 'world-dependent' term, that is, possibly naming different constants in different worlds.Such things cannot be dealt with properly with the usual first-order S4 machinery.In [6,7] Stalnaker and Thomason created an extension of ordinary first-order S4, by adding an abstraction operator, to handle similar 'world-dependent' terms (definite descriptions are things of this sort).We use this fundamental idea in an essential way in constructing our system.The syntactic purpose of the abstraction operator is to specify exactly the scope of a substitution for a free variable.Let us denote substitution of the term/ for free x in Xby X{x/f).If / is a 'world-dependent' term, [OX] (x/f) and O[X(x/f)] could be taken in a natural way to have different semantic meanings.Let Γ be a possible world of a Kripke model and suppose /'names' the object c in Γ.To say [OX] (x/f) is true in Γ seems to say [Όx] (x/c) or <>X(x/c) is true in Γ.That is, for some world Δ possible relative to Γ, X{x/c) is true in Δ.