Timeline for Weakest subsystems of second order arithmetic for mathematical logic
Current License: CC BY-SA 2.5
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 9, 2010 at 7:27 | comment | added | Kaveh | @Sergei Tropanets: See the first chapter of Girard's book "Proof Theory and Logical Complexity". | |
| Oct 5, 2010 at 23:38 | comment | added | Grant Olney Passmore | Shankar's proof of Goedel's First Incompleteness Theorem which he formalised within the Boyer-Moore theorem prover, (Nq)thm, is essentially a proof in PRA. Once one eliminates some conveniences (having direct access to ordered pairs instead of coding them as natural numbers, etc.), one sees that the Boyer-Moore logic used in that work is essentially PRA+TI(epsilon-0). But, Shankar does not use TI(epsilon-0) in his proof. So, his proof is formalised essentially in PRA. See Shankar's CUP book "Metamathematics, Machines and Goedel's Proof" for the gory details. | |
| Jul 17, 2010 at 2:30 | comment | added | Carl Mummert | 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 | |
| Jul 16, 2010 at 23:56 | comment | added | Sergei Tropanets | Where one can find the accurate proof of Godel incompleteness theorems in PRA? | |
| Jul 8, 2010 at 12:20 | comment | added | Charles Stewart | 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. | |
| Jul 8, 2010 at 11:19 | comment | added | Carl Mummert | 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. | |
| Jul 8, 2010 at 9:13 | comment | added | Charles Stewart | 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. | |
| Jul 8, 2010 at 7:27 | vote | accept | Marc Alcobé García | ||
| Jul 9, 2010 at 10:29 | |||||
| Jul 7, 2010 at 15:37 | history | answered | Carl Mummert | CC BY-SA 2.5 |