Timeline for Which kind of foundation are mathematicians using when proving metatheorems?
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 1, 2017 at 2:21 | comment | added | Thomas Benjamin | How are material set theory and structural set theory related from the point of view of category theory? Would the answer to this question help answer the OP's question? | |
| Jan 31, 2017 at 19:35 | vote | accept | CommunityBot | ||
| Jan 31, 2017 at 17:54 | answer | added | Mike Shulman | timeline score: 19 | |
| Jan 31, 2017 at 16:19 | comment | added | Todd Trimble | A very weak form of structural set theory would be enough, if my reading is correct. A similarly weak form of material set theory would be enough too (but maybe overkill IMO). | |
| Jan 31, 2017 at 16:06 | comment | added | user103598 | @ToddTrimble: Thanks. "so it looks like some set theory is being invoked there" Is this set theory a material or a structural set theory? | |
| Jan 31, 2017 at 15:58 | answer | added | Nik Weaver | timeline score: 12 | |
| Jan 31, 2017 at 15:58 | comment | added | Todd Trimble | I think the meta-theory for interpreting SEAR in ZF is nothing more than first-order logic: one just makes the necessary definitions directly in the theory. In the other direction, interpreting ZF in SEAR, we define ZF-sets as equivalence classes of certain well-founded graphs, as described in the nLab article on pure sets ncatlab.org/nlab/show/pure+set, so it looks like some set theory is being invoked there. But I'm supposing nothing more than that (compare the distinction between set and 'setoid': ncatlab.org/nlab/show/equivalence+relation). | |
| Jan 31, 2017 at 13:20 | review | First posts | |||
| Jan 31, 2017 at 13:22 | |||||
| Jan 31, 2017 at 13:17 | history | asked | user103598 | CC BY-SA 3.0 |