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 L_(3)-valued propositional logic, a multisequent is a triple Δ∣Θ∣Γ, which i...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 L_(3)-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. There is a sound, complete and monotonic Gentzen deduction system G for sequents. Dually, there is a sound, complete and nonmonotonic Gentzen deduction system G′ for co-sequents Δ: Θ: Γ. By taking different quantifiers some or every, there are 8 kinds of definitions of validity of multisequent Δ∣Θ∣Γ and 8 kinds of definitions of validity of co-multisequent Δ: Θ: Γ, and correspondingly there are 8 sound and complete Gentzen deduction systems for sequents and 8 sound and complete Gentzen deduction systems for co-sequents. Correspondingly their monotonicity is discussed.展开更多
基金supported by the Open Fund of the State KeyLaboratory of Sofware Development Environment(SKLSDE-2010KF-06)Beijing University of Aeronautics and Astronautics,and by the National Basic Research Program of China(973 Program)(2005CB321901).
文摘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 L_(3)-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. There is a sound, complete and monotonic Gentzen deduction system G for sequents. Dually, there is a sound, complete and nonmonotonic Gentzen deduction system G′ for co-sequents Δ: Θ: Γ. By taking different quantifiers some or every, there are 8 kinds of definitions of validity of multisequent Δ∣Θ∣Γ and 8 kinds of definitions of validity of co-multisequent Δ: Θ: Γ, and correspondingly there are 8 sound and complete Gentzen deduction systems for sequents and 8 sound and complete Gentzen deduction systems for co-sequents. Correspondingly their monotonicity is discussed.
