Department of Mathematics

We investigate the position that foundational theories should be modelled on ordinary computability, with axioms and theorems presented as sequents of Σ formulas. We define a proof from such a theory to be a finite sequence of Σ formulas, with an axiom of the theory applied at each step. We obtain a complete system of logical axioms for this style of proof. In such a proof, free variables are not implicitly universally quantified, but rather behave like parameters, so each formula may be computationally verified, notionally in an infinitary setting, and literally in a finitary one. We show that such a foundational theory may establish the semantic properties of the Σ truth predicate, and may additionally establish that the truth of the assumption of any of its axioms implies the truth of the conclusion, but nevertheless that theory may be strong enough to formalize standard foundational theories in both the finitary and infinitary settings. We also show that the Σ truth predicate may be extended to intuitionistic sentences in a way that respects the connectives permitted in Σ formulas, by appealing to the constructive properties of intuitionstic deduction. Finally, we propose two completeness principles for the universe of pure sets, and show that they are equivalent.