Theory Interpretation in Simple Type Theory
William M. Farmer
1994
Abstract
Theory interpretation is a logical technique for relating one
axiomatic theory to another with important applications in mathematics
and computer science as well as in logic itself. This paper presents
a method for theory interpretation in a version of simple type theory,
called LUTINS, which admits partial functions and subtypes. The
method is patterned on the standard approach to theory interpretation
in first-order logic. Although the method is based on a nonclassical
version of simple type theory, it is intended as a guide for theory
interpretation in classical simple type theories as well as in
predicate logics with partial functions.