μ- Head Form Proofs with at Most Two Formulas in the Succedent

We investigate a special form of cut-free proofs in classical propositional logic which we call μ-head form proofs.The number of formula occurrences on the right side of sequents can characterize the distinction between classical systems and intuitionistic systems.From the existence of μ-head form proofs for arbitrary classical propositional theorems it is derived that at most two occurrences on the right side of sequents are enough to prove them.Moreover the notion of μ-head form proofs reveals some interesting and intimate connections between classical logic and intuitionistic logic.As a corollary the μ-head form proofs can be embedded into intuitionistic proofs a fact well-known as Glivenko's Theorem.The notion of μ-head form proofs separates a proof into a classical part and an intuitionistic part characterized by the disjunction property.Further this notion can be naturally extended to proofs of a restricted LK which we call an L'K system.Although the L'K proof is also classical it contains an intuitionistic proof with a non-trivial form which satisfies the disjunction property.The L'K system has the cut-elimination property.We can find some analogy between two pairs of sequent calculi(LJ L'J) and (L'K LK).

We investigate a special form of cut-free proofs in classical propositional logic,which we call μ-head form proofs.The number of formula occurrences on the right side of sequents can characterize the distinction between classical systems and intuitionistic systems.From the existence of μ-head form proofs for arbitrary classical propositional theorems,it is derived that at most two occurrences on the right side of sequents are enough to prove them.Moreover,the notion of μ-head form proofs reveals some interesting and intimate connections between classical logic and intuitionistic logic.As a corollary,the μ-head form proofs can be embedded into intuitionistic proofs,a fact well-known as Glivenko's Theorem.The notion of μ-head form proofs separates a proof into a classical part and an intuitionistic part characterized by the disjunction property.Further,this notion can be naturally extended to proofs of a restricted LK,which we call an L'K system.Although the L'K proof is also classical,it contains an intuitionistic proof with a non-trivial form,which satisfies the disjunction property.The L'K system has the cut-elimination property.We can find some analogy between two pairs of sequent calculi(LJ,L'J) and (L'K,LK).