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

TL;DR

This paper introduces ${\rm CTT}_{\rm uqe}$, an extension of Church's type theory with quotation and evaluation, enabling reasoning about syntax, semantics, and theory morphisms, including undefined expressions and multiple base types.

Contribution

It formalizes syntax and semantics for ${\rm CTT}_{\rm uqe}$ and defines theory morphisms within this framework, expanding the applicability of Church's type theory.

Findings

Defined syntax and semantics of ${\rm CTT}_{\rm uqe}$

Introduced theory morphisms for ${\rm CTT}_{\rm uqe}$

Provided illustrative examples of theory morphisms

Abstract

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