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

William M. Farmer

2017

Abstract

CTT_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.  CTT_uqe is a variant of CTT_qe that admits undefined
expressions, partial functions, and multiple base types of
individuals.  It is better suited than CTT_qe as a logic for building
networks of theories connected by theory morphisms.  This paper
presents the syntax and semantics of CTT_uqe, defines a notion of a
theory morphism from one CTT_uqe theory to another, and gives two
simple examples that illustrate the use of theory morphisms in
CTT_uqe.