Timeline for Set theories without "junk" theorems?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 11, 2023 at 16:48 | comment | added | Thorsten Altenkirch | @JacquesCarette Indeed, however, Junk theorems are also absent from pre HoTT Type Theory. The strange thing about ITT is that you cannot define any property that distinguishes different presentations but you cannot show that they are equal either. | |
| Sep 8, 2023 at 0:08 | comment | added | Jacques Carette | HoTT was still very very young 5.5 years ago when that comment was first written @ThorstenAltenkirch ! Things are still evolving indeed. | |
| Sep 6, 2023 at 11:14 | comment | added | Thorsten Altenkirch | @JacquesCarette why is HoTT anachronistic? If it hasn't reached the collective consciousness maybe it should. actually it seems that formal verification using Type Theory is becoming more widespread, e.g. using systems like Coq or Lean. Yes, these systems don't implement HoTT and univalence but they already exclude junk theorems. In a way you have the pain without the benefits. | |
| Mar 8, 2019 at 17:22 | comment | added | Asaf Karagila♦ | @David: Serving someone junk covered in sugar might taste sweet, but it's still junk. To claim that ETCS or HTT removing junk theorems is the very definition disingenuous, at best they make it slightly less natural to pronounce the junk, but it's there just as well. And arguably, asking in a ZFC context whether or not "is $\pi$ an ordered pair?" should receive an answer of "how did you code $\pi$ and how did you code ordered pairs?". | |
| Mar 7, 2019 at 23:41 | comment | added | David Roberts♦ | I wouldn't say "3 is a member of 7", but rather make the coding explicit: "3 is a member of the set corresponding to 7". It's like power sets in ETCS: their elements aren't literally subsets, but we talk as if they are, hiding the correspondence under sugaring. | |
| Mar 7, 2019 at 16:28 | comment | added | Asaf Karagila♦ | @David: Yes, I know that there are situations where the set of reals can be injectively mapped into the natural numbers, but there is no bijection between them. That was one of the "Whoa..." moments I've had on this site before. But nevertheless, I think that the bijection between $\Bbb N$ and $\Bbb{N\times N}$ is as constructive as it gets, at least the Cantor pairing one. So very easily we can code finite sets of natural numbers as natural numbers. Even though the natural numbers are not "intrinsicly set theoretic objects". And then we can ask if $3$ is a member of $7$, for example. | |
| Mar 7, 2019 at 3:05 | comment | added | David Roberts♦ | @Adam I wouldn't say $A=B$ is defined to be the type $A\simeq B$ in UF/HoTT. It's an axiom in UF/HoTT that the canonical map $A=B \to A \simeq B$ has contractible fibres. Or in flavours of cubical type theory it's a theorem that this is the case. | |
| Mar 7, 2019 at 3:03 | comment | added | David Roberts♦ | @Asaf Note that constructively one needs to be clear what "$\mathbb{R}$" means. If $\mathbb{R} = 2^\mathbb{N}$ (the set of functions), then $2^\mathbb{N} = 2^{\mathbb{N}\sqcup \mathbb{N}} = 2^\mathbb{N}\times 2^\mathbb{N}$, where by $=$ I mean isomorphic. Choosing a decomposition $\mathbb{N} = \mathbb{N}\sqcup \mathbb{N}$ for instance into odds and evens gives the isomorphisms canonically. If one means Dedekind cuts, and is working in a framework with Dedekind cuts ≠ Cantor–Cauchy reals, then it's a bit more involved... | |
| Feb 14, 2019 at 11:05 | comment | added | Asaf Karagila♦ | Are you saying that in type theory there is no way to prove that $\Bbb R$ and $\Bbb R^2$ have the same cardinality, or that the Cantor space is isomorphic to its square? | |
| Feb 13, 2019 at 23:43 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
tidying up
|
| Mar 26, 2018 at 21:48 | comment | added | Carl Mummert | The inability to ask meaningless questions would come from any type theory. Even Peano arithmetic, though perhaps not very expressive, has the property that there are no junk theorems: every term represents a number and every atomic sentence represents an honest relationship between numbers. | |
| Mar 25, 2018 at 1:44 | comment | added | Jacques Carette | Yes - but the answer you give is close to anachronistic. HoTT hadn't really reached the collective consciousness yet. | |
| Mar 24, 2018 at 16:49 | history | answered | Adam P. Goucher | CC BY-SA 3.0 |