Abstract

Reverse mathematics is a research area concerned with the logical strength of mathematical theorems. Traditionally, a scale for measuring strength is furnished by certain standard systems couched in the language of second order arithmetic. Roughly, a mathematical theorem M has strength T (with T be a one of the theories on the standard scale) if T proves M whereas none of the weaker theories proves M.

The standard scale of theories, however, is based on the rather impoverished language of second order arithmetic whose ontology is restricted to natural numbers and sets of natural numbers, and therefore is not expressive enough to be able to talk about higher order sets.

The aim is to develop reverse mathematics using a scale of higher order theories. A novel aspect is also to use theories that use different logics for mathematical objects, namely classical logic for numbers but intuitionistic logic for higher type mathematical objects.

The switch to intuitionistic logic for higher type objects has the advantage that the logical strength of the theories can be tamed while at the same time allowing for the expressiveness of higher type languages. A further exciting aspect of intuitionistic logic is that it introduces a new dimension of axiomatic freedom in mathematics in that principles, which are impossible with classical logic, can be employed in proofs of mathematical theorems.