A remark on Gentzen's calculus of sequents.
Johannes Czermak · Notre Dame Journal of Formal Logic · 1977
In this short note we call attention to a simple but perhaps interesting property of Gentzen's calculus of sequents (c/.[1]): the restriction to sequents whose antecedent contains at most one formula does not affect the derivability of classically valid formulas without existential quantifier and implication sign (in contrast to the corresponding restriction concerning the succedent; as is well-known, in this case we get the intuitionistic calculus; see [1], p. 192).Let us call the system obtained from Gentzen's calculus by this restriction the "dual-intuitionistic calculus DJ'\ In [2] we prove by embeddings of propositional logics in S4: Each classically valid N-K-A-formula is derivable in DJ.Now we give a direct proof of this theorem, extending it to formulas containing the universal quantifier.The axioms of DJ are all the sequents of the form a -> a.The rules of inference are: r-A,«,E,e Γ-A,«,« "' Γ-Δ,β,α,θ ι ' Γ-Δ,α a(a) -Δ Γ-A,α(α) ( ^' τixa(x)->A K{ * i} Γ-Δ.ΠwW