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.

I. Introduction

The Gentzen system for the propositional logic is a deduction system which is logically equivalent to the corresponding axiomatic system ([1], [2]) and is also called sequent calculus. The Gentzen system and were introduced in 1934 by Gerhard Gentzen([1]) as a tool for studying natural deduction of first-order logic. And the main theorem(Hauptsatz) the cut-elimination theorem was applied to give a (transfinite) proof of the consistency of Peano arithmetic, in response to Godel's incompleteness theorems. Predicate calculus proofs are generally much easier to discover with sequent calculus, and are often shorter. Axiomatic system is more suited to practical theorem-proving. Gentzen system is more suited to theoretical analysis. The Gentzen system for other logics are proposed for the automatic reasoning, such as the Gentzen system for the modal logic ([2]), for the description logic ([3], [4]), and the dynamic logic ([3], [5]).