Uniqueness of normal proofs in implicational intuitionistic logic

DOI10.1023/A:1008254111992MaRDI QIDQ1288178zbMATH OpenOpenAlexFDO

Authors Takahito Aoto

Publication date 20 June 1999

Published in Journal of Logic, Language and Information (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1008254111992

zbMATH Keywords

implicational intuitionistic logicKomori's problemminimal formulasminimal implicational theoremnatural deductionnon-prime contractionuniqueness of normal proofs

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05)

Review text

This paper includes the excellent result on the uniqueness of normal proofs in implicational intuitionistic logic. All previous results are covered with the result. A minimal theorem in a logic \(L\) is an \(L\)-theorem which is not a nontrivial substitution instance of another \(L\)-theorem. The reviewer [in: Proc. 10th Symp. on Semigroups, Sakado/Jap. 1986, 5-11 (1987)] raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system \(NJ\). Two sufficient conditions for a minimal implicational intuitionistic theorem \(A\) to have a unique \(\beta\)-normal proof in \(NJ\) have been obtained. One of them requires \(A\) to be provable in BCK; it follows from a series of results (Hirokawa, 1993; Jaskowski, 1963; Kashima, 1997). The other needs \(A\) to be of depth \(\leq 2\); it was proved by \textit{M. Tatsuta} [J. Symb. Log. 58, No. 3, 789-799 (1993; Zbl 0791.03004)]. The author gives a sufficient condition for a minimal implicational theorem in intuitionistic logic to have a unique normal proof in the natural deduction system \(NJ\). The result is that a minimal implicational intuitionistic theorem \(A\) has a unique \(\beta\)-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. The result covers the two conditions mentioned above.

Recommendations

• Uniqueness of normal proofs of minimal formulas
• scientific article; zbMATH DE number 700345
• Studying provability in implicational intuitionistic logic: the formula tree approach

Cited in

(9)

• Game semantics and uniqueness of type inhabitance in the simply-typed -calculus
• A Datalog recognizer for almost affine -CFGs
• Uniqueness of normal proofs of minimal formulas
• scientific article; zbMATH DE number 517044 (Why is no real title available?)
• scientific article; zbMATH DE number 700345 (Why is no real title available?)
• Studying provability in implicational intuitionistic logic: the formula tree approach
• The Yoneda reduction of polymorphic types
• Pregrammars and intersection types
• On the membership problem for non-linear abstract categorial grammars

This page was built for publication: Uniqueness of normal proofs in implicational intuitionistic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1288178)