A complete system of deduction for Sigma formulas

TL;DR

This paper introduces a deduction system using only Sigma formulas, providing a complete, finitistic framework that captures classical and intuitionistic reasoning, and connects to primitive recursive arithmetic and reverse mathematics.

Contribution

It develops a complete Sigma-formula-based deduction system that explicitly models finitistic reasoning and relates to PRA and reverse mathematics.

Findings

The system is complete for Sigma formulas.

It distinguishes classical from intuitionistic reasoning via a distributive law.

Implications of Sigma formulas are characterized within reverse mathematics.

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.