Higher-Order Illative Combinatory Logic

Publisher： Cambridge University Press

E-ISSN： 1943-5886|78|3|837-872

ISSN： 0022-4812

Source： The Journal of Symbolic Logic, Vol.78, Iss.3, 2013-09, pp. : 837-872

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

We show a model construction for a system of higher-order illative combinatory logic 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 of Barendregt, Bunder and Dekkers, which gives a partial answer to a question posed by these authors.

Related content

Systems of illative combinatory logic complete for first-order propositional and predicate calculus

By  

The Journal of Symbolic Logic, Vol. 58, Iss. 3, 1993-09 ,pp. : 769-788 (20)

Cambridge University Press

Access to resources Recommend Favorite

Consistency notions in illative combinatory logic

By  

The Journal of Symbolic Logic, Vol. 42, Iss. 4, 1977-12 ,pp. : 527-529 (3)

Cambridge University Press

Access to resources Recommend Favorite

Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic

By  

The Journal of Symbolic Logic, Vol. 63, Iss. 3, 1998-09 ,pp. : 869-890 (22)

Cambridge University Press

Access to resources Recommend Favorite

A weak absolute consistency proof for some systems of illative combinatory logic

By  

The Journal of Symbolic Logic, Vol. 48, Iss. 3, 1983-09 ,pp. : 771-776 (6)

Cambridge University Press

Access to resources Recommend Favorite

Some consistency proofs and a characterization of inconsistency proofs in illative combinatory logic

By  

The Journal of Symbolic Logic, Vol. 52, Iss. 1, 1987-03 ,pp. : 89-110 (22)

Cambridge University Press

Access to resources Recommend Favorite