Fibring Logics with Topos Semantics

摘要

The concept of flbring is extended to higher-order logics with arbitrary modalities and binding operators. A general completeness theorem is established for such logics including HOL and with the meta-theorem of deduction. As a corollary, completeness is shown to be preserved when flbring such rich logics. This result is extended to weaker logics in the cases where fibring preserves conservativeness of HOL-enrichments. Soundness is shown to be preserved by fibring without any further assumptions.