Higher-order illative combinatory logic

DOI10.2178/JSL.7803080MaRDI QIDQ2869904zbMATH OpenOpenAlexFDO

Authors Łukasz Czajka

Publication date 7 January 2014

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

Full work available at URL https://arxiv.org/abs/1202.3672, https://projecteuclid.org/euclid.jsl/1389032278

zbMATH Keywords

strong consistencyillative combinatory logic

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Abstract: We show a model construction for a system of higher-order illative combinatory logic $mathcal{I}_{o}mega$, thus establishing its strong consistency. We also use a variant of this construction to provide a complete embedding of first-order intuitionistic predicate logic with second-order propositional quantifiers into the system $mathcal{I}_0$ of Barendregt, Bunder and Dekkers, which gives a partial answer to a question posed by these authors.

Recommendations

• Systems of illative combinatory logic complete for first-order propositional and predicate calculus
• Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus
• Some consistency proofs and a characterization of inconsistency proofs in illative combinatory logic
• A semantic approach to illative combinatory logic
• scientific article; zbMATH DE number 4108723

Cites work

• Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus
• Equivalences between pure type systems and systems of illative combinatory logic
• Fuzzy Logic in Computer Science
• Systems of illative combinatory logic complete for first-order propositional and predicate calculus

Cited in

(11)

• An untyped higher order logic with Y combinator
• scientific article; zbMATH DE number 4108723 (Why is no real title available?)
• scientific article; zbMATH DE number 1028827 (Why is no real title available?)
• A semantic approach to illative combinatory logic
• scientific article; zbMATH DE number 4097340 (Why is no real title available?)
• Some consistency proofs and a characterization of inconsistency proofs in illative combinatory logic
• On the role of implication in formal logic
• Bunder's paradox
• scientific article; zbMATH DE number 4121963 (Why is no real title available?)
• Predicate calculus of arbitrarily high finite order
• Systems of combinatory logic related to predicative and ``mildly impredicative fragments of Quine's ``New Foundations

This page was built for publication: Higher-order illative combinatory logic

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