Monotonic and nonmonotonic gentzen deduction systems for L3-valued propositional logic

摘要

A sequent is a pair (Γ, Δ), which is true under an assignment if either some formula in Γ is false, or some formula in Δ is true. In L3-valued propositional logic, a multisequent is a triple Δ|Θ|Γ, which is true under an assignment if either some formula in Δ has truth-value t, or some formula in Θ has truth-value m, or some formula in Γ has truth-value f. Correspondingly there is a sound and complete Gentzen deduction system G for multisequents which is monotonic. Dually, a co-multisequent is a triple Δ: Θ: Γ, which is valid if there is an assignment v in which each formula in Δ has truth-value ≠ t, each formula in Θ has truth-value ≠ m, and each formula in Γ has truth-value ≠ f. Correspondingly there is a sound and complete Gentzen deduction system G− for co-multisequents which is nonmonotonic.