Uniqueness of normal proofs in implicational intuitionistic logic

Takahito Aoto

Research output: Contribution to journalArticlepeer-review

9 Citations (Scopus)

Abstract

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

Original languageEnglish
Pages (from-to)217-242
Number of pages26
JournalJournal of Logic, Language and Information
Volume8
Issue number2
DOIs
Publication statusPublished - 1999 Jan 1

Keywords

  • Coherence
  • Komori's problem
  • Minimal formulas
  • Natural deduction
  • Non-prime contraction
  • Uniqueness of normal proofs

ASJC Scopus subject areas

  • Computer Science (miscellaneous)
  • Philosophy
  • Linguistics and Language

Fingerprint Dive into the research topics of 'Uniqueness of normal proofs in implicational intuitionistic logic'. Together they form a unique fingerprint.

Cite this