Theory Interpretation in Simple Type Theory

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 firstorder 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.

• Type: Conference
• Year: 1993
• Where: HOA
• Authors: William M. Farmer
• Keywords: HOA 1993, Partial Functions, Simple Type Theory, Theoretical Computer Science, Theory Interpretation