Theory Morphisms in Church’s Type Theory with Quotation and Evaluation

Abstract$${\textsc {ctt}}_\mathrm{qe}$$ is a version of Church’s type theory with global quotation and evaluation operators that is engineered to reason about the interplay of syntax and semantics and to formalize syntax-based mathematical algorithms. $${\textsc {ctt}}_\mathrm{uqe}$$ is a variant of $${\textsc {ctt}}_\mathrm{qe}$$ that admits undefined expressions, partial functions, and multiple base types of individuals. It is better suited than $${\textsc {ctt}}_\mathrm{qe}$$ as a logic for building networks of theories connected by theory morphisms. This paper presents the syntax and semantics of $${\textsc {ctt}}_\mathrm{uqe}$$, defines a notion of a theory morphism from one $${\textsc {ctt}}_\mathrm{uqe}$$ theory to another, and gives two simple examples involving monoids that illustrate the use of theory morphisms in $${\textsc {ctt}}_\mathrm{uqe}$$.