Timeline for Ordinal Exponentiation in Genzen's Sequent Calculus
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 26, 2013 at 17:12 | comment | added | Noah Schweber | Oh, I didn't know that (both the part about PA having cut-elimination for appropriate endsequent proofs, and the part about that being what people mean by "cut-elimination for PA"). Thanks! | |
| Aug 25, 2013 at 19:18 | comment | added | Henry Towsner | This is basically right. One caveat: PA has cut-elimination for proofs whose endsequent consists of $\Sigma_1$ formulas, and this is usually what people mean when they talk about cut-elimination for PA. (This is basically equivalent to the fact that the infinitary system has full cut-elimination.) | |
| Aug 3, 2013 at 17:16 | history | edited | Noah Schweber | CC BY-SA 3.0 |
added 28 characters in body
|
| Aug 2, 2013 at 19:33 | history | edited | Noah Schweber | CC BY-SA 3.0 |
deleted 61 characters in body
|
| Aug 2, 2013 at 7:18 | history | edited | Noah Schweber | CC BY-SA 3.0 |
added 2566 characters in body
|
| Aug 2, 2013 at 3:49 | history | answered | Noah Schweber | CC BY-SA 3.0 |