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

From MaRDI portal
Importer (talk | contribs)
Created a new Item
 
Added link to MaRDI item.
links / mardi / namelinks / mardi / name
 

Revision as of 22:36, 30 January 2024

scientific article
Language Label Description Also known as
English
Truth values and proof theory
scientific article

    Statements

    Truth values and proof theory (English)
    0 references
    0 references
    16 November 2009
    0 references
    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.
    0 references
    0 references
    sequent calculus
    0 references
    completeness
    0 references
    intuitionistic logic
    0 references
    modal logic
    0 references
    classical logic
    0 references
    maximal consistency
    0 references
    semantics
    0 references

    Identifiers