A complete system of deduction for Sigma formulas

Abstract

The Sigma formulas of the language of arithmetic express semidecidable relations on the natural numbers. More generally, whenever a totality of objects is regarded as incomplete, the Sigma formulas express relations that are witnessed in a completed portion of that totality when they hold. In this sense, the Sigma formulas are more concrete semantically than other first-order formulas. We describe a system of deduction that uses only Sigma formulas. Each axiom, an implication between two Sigma formulas, is implemented as a rewriting rule for subformulas. We exhibit a complete class of logical axioms for this system, and we observe that a distributive law distinguishes classical reasoning from intuitionistic reasoning in this setting. Skolem's theory PRA of primitive recursive arithmetic can be formulated in our deductive system. In Skolem's system, free variables are universally quantified implicitly, but in our formulation, free variables act as parameters to the deduction. In this sense, our formulation is more explicitly finitistic. Furthermore, most of our results are themselves finistic, being theorems of PRA. In particular, appending our main theorem to a celebrated chain of reductions from reverse mathematics, we find that an implication of Sigma formulas is derivable in WKL_0 if and only if there is a deduction from the antecedent to the consequent in our formulation of PRA.