Timeline for Proof theory and subsystems of second-order arithmetic: in particular the reverse mathematics of Godel's system $T$
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 30, 2019 at 23:38 | comment | added | Thomas Benjamin | (cont.) for a strategy [as regards proving normalization for $F$] which goes outside $PA_2$", holds. | |
| Oct 30, 2019 at 23:32 | comment | added | Thomas Benjamin | (cont.) $F$ (Girard and Taylor, 1987, pp. 122-123)", It would seem you are corrrect in inferring that $PA_2$ is $Z_2$(since Girard also states on Pg. 113, that "...we seek to use 'all possible' axioms of comprehension..." ). But along with using all possible axioms of comprehension, one must therefore infer that one is using the full second-order induction scheme as well , so that $PA_2$ and $Z_2$ are equiconsistent (this from Carl Mummert's answer to David Roberts' mathoverflow question "$Z_2$ versus second-order $PA$ [question 97077]). But still and all, Girard's statement, "we must look | |
| Oct 30, 2019 at 23:17 | comment | added | Thomas Benjamin | While in the proposition in the middle of pg. 122 Girard states that, "The functions representable in $F$ are provably total in second-order Peano arithmetic $PA_2$", at the bottom of pg. 122 he also states, "...But $PA_2$ is precisely the system of arithmetic with induction, comprehension, and second order quantification, which is $Z_2$. Given also that the Wikipedia entry, "Second-order Arithmetic", under the subheading, "Definable functions", states that "The first-order functions that are provably total in second-order arithmetic are precisely the same as those representable in system | |
| Oct 28, 2019 at 22:20 | comment | added | Noah Schweber | Z$_2$ is cosmically stronger than PA. Z$_2$ is the union of the theories $\Pi^1_n$-CA$_0$ for $n\in\mathbb{N}$; even $\Pi^1_1$-CA$_0$ is galactically stronger than ATR$_0$, which is light-years more powerful than ACA$_0$ which is conservative over PA. While there's certainly an analogy between the two, Z$_2$ is a fundamentally different thing. (Meanwhile, your parenthetical is correct.) | |
| Oct 28, 2019 at 21:52 | comment | added | Thomas Benjamin | @NoahSchweber: How is $Z_2$ related to $PA$, just for the record (am I to infer that $Z_2$ is a bi-sorted first-order theory)? | |
| Oct 28, 2019 at 21:47 | comment | added | Noah Schweber | Note that what Girard means by "second-order arithmetic" is not the same as second-order Peano arithmetic - Girard's second-order arithmetic is a first-order theory. (In fact I think it's just Z$_2$.) | |
| Oct 28, 2019 at 21:46 | comment | added | Thomas Benjamin | (cont.) deduced from normalization within $PA_2$, the normalization theorem cannot be proved within $PA_2$. That gives us an essential piece of information for the proof: we must look for a strategy which goes outside $PA_2$." Since the corollary, "All terms of $F$ are strongly normalisable" seems to be proven in a finite number of steps, strong normalisability is proven by finite means yet by means not provable in$PA_2$. Would these means be 'ideal' in Hilbert's sense? | |
| Oct 28, 2019 at 21:33 | comment | added | Thomas Benjamin | It is interesting to note that in Girard's book PROOFS AND TYPES, Chapter 14 ("Strong normalization for $F$") one finds the following comment on pg. 113: "...Existence is much more delicate; in fact, we shall see in Chapter 15 that the normalization theorem for $F$ implies the consistency of second order arithmetic $PA_2$. The classic result of logic, if anything deserves that name, is Godel's second incompleteness theorem, which says (assuming that it is not contradictory) that the consistency of $PA_2$ cannot be proved within $PA_2$. Consequently, since consistency can be | |
| Oct 23, 2019 at 19:56 | comment | added | Noah Schweber | Incidentally, this cstheory.stackexchange answer looks relevant with regards to formulating the question more precisely - specifically, the difference between proving consistency and normalization. (There system F is talked about rather than system T, but at a glance I think the same issue holds.) | |
| Oct 23, 2019 at 19:48 | history | edited | Noah Schweber | CC BY-SA 4.0 |
added 11 characters in body
|
| Oct 23, 2019 at 19:48 | comment | added | Noah Schweber | Note that there's a crucial terminology distinction here (which I botched in a comment thread on the OP's prior question): primitive recursive function vs. primitive recursive functional. | |
| Oct 23, 2019 at 19:43 | history | edited | Thomas Benjamin | CC BY-SA 4.0 |
eliminated stuttering
|
| Oct 23, 2019 at 19:29 | history | asked | Thomas Benjamin | CC BY-SA 4.0 |