Timeline for Feferman's universes for proof assistants?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 28, 2023 at 17:09 | comment | added | Victor Makarov | @Tymothy Chow Maybe you should also mention the 2004 paper of Feferman <a href="math.stanford.edu/~feferman/papers/Ambiguity.pdf"> Typical Ambiguity: Trying to Have Your Cake and Eat it too</a>. There he describes $ZFC/U_{<\omega}$ which seems more advanced than 1969 $ZFC/s$. | |
| Dec 29, 2022 at 22:30 | comment | added | Timothy Chow | Feferman's original paper is Set-theoretical foundations of category theory but I haven't found a non-paywalled link. Mike Shulman's paper Set theory for category theory contains a readable summary; see pages 24-25 in particular. | |
| Dec 29, 2022 at 19:41 | comment | added | Sam Sanders | Perhaps a short reminder of what a "Feferman universe" is, would be in order? | |
| Dec 29, 2022 at 16:46 | comment | added | François G. Dorais | I monitor proof assistants on a regular basis. Enough people there are willing and able to answer theoretical questions, there's just too few people asking. Anyway, the Feferman trick already plays a role there but at the next level up, as I tried to explain here: mathoverflow.net/questions/380539/… | |
| Dec 29, 2022 at 16:37 | comment | added | Hanul Jeon | I am not an expert on type theory, but I know that universes in Martin-Löf Type Theory (MLTT) are given with finitely many (introduction and elimination) rules, and adding (a form of) extensionality with LEM to MLTT results in a theory whose strength is more or less similar to that of ZFC. That seems to mean Feferman's idea would not work under type-theoretic setups. | |
| Dec 29, 2022 at 13:51 | history | asked | Timothy Chow | CC BY-SA 4.0 |