The Variant Gentzen System for the Propositional Logic

The Gentzen system for the propositional logic is a deduction system which is logically equivalent to the corresponding axiomatic system. In the Gentzen system, the validity and provability of a sequence Γ ⇒ Δ are considered. The validity(⊨) corresponds to the provability(⊢). In this paper, we propose the variant Gentzen system which is a dual-system of the Gentzen system. A co-sequence Γ|Δ is introduced, and the variant Gentzen system is defined such that the satisfiability(⊨^co) of the co-sequence corresponds to the provability(⊢^co) of it. And another dual-Gentzen system is given such that the unsatisfiable of the co-sequence corresponds to the provability. The soundness and the completeness theorems of the both system are proved.