Timeline for Show that Z2 is not conservative over PA
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 26, 2014 at 1:13 | comment | added | A.C. | I've updated the question per this discussion. Furthermore, in response to: "So if your question is 'Why does Z2 prove Con(PA)?', then what you should want to see is an instance of Z2 proving induction along very long well-orderings." I would say, "Yes, this is exactly what I'm looking for, but I would still be interested if we can prove something simpler than Con(PA), as long as it can be translated into a first-order formula." | |
| Jan 26, 2014 at 1:03 | comment | added | A.C. | My apologies; the consistency of PA is a red herring. I'll settle for any first-order sentence that makes use of the special features of $\mathbf{Z}_2$. (I don't particularly care how much impredicativity gets used, either; it doesn't matter whether the formula is $\Pi_1^1$ or $\Pi_0^{200}$.) Also, per an update you just made: I was taught that "impredicativity" is the use of set quantifiers in the definition of a set. But what I'm looking for right now is an understanding of how second-order induction gives you access to proofs that first-order induction doesn't. | |
| Jan 26, 2014 at 0:58 | history | edited | Noah Schweber | CC BY-SA 3.0 |
added 1165 characters in body
|
| Jan 26, 2014 at 0:49 | comment | added | Noah Schweber | (Specifically, I'm confused by the linking of consistency proofs with impredicativity, which seems to me like it might be a red herring in this context.) | |
| Jan 26, 2014 at 0:43 | comment | added | Noah Schweber | This is not what I describe in the beginning of my answer. There, I'm talking about proving induction along $\omega$ - a relatively short well-ordering - for complex (=high quantifier-complexity) statements, which is not the same thing. I gave that example since I think it's an easier example of something $Z_2$ proves that $ACA_0/PA$ doesn't, but now I think it was misleading. I think I should edit my answer to address your actual question, but I'm not quite clear what that question is. What exactly are you looking for? | |
| Jan 26, 2014 at 0:40 | comment | added | Noah Schweber | (By the way, $\epsilon_0$ is the least fixed point of the map $\alpha\mapsto \omega^\alpha$, usually suggestively written as $\epsilon_0:= \omega^{\omega^{\omega^{.^{.^.}}}}$.) So the way that $Z_2$ proves $Con(PA)$ is by proving induction along very long well-orderings. So if your question is "Why does $Z_2$ prove $Con(PA)$?", then what you should want to see is an instance of $Z_2$ proving induction along very long well-orderings. (cont'd) | |
| Jan 26, 2014 at 0:33 | comment | added | Noah Schweber | I think there's still a confusion: "a la Gentzen" is just a reference to the fact that, for all natural theories (including $PA$), a very small finitary theory together with "enough" induction proves that theory's consistency. Now, what "enough" means here varies from theory to theory, and is known as the "proof-theoretic ordinal" of a theory. For example, the proof-theoretic ordinal of $PA$ is $\epsilon_0$, which means that "$\epsilon_0$ is well-founded" (together with a very weak - much weaker than $RCA_0$ - base theory) proves $Con(PA)$. (cont'd) | |
| Jan 25, 2014 at 23:01 | history | edited | François G. Dorais | CC BY-SA 3.0 |
fixed typos in formula
|
| Jan 25, 2014 at 22:50 | comment | added | A.C. | Great, OK. What I understand right now: We first use $\mathsf{Z}_2$ (or even $\mathsf{ATR}_0$) to define an impredicative set. Once we have it, we find an inductive proof that all numbers are in this set. Which means that every number has whatever property defined that set. This property can't be first-order since its formula still contains set quantifiers, but "à la" Gentzen, we can somehow eliminate those, yielding a theorem containing only first-order symbols but requiring second-order logic to prove. I promise not to leave before accepting an answer, but I need an evening to digest this. | |
| Jan 25, 2014 at 22:03 | comment | added | Noah Schweber | I just realized that in my answer when I say "a la Gentzen" I assume familiarity with Gentzen's work. Francois' answer has an explanation of what I mean by that. | |
| Jan 25, 2014 at 21:54 | history | answered | Noah Schweber | CC BY-SA 3.0 |