Timeline for Show that Z2 is not conservative over PA
Current License: CC BY-SA 3.0
5 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Jan 26, 2014 at 3:41 | comment | added | Noah Schweber | What Francois described is how to talk about ordinals directly in the language of $PA$, which is what you really want. However, let me point out that talking about well-orderings in $Z_2$ is substantially easier; in particular, the statement "$R(x, y)$ is a well-ordering" no longer has to be expressed as an induction scheme, but is just a single $\Pi^1_1$ sentence. | |
Jan 26, 2014 at 3:00 | vote | accept | A.C. | ||
Jan 26, 2014 at 1:29 | comment | added | François G. Dorais | @A.C. Every ordinal below $\varepsilon_0$ has a unique hereditary base $\omega$ representation and the ordering of two such ordinals can be determined recursively from these finite representations (coded using numbers in the usual manner). Longer wellorderings such as $\Gamma_0$ have similar, but more complicated, computable systems of notations. | |
Jan 26, 2014 at 1:24 | comment | added | A.C. | Excellent! I think Goodstein's Theorem is a nicer example of what I'm looking for than Con(PA), primarily because it's simpler. From here I have to understand three things: How to encode the claim that $\epsilon_0$ is well-founded into the language of $\mathsf{Z}_2$, how to prove that claim, and then how to translate that claim into a first-order sentence (which will probably be Goodstein's theorem; I assume technical reasons make it impossible to encode the well-foundedness of $\epsilon_0$ directly in first-order terms). I may be able to do these without assistance; I'm still reading. | |
Jan 25, 2014 at 22:00 | history | answered | François G. Dorais | CC BY-SA 3.0 |