8
$\begingroup$

It is known that to prove completeness of first-order logic for countable languages WKL0 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?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
7
$\begingroup$

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

  1. Avigad, 2003, Number theory and elementary arithmetic. NB. Avigad calls elementary arithmetic, EA.
  2. Friedman, 2010, Concrete Incompleteness from EFA through Large Cardinals.
Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ For those who aren't familiar with these systems, RCA0 is exactly ERCA0 plus induction for Sigma^0_1 formulas, and WKL0 is exactly EWKL0 plus induction for Sigma^0_1 formulas. $\endgroup$
    – Carl Mummert
    Commented Jul 8, 2010 at 11:33
6
$\begingroup$

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 WKL0 over RCA0, so no weaker system containing RCA0 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 RCA0.

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 RCA0, for example.

Improve this answer
$\endgroup$
7
  • $\begingroup$ But Simpson's book does not discuss the literature on base theories weaker than RCA-0, so this answer does not really address the question. $\endgroup$
    – Charles Stewart
    Commented Jul 8, 2010 at 9:13
  • $\begingroup$ For second-order theorems, the way that I generally interpret the phrase "weakest subsystem that can prove X" is "weakest extension of RCA0 that can prove X". If we don't fix a base system, the weakest system that can prove X is the system that has only one axiom, namely X itself. But this is unlikely to be equivalent to any well-known system. The key property of a base system is that it is "weak enough". and RCA0 is generally considered to be weak enough for studying of the strength of second-order principles. The choice of the base system is always somewhat arbitrary, however. $\endgroup$
    – Carl Mummert
    Commented Jul 8, 2010 at 11:19
  • $\begingroup$ Right, but there's a constraint on base systems, namely that you need to be able to do reverse mathematics over them. The quote of Friedman I cited in my answer gives a case for saying ERCA-0 might be the weakest reasonable base system: not a strong case, but a "best we can do now" sort of case. I fixed my answer to make this a little clearer. $\endgroup$
    – Charles Stewart
    Commented Jul 8, 2010 at 12:20
  • $\begingroup$ Where one can find the accurate proof of Godel incompleteness theorems in PRA? $\endgroup$
    – Sergei Tropanets
    Commented Jul 16, 2010 at 23:56
  • 2
    $\begingroup$ Smorynski discusses this in his article in the Handbook of Mathematical Logic. However, since the incompleteness theorem for any particular effective theory can be expressed as a Pi^0_2 statement, it is enough to show it is provable in WKL_0 to know it is provable in PRA. This method is discussed in detail by Kikuchi and Tanaki in this paper: projecteuclid.org/euclid.ndjfl/1040511346 $\endgroup$
    – Carl Mummert
    Commented Jul 17, 2010 at 2:30

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .