Weakest subsystems of second order arithmetic for mathematical logic - MathOverflow

Weakest subsystems of second order arithmetic for mathematical logic

2010-07-07T15:29:52Z

It is known that to prove completeness of first-order logic for countable languages WKL₀ is enough. But, is it the weakest subsystem where one can prove it?

What about the incompleteness theorems? Is it known which are the weakest subsystems of second order arithmetic where one would be able to prove each of them?

Answer by Carl Mummert for Weakest subsystems of second order arithmetic for mathematical logic

2010-07-07T15:37:05Z

This is all in Stephen Simpson's book Subsystems of second order arithmetic.

The completeness theorem "every consistent countable first-order theory has a model" is equivalent to WKL₀ over RCA₀, so no weaker system containing RCA₀ can prove that theorem. However, the special case of the completeness theorem in which the theory is already closed under logical consequence is provable in RCA₀.

The incompleteness theorems are stated in the language of first-order arithmetic. They are provable in first-order primitive recursive arithmetic (PRA) and therefore they are provable in any subsystem of second order arithmetic whose first-order part includes PRA. This includes RCA₀, for example.

Answer by Charles Stewart for Weakest subsystems of second order arithmetic for mathematical logic

2010-07-08T09:12:10Z

In fact, the incompleteness and completeness theorems can be proven in subsystems of second-order arithmetic weaker than RCA-0: incompleteness can be proven in EFA (first-order elementary arithmetic), which proves exponentiation total, but cannot prove iterated exponentiation to be total. In fact, systems much weaker than EFA can prove incompleteness: Solovay has shown that any sane system of arithmetic (more or less, any first-order equational logic where there are reasonable definitions of zero and successor) strong enough to prove that multiplication is total can prove incompleteness. But EFA is interesting because "Exponential Function Arithmetic is the weakest system in use for which the coding of finite objects by nonnegative integers is worry free" (Friedman 2010): EFA is a reasonable first-order base upon which to build reverse mathematics.

EFA can be usefully extended to the language of second-order arithmetic using the comprehension scheme ∀x (φ(x) ↔ ψ(x)) → ∃Y ∀x (x ∈ Y ↔ φ(x)), where where φ and ψ are Σ-0-1 and Π-0-1 predicates which may have free second-order variables (this definition is from Avigad 2003). This language, call it ERCA-0, is then an analog of RCA-0-like that is a conservative extension of EFA. Avigad shows how this base system can be considered as a weaker base theory for reverse mathematics, with a series of weaker analogs to other fixtures of the reverse mathematics landscape: in particular, EWKL-0, that analog of WKL-0, can prove the completeness theorem.

To summarise: ERCA-0 is weaker than RCA-0 and can prove the incompleteness theorems; EWKL-0 is weaker than WKL-0 and can prove the completeness theorem. We can hope for weaker systems still, but Friedman's remark suggests that such systems will be more complex, and less suitable for reverse mathematics: there's a sense in which we might expect this to be around the best "weak" base system.

References

Avigad, 2003, Number theory and elementary arithmetic. NB. Avigad calls elementary arithmetic, EA.
Friedman, 2010, Concrete Incompleteness from EFA through Large Cardinals.