Uniqueness of Normal Proofs in Implicational Intuitionistic Logic

摘要: A minimal theorem in a logic L is an L-theorem which not non-trivial substitution instance of another L-theorem. Komori (1987) raised the question whether every implicational intuitionistic has unique normal proof natural deduction system NJ. The answer been known to be partially positive and generally negative. It shown here that β-normal NJ whenever provable without non-prime contraction. contraction rule implication introduction whose cancelled assumption differs from propositional variable appears more than once proof. Our result improves partial solutions Komori‘s problem. Also, we present simple example does have βη-normal