Semantic consistency proofs for systems of illative combinatory logic

Systemy illatywnej logiki kombinatorycznej rozszerzająbeztypowy rachunek kombinatorów o dodatkowe stałe mające na celureprezentację pojęć logicznych. W pracy wprowadzamy pewne silnesystemy illatywnej logiki kombinatorycznej będące rozszerzeniemwcześniejszych systemów Barendregta, Bundera i Dekkersa. Tym samymkontynuujemy kierunek badań Curry'ego i Bundera nad illatywną logikąkombinatoryczną. Definiujemy semantykę dla systemów illatywnych ipoprzez konstrukcje modeli pokazujemy niesprzeczność naszychsystemów. Niektóre spośród systemów których niesprzeczność wykazaliśmysą znacznie silniejsze niż systemy Barendregta, Bundera i Dekkersa. Wszczególności, najsilniejszy z naszych systemów zawiera pełnąekstensjonalną klasyczną logikę wyższego rzędu rozszerzoną o zależnetypy funkcyjne, sumy zależne, podtypy i W-typy.

Illative systems of combinatory logic consist of combinatory logicextended with additional constants intended to represent logicalnotions. We introduce some strong systems of illative combinatorylogic, extending earlier systems of Barendregt, Bunder and Dekkers.This continues Curry's and Bunder's lines of research on illativecombinatory logic. We define semantics for illative systems and showour systems consistent by model constructions. We also investigateproperties of translations of traditional systems of logic into thecorresponding systems of illative combinatory logic. Some of thesystems shown consistent in the present work are much stronger thanthe systems shown consistent by Barendregt, Bunder and Dekkers. Inparticular, the strongest of our systems essentially incorporatesfull extensional classical higher-order logic extended withdependent function types, dependent sums, subtypes and W-types,which allows to interpret a great deal of mathematics in thissystem.