# On sequents of $\Sigma$ formulas

## TL;DR

This paper explores the metamathematics of $
abla$ formulas within theories based on implications between such formulas, revealing their strength in proving correctness, intuitionistic validity, and set-theoretic completeness principles.

## Contribution

It introduces a novel class of theories with implications between $
abla$ formulas and demonstrates their significant metamathematical properties.

## Key findings

- Strong theories prove their own correctness.
- Extensions prove intuitionistic reasoning validity.
- Equivalence of two completeness principles in potentialist set theory.

## Abstract

We investigate the position that foundational theories should be modelled on ordinary computability. In this context, we investigate the metamathematics of $\Sigma$ formulas. We consider theories whose axioms are implications between $\Sigma$ formulas, and we show that arbitrarily strong such theories prove their own correctness. We also show that a natural extension of such a theory proves the validity of intuitionistic reasoning for that theory. Finally, we show the equivalence of two completeness principles appropriate to a potentialist conception of the universe of sets.