Theory of types

The theory of types was first described by Bertrand Russell in 1908. He was seeking a logical theory that could serve as a framework for mathematics, and, in particular, a theory that would avoid the so-called ‘vicious-circle’ antinomies, such as his own paradox of the property of those properties that are not properties of themselves – or, similarly, of the class of those classes that are not members of themselves. Such paradoxes can be thought of as resulting when logical distinctions are not made between different types of entities, and, in particular, between different types of properties and relations that might be predicated of entities, such as the distinction between concrete objects and their properties, and the properties of those properties, and so on. In ‘ramified’ type theory, the hierarchy of properties and relations is, as it were, two-dimensional, where properties and relations are distinguished first by their order, and then by their level within each order. In ‘simple’ type theory properties and relations are distinguished only by their orders.

GLIVENKO AND KURODA FOR SIMPLE TYPE THEORY

Glivenko’s theorem states that an arbitrary propositional formula is classically provable if and only if its double negation is intuitionistically provable. The result does not extend to full first-order predicate logic, but does extend to first-order predicate logic without the universal quantifier. A recent paper by Zdanowski shows that Glivenko’s theorem also holds for second-order propositional logic without the universal quantifier. We prove that Glivenko’s theorem extends to some versions of simple type theory without the universal quantifier. Moreover, we prove that Kuroda’s negative translation, which is known to embed classical first-order logic into intuitionistic first-order logic, extends to the same versions of simple type theory. We also prove that the Glivenko property fails for simple type theory once a weak form of functional extensionality is included.