Weakest subsystems of second order arithmetic for mathematical logic - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-20T04:52:50Z http://mathoverflow.net/feeds/question/30904 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/30904/weakest-subsystems-of-second-order-arithmetic-for-mathematical-logic Weakest subsystems of second order arithmetic for mathematical logic Marc Alcobé García 2010-07-07T15:29:52Z 2010-07-08T12:16:39Z <p>It is known that to prove completeness of first-order logic for countable languages WKL<sub>0</sub> is enough. But, is it the weakest subsystem where one can prove it?</p> <p>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?</p> http://mathoverflow.net/questions/30904/weakest-subsystems-of-second-order-arithmetic-for-mathematical-logic/30905#30905 Answer by Carl Mummert for Weakest subsystems of second order arithmetic for mathematical logic Carl Mummert 2010-07-07T15:37:05Z 2010-07-07T15:37:05Z <p>This is all in Stephen Simpson's book <em>Subsystems of second order arithmetic</em>. </p> <p>The completeness theorem "every consistent countable first-order theory has a model" is equivalent to WKL<sub>0</sub> over RCA<sub>0</sub>, so no weaker system containing RCA<sub>0</sub> 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<sub>0</sub>. </p> <p>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<sub>0</sub>, for example. </p> http://mathoverflow.net/questions/30904/weakest-subsystems-of-second-order-arithmetic-for-mathematical-logic/31008#31008 Answer by Charles Stewart for Weakest subsystems of second order arithmetic for mathematical logic Charles Stewart 2010-07-08T09:12:10Z 2010-07-08T12:16:39Z <p>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.</p> <p>EFA can be usefully extended to the language of second-order arithmetic using the comprehension scheme ∀x (φ(x) ↔ ψ(x)) → <b>∃Y</b> ∀x (x ∈ <b>Y</b> ↔ φ(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.</p> <p>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.</p> <p><strong>References</strong> </p> <ol> <li>Avigad, 2003, <a href="http://www.andrew.cmu.edu/user/avigad/Papers/elementary.pdf" rel="nofollow">Number theory and elementary arithmetic</a>. NB. Avigad calls elementary arithmetic, EA.</li> <li>Friedman, 2010, <a href="http://www.math.ohio-state.edu/~friedman/pdf/ConIncompAmst051010.pdf" rel="nofollow">Concrete Incompleteness from EFA through Large Cardinals</a>.</li> </ol>