Truth values and proof theory (Q1037601): Difference between revisions

Canonical models constructed from the maximally consistent (with respect to derivability with cut) sequents provide completeness proofs for classical, intuitionistic and modal logic. The author reverses this process. In the classical case the conditions, say, for \(A\& B\in X\), \(A\&B\in Y\) in a maximally consistent sequent \(X\vdash Y\) determine standard Boolean semantics. In the intuitionistic case, two possible definitions of maximal consistency lead to two different semantics. If \(X\vdash Y\) is defined to be consistent when \(X\vdash A\) is underivable for every \(A\in Y\), then Beth semantics results. If \(X\vdash Y\) is consistent when \(X\vdash Y'\) is underivable for every \(Y'\subseteq Y\) in a multiple-succedent formulation, then Kripke semantics results. For S5, the authors considers a Kripke-style hypersequent (tableau) formulation where sequents correspond to possible worlds. It would be interesting to see whether the same result can be obtained from a cut-free sequent formulation by G. Shvarts.