Timeline for Proof strength of Calculus of (Inductive) Constructions
Current License: CC BY-SA 3.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 13, 2017 at 12:58 | history | edited | CommunityBot |
replaced http://mathoverflow.net/ with https://mathoverflow.net/
|
|
| Dec 8, 2012 at 17:07 | answer | added | Gro-Tsen | timeline score: 4 | |
| Jul 10, 2011 at 23:15 | answer | added | Daniel Mehkeri | timeline score: 2 | |
| Jul 1, 2011 at 21:27 | answer | added | Andrej Bauer | timeline score: 11 | |
| Jul 1, 2011 at 11:06 | comment | added | Emil Jeřábek | @David: This is an old result of Gödel. See en.wikipedia.org/wiki/G%C3%B6del-Gentzen_translation for definition of the translation and some references (the verification that the translation works is routine). | |
| Jul 1, 2011 at 10:56 | answer | added | Neel Krishnaswami | timeline score: 20 | |
| Jul 1, 2011 at 10:39 | comment | added | David Roberts♦ | @Emil RE constructive Heyting arithmetic - thanks for that, do you know where I could find details? Fleshed out, that would make a dcent answer. | |
| Jul 1, 2011 at 10:38 | comment | added | David Roberts♦ | @Noam, @Emil - I'm not personally looking for a constructive proof of Con(PA), but interested in the general question of the comparability of logical strength along classical set-theoretical lines, and logical strength of internal logic of a category, and logical strength of bare-bones proof assistants. But I guess a constructive proof that also avoided $\epsilon_0$-induction would be a awesome achievement. | |
| Jul 1, 2011 at 10:20 | comment | added | Emil Jeřábek | If you need constructive justification for consistency of PA, I guess there are easier ways to do it. I’m not familiar with CIC, but it sounds like some sort of higher-order logic/type theory. Thus, it’s quite likely much stronger than the constructive Heyting arithmetic, which is well-known to be equiconsistent with PA. | |
| Jul 1, 2011 at 9:25 | comment | added | Noam Zeilberger | In response to your motivation, note there are already constructive proofs of Con(PA), such as Gentzen's cut-elimination theorem and Gödel's Dialectica interpretation. However, these can be criticized philosophically as circular, since they rely on principles (e.g., transfinite induction up to $\epsilon_0$ for primitive recursive statements) which are equivalent to Con(PA), albeit in a non-trivial way; indeed, these proofs establish one direction of that equivalence. You can read Tait's FOM posts for a good discussion of this (e.g., cs.nyu.edu/pipermail/fom/2011-June/015556.html). | |
| Jul 1, 2011 at 9:14 | comment | added | David Roberts♦ | @joro - Voevodsky's personal version of Coq is different to the trunk, for sure, but I don't know the depth at which his modification is made. That would be another facet to this line of reasoning. | |
| Jul 1, 2011 at 8:35 | comment | added | joro | @David Isn't CIC too broad? Voevodsky has a Coq fork reflecting his new theory, so I am inclined to believe Coq and Voevodsky's fork are quite different types of CIC. | |
| Jul 1, 2011 at 5:12 | history | edited | Zev Chonoles | CC BY-SA 3.0 |
fixed LaTeX (the pair of underscores were being interpreted as an italics command)
|
| Jul 1, 2011 at 5:08 | history | asked | David Roberts♦ | CC BY-SA 3.0 |