Principal type-schemes and condensed detachment

DOI10.2307/2274956zbMath0708.03007OpenAlexW2040259072WikidataQ56138479 ScholiaQ56138479MaRDI QIDQ3489979

David Meredith, J. Roger Hindley

Publication date: 1990

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

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

zbMATH Keywords

condensed detachmentCurry-Howard isomorphismcombinatory logictype assignmentformulae as typesintuitionistic implicational logics

Mathematics Subject Classification ID

Classical propositional logic (03B05) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items

Note on Deduction Theorems in contraction-free logics, A simplified form of condensed detachment, A finitely axiomatized formalization of predicate calculus with equality, Principal type-schemes of BCI-lambda-terms, Condensed detachment is complete for relevance logic: A computer-aided proof, Implementing the `Fool's model' of combinatory logic, Most general first order theorems are not recursively enumerable, The converse principal type-scheme theorem in lambda calculus, Principal types of BCK-lambda-terms, Learning from Łukasiewicz and Meredith: investigations into proof structures, Double-negation elimination in some propositional logics

Cites Work

• Combinatory logic. Vol. II
• On Entailment
• The combinatory foundations of mathematical logic
• Unnamed Item
• Unnamed Item