Proof theory, higher order theories of reverse mathematics, and semi-intuitionism

点击翻译按钮获取中文摘要

The project resides in the EPSRC research area of logic and combinatorics. 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 naturalnumbers, and therefore is not expressive enough to be able to talk about higher order sets. In this project 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 new principles, which are impossible with classical logic, can be employed in proofs of mathematical theorems.The project requires the study of the proof-theoretic strength of higher-type systems, using techniques from ordinal analysis and functional interpretation. Another important part of the project will be the development of mathematics in semi-intuitionistic theories which has never been carried out in a systematic way.