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?



Weakest subsystems of second order arithmetic for mathematical logic
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](http://www.andrew.cmu.edu/user/avigad/Papers/elementary.pdf). NB. Avigad calls elementary arithmetic, EA.
2. Friedman, 2010, [Concrete Incompleteness from EFA through Large Cardinals](http://www.math.ohio-state.edu/~friedman/pdf/ConIncompAmst051010.pdf).


