Uniqueness of normal proofs of minimal formulas

DOI10.2307/2275097MaRDI QIDQ4276021zbMATH OpenOpenAlexFDO

Authors Makoto Tatsuta

Publication date 7 July 1994

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2307/2275097

zbMATH Keywords

BCKminimal formulaNJNKnormal formnormal proofprovable formulassubstitution relation

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) BCK-algebras, BCI-algebras (06F35)

Recommendations

• scientific article; zbMATH DE number 700345
• scientific article; zbMATH DE number 517044
• Uniqueness of normal proofs in implicational intuitionistic logic
• Proof-graphs for minimal implicational logic
• The number of proofs for a BCK-formula

Cites work

• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• Principal types of BCK-lambda-terms

Cited in

(7)

• Uniqueness of normal proofs in implicational intuitionistic logic
• How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning
• 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000. La Sorbonne, Paris, France, July 23-31, 2000
• scientific article; zbMATH DE number 408809 (Why is no real title available?)
• 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

This page was built for publication: Uniqueness of normal proofs of minimal formulas

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