Semantic consistency proofs for systems of illative combinatory logic
Łukasz Czajka · 2015
Illative systems of combinatory logic consist of combinatory logic extended with additional constants intended to represent logical notions. We introduce some strong systems of illative combinatory logic, extending earlier systems of Barendregt, Bunder and Dekkers. This continues Curry’s and Bunder’s lines of research on illative combinatory logic. We define semantics for illative systems and show our systems consistent by model constructions. We also investigate properties of translations of traditional systems of logic into the corresponding systems of illative combinatory logic. Some of the systems shown consistent in the present work are much stronger than the systems shown consistent by Barendregt, Bunder and Dekkers. In particular, the strongest of our systems essentially incorporates full extensional classical higher-order logic extended with dependent function types, dependent sums, subtypes and W-types, which allows to interpret a great deal of mathematics in this system.