Truth values and proof theory (Q1037601): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
links / mardi / name | links / 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
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
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