A Formulation of the Simple Theory of Types (for Isabelle)

TL;DR

This paper formulates simple type theory for the Isabelle theorem prover, incorporating explicit type inference, recursive types, and higher-order logic, aiming to support general mathematics and computational reasoning.

Contribution

It introduces a formal simple type theory tailored for Isabelle, including explicit inference rules, recursive types, and higher-order logic via reflection.

Findings

Logic is suitable for general mathematics and computational problems.

Isabelle proof procedures are described.

Recursive types and functions can be formally constructed.

Abstract

Simple type theory is formulated for use with the generic theorem prover Isabelle. This requires explicit type inference rules. There are function, product, and subset types, which may be empty. Descriptions (the eta-operator) introduce the Axiom of Choice. Higher-order logic is obtained through reflection between formulae and terms of type bool. Recursive types and functions can be formally constructed. Isabelle proof procedures are described. The logic appears suitable for general mathematics as well as computational problems.