Higher-order illative combinatory logic

DOI10.2178/JSL.7803080zbMATH Open1341.03018arXiv1202.3672OpenAlexW2963381779MaRDI QIDQ2869904FDOQ2869904

Authors: Łukasz Czajka 

Publication date: 7 January 2014

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

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.

Full work available at URL: https://arxiv.org/abs/1202.3672

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

zbMATH Keywords

strong consistencyillative combinatory logic

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

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

Cited In (11)

• Title not available (Why is that?)
• Title not available (Why is that?)
• A semantic approach to illative combinatory logic
• Title not available (Why is that?)
• Some consistency proofs and a characterization of inconsistency proofs in illative combinatory logic
• On the role of implication in formal logic
• Bunder's paradox
• Title not available (Why is that?)
• Predicate calculus of arbitrarily high finite order
• Systems of combinatory logic related to predicative and ``mildly impredicative fragments of Quine's ``New Foundations
• An untyped higher order logic with Y combinator

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)