μ-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 ort the right side of sequents can characterize the distinction between classical systems and intuitionistic systems. From the existence of μ-heed 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>.
一般社団法人情報処理学会の論文
1997-06-15