Timeline for Gentzen's result on PA
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 11, 2020 at 8:48 | comment | added | none | I found an online draft of this book (Proof theory, by Herman Ruge Jervell) to be a very accessible introduction to Gentzen's proof and the concepts leading up to it. The draft is no longer at its old location but | |
| Jan 6, 2020 at 3:58 | history | became hot network question | |||
| Jan 5, 2020 at 22:29 | comment | added | Timothy Chow | Noah Schweber has answered your question, but note that the existence of some $\varphi$ follows from Gentzen's consistency proof. Namely, if there were no such $\varphi$, then by mimicking Gentzen's consistency proof, we would be able to prove the consistency of PA within PA itself. | |
| Jan 5, 2020 at 21:16 | vote | accept | Gabriel Nivasch | ||
| Jan 5, 2020 at 20:22 | comment | added | Wojowu | To answer the first part of the question: yes, transfinite induction is stated as a schema, just like usual induction. When talking about theories weaker than PA we may want to restrict which formulas we include (e.g. only quantifier-free or bounded ones), but for PA and stronger it doesn't matter. | |
| Jan 5, 2020 at 20:20 | history | edited | Martin Sleziak |
added the (peano-arithmetic) tag (Feel free to remove it if - for some reason - it's not a good fit for the question.)
|
|
| Jan 5, 2020 at 20:05 | answer | added | Noah Schweber | timeline score: 11 | |
| Jan 5, 2020 at 19:47 | comment | added | Gabriel Nivasch | I saw question mathoverflow.net/questions/5065 , and it does not answer my question. Over there, the OP wanted to know how you encode ordinals <eps_0 as natural numbers. I understand how you do that | |
| Jan 5, 2020 at 19:46 | history | asked | Gabriel Nivasch | CC BY-SA 4.0 |