Timeline for Is material set theory conservative over structural set theory?
Current License: CC BY-SA 4.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 22, 2021 at 14:31 | comment | added | Tom Leinster | @PeterLeFanuLumsdaine That's very mysterious of you, and I'll believe it when I see it. I've sent you an email asking for one example. | |
| Jul 5, 2021 at 11:29 | comment | added | Peter LeFanu Lumsdaine | @TomLeinster: I’d argue there are certainly “junk theorems” in ETCS (also in dependent type theories, and just about any other foundational system I’ve seen or can imagine). Going into this carefully is too long for a comment — if you ask a new question and ping me here, I can give it as an answer there, or else by email if you’d rather! | |
| Jun 4, 2021 at 22:05 | comment | added | Tom Leinster | Final point for now: in my first comment, I said that I'd never seen anyone succeed in producing a "junk theorem" in ETCS that doesn't involve an abuse of notation. If you allow yourself to abuse notation, e.g. referring to an injection $i: A \to X$ as just "$A$", it's easy. But that says nothing about ETCS: in any mathematical context whatsoever, you can get meaningless statements by abusing notation in an unwise way. | |
| Jun 4, 2021 at 22:05 | comment | added | Tom Leinster | Generally, an $I$-indexed family of elements of a set $X$ is the same as a function $I \to X$ (and is usually defined that way). But we use different language for families and functions, even though they're formally identical. And that's fine -- we translate back and forth without a second thought. The case $I = \mathbb{N}$ is sequences; the case $I = 1$ is elements. | |
| Jun 4, 2021 at 22:04 | comment | added | Tom Leinster | In exactly the same way, ETCS defines an element of a set $X$ as a function $1 \to X$ (where $1$ is a fixed terminal set). Officially, we could ask whether an element of $X$ is surjective. No one uses that language, but it is a meaningful question ("is $x$ the only element of $X$?") phrased in an unusual way. The strange possibility of asking whether an element "is surjective" should not be seen as a drawback of the ETCS definition of element, any more than for sequences. | |
| Jun 4, 2021 at 22:04 | comment | added | Tom Leinster | For comparison, consider sequences. Everyone defines a sequence in a set $X$ as a function $\mathbb{N} \to X$. So officially, we could ask whether a sequence in $X$ is surjective. No one uses that language; we say "exhaustive" or some such. But if we did say a sequence was surjective, it would be a meaningful statement phrased in unusual language. And the strange possibility of asking whether a sequence "is surjective" is not seen as a drawback of the formal definition of sequence. | |
| Jun 4, 2021 at 22:03 | comment | added | Tom Leinster | ETCS (and the apparatus around it) sometimes produces statements that are perfectly meaningful but phrased in unusual language. This is not the same as a "junk theorem" - a term I don't like, but which I take to mean "theorem about meaningful entities that is only true because of arbitrary hidden conventions". | |
| Jun 4, 2021 at 22:03 | comment | added | Tom Leinster | I've never seen an example of a "junk theorem" in ETCS that doesn't involve an abuse of notation. That's despite how often this topic comes up on MO, and despite all the comments it tends to attract. I don't believe such examples exist. | |
| Mar 29, 2021 at 20:43 | history | became hot network question | |||
| Mar 29, 2021 at 14:59 | comment | added | Asaf Karagila♦ | @Simon: I'm sorry if I'm somewhat aggressive here. My point here is that people treat this as a good reason to think that ZFC is not "worth the effort", and in a world where I repeatedly hear about how set theory "is dying out", repeating these claims that somehow structural set theory is "free of junk" is both false and damaging to an entire field of mathematics. So I get a bit anxious when I see it. | |
| Mar 29, 2021 at 14:33 | comment | added | Simon Henry | @AsafKaragila I wasn't casting any judgment of value on material vs structural set theories. I was just clarifying what is meant by "global $\in$ relation" and not using it as it seemed it was unclear. But If you want to go down that road again, I am pretty sure analyst are pretty happy to know that the range of $3$ only has one element, once you told them you are just calling 3 the function $* \mapsto 3$, which I think is a notation they would agree with ;-) | |
| Mar 29, 2021 at 14:17 | comment | added | Asaf Karagila♦ | @Simon: Yes, that wasn't a great example. You can ask if $\sqrt2$ and $e$ are isomorphic or what are the domain and range of $3$, and many other questions that you can cast in a way that makes sense, whereas an analyst will simply blink and tell you to stop talking nonsense... :) | |
| Mar 29, 2021 at 14:03 | comment | added | Simon Henry | @AsafKaragila I'm not sure what is your point here ? I guess if you work in a theory that identifies elements of a set with functions from the singleton then it does. is that what you mean ? In that case then that's definitely not a meaningless statement: It is about whether there exists other real number than $\sqrt{2}$, I think that's a question we might want to know the answer to ! | |
| Mar 29, 2021 at 13:58 | answer | added | Simon Henry | timeline score: 11 | |
| Mar 29, 2021 at 13:56 | comment | added | Asaf Karagila♦ | @Simon: In structural set theory it makes sense to ask "is $\sqrt2$ surjective?" | |
| Mar 29, 2021 at 13:16 | comment | added | Simon Henry | @Wojowu in material set theories like ZF you are allowed to use the $\in$ or $=$ relation for arbitrary sets (it makes sense to ask whether $2 \in \pi$ or $exp = \mathbb{Q}$). In a structual set theories it only makes sense to ask whether two elements of a same sets are equal, or whether an element of a set X belong a subset U of X. I think the concrete formulation of the question is "Given a statement in the language of, say, ETCS which can be proved - when translated - in bounded ZF, can it be proved in ETCS ?" | |
| Mar 29, 2021 at 13:04 | comment | added | Monroe Eskew | It depends on the specific theories involved. | |
| Mar 29, 2021 at 12:51 | comment | added | Wojowu | What is "global $\in$-relation" and "global $=$-relation", and what does it mean to (not) use them in an "essential way"? | |
| Mar 29, 2021 at 12:42 | review | First posts | |||
| Mar 29, 2021 at 13:08 | |||||
| Mar 29, 2021 at 12:39 | history | asked | user177848 | CC BY-SA 4.0 |