  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.
