–
Room P3.10, Mathematics Building
Amílcar Sernadas, Instituto Superior Técnico
Topos semantics of fibring revisited
After a brief overview of the topic, the concept of fibring 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 fibring 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.