Comparison of constructive multi-typed theory with subsystems of second order arithmetic

TL;DR

This paper introduces a new constructive axiomatic theory BT, compares it with second-order arithmetic systems, and analyzes their proof-theoretical strengths, highlighting its consistency with classical logic and constructive principles.

Contribution

It presents BT, a novel constructive theory with predicative comprehension, and explores its interpretability and proof-theoretic strength relative to existing second-order systems.

Findings

BT is mutually interpretable with PATr and SA.

BT is consistent with classical logic and constructive principles.

Fragments of BT, PATr, and SA have varying proof-theoretic strengths.

Abstract

This paper describes an axiomatic theory BT for constructive mathematics. BT has a predicative comprehension axiom for a countable number of set types and usual combinatorial operations. BT has intuitionistic logic, is consistent with classical logic and has such constructive features as consistency with formal Church thesis, and existence and disjunction properties. BT is mutually interpretable with a so called theory of arithmetical truth PATr and with a second-order arithmetic SA that contains infinitely many sorts of sets of natural numbers. We compare BT with some standard second-order arithmetics and investigate the proof-theoretical strengths of fragments of BT, PATr and SA.