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?