Timeline for Logical Reations for an Impredicative System in a Predicative MetaTheory
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 9, 2022 at 22:05 | comment | added | Jason Hu | @ŁukaszLew i am not sure if it's my browser but the link is horribly unreadable. everything is in its veery raw latex form. | |
| Mar 23, 2021 at 18:27 | comment | added | Łukasz Lew | fplab.bitbucket.io/posts/2012-12-06-induction-recursion.html by Venanzio Capretta | |
| Jun 8, 2018 at 4:08 | comment | added | Łukasz Lew | @cody Unfortunately, the link does not work any more. Are you able to find this content again? Are you aware of new publications in the area of formalizing impredicativity? | |
| Oct 24, 2015 at 4:29 | vote | accept | Max New | ||
| Oct 22, 2015 at 14:49 | comment | added | cody | I should add though, that induction recursion is known to be weaker than impredicative quantification in certain cases, as is nicely explained here: fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html | |
| Oct 20, 2015 at 19:41 | comment | added | cody | @MaxNew: This is actually quite difficult to find a citation for. The closest I can find is The Strength of Some Martin-Löf Type Theories which definitely settles the question for a predicative theory with a single universe and some kind of induction. But Agda has the terrifying induction recursion which makes it vastly more powerful. | |
| Oct 20, 2015 at 18:09 | comment | added | Max New | Wow, really? You can't prove System F normalizes in Agda? Do you have a citation for that? | |
| Oct 20, 2015 at 16:02 | history | answered | cody | CC BY-SA 3.0 |