## 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 language | English |
---|---|

Pages (from-to) | 217-242 |

Number of pages | 26 |

Journal | Journal of Logic, Language and Information |

Volume | 8 |

Issue number | 2 |

DOIs | |

Publication status | Published - 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