Timeline for Cauchy reals and Dedekind reals satisfy "the same mathematical theorems"
Current License: CC BY-SA 4.0
22 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 19, 2019 at 8:25 | comment | added | Andrej Bauer | I rest my case :-) | |
| Jul 18, 2019 at 14:35 | comment | added | François G. Dorais | ... the issue is that I require $\phi(A)$ to be a formula in the language of set theory. I do not allow new symbols for then I would have to factor these into the (otherwise trivial) translation from $V$ to $V(A)$. This is important but it is not restrictive. It does, however, put additional burden on the "formalizer" who has to fully translate BSD (to keep the same example) in the language of set theory prior to applying the metatheorem. That is a massive task! | |
| Jul 18, 2019 at 14:27 | comment | added | François G. Dorais | @AndrejBauer It looks like we're trying to solve different problems. From my point of view, scaling isn't an issue at all but from your perspective it looks like a major endeavor. But something you said in passing gave me a hunch... In my view, I prove a metatheorem: If $\phi(A)$ is a statement in the language of set theory meeting this and that syntactic requirement, then ZFC proves the universal closure of $(\forall A, A')(A \cong A' \to \phi(A) \to \phi(A'))$. I'm being deliberately vague about the syntactic requirements and I originally thought that was the issue but I now think ... | |
| Jul 18, 2019 at 14:04 | comment | added | François G. Dorais | @Pierre-YvesGaillard $V(A)$ is a model of ZFA, where the elements of $A$ are the atoms. In ZFA, atoms have no elements (and extensionality is slightly modified to allow this). Inside $V(A)$ there is no way to know what the atoms originally contained. In both cases you propose $V_1(A) = \{\ast,\varnothing,\{\ast\}\}$, where $\ast$ denotes the atom. | |
| Jul 18, 2019 at 11:55 | comment | added | Pierre-Yves Gaillard | @FrançoisG.Dorais - What do you exactly mean by "if $A'$ is any isomorphic structure to $A$, then the isomorphism of $A'$ and $A$ lifts uniquely to an isomorphism of $V(A')$ and $V(A)$"? [I'm asking this because it seems to me that $A'$ equipotent to $A$ does not imply $V_1(A')$ equipotent to $V_1(A)$ --- take $A=\{\varnothing\},A'=\{\{\varnothing\}\}$.] | |
| Jul 18, 2019 at 7:27 | comment | added | Andrej Bauer | Mizar is written in something that is more type theory than set theory, even though at the bottom there is ZFC. This is not meant as a criticism, only an observation. People who have never tried to formalize mathematics are unaware of many "engineering" problems that crop up, and some may even underestimate them or dismiss them. That's why I am interested in @FrançoisG.Dorais suggestion: I don't see how to make it scale. It solves nicely a single problem, but how would it work if many people used it to formalize many chapter of mathematics? How would they combine their work? | |
| Jul 18, 2019 at 1:08 | comment | added | Mario Carneiro | @AndrejBauer Umm... I guess that depends on what counts as "decent", but Metamath and Mizar are both significant formalized bodies in ZFC or a very close cousin. Not all formalized systems use type theory. As for "enjoyable", there's no accounting for taste but I enjoy it quite a bit. Frankly the foundational system doesn't matter too much when it comes to the game-like feeling of formalization, so I would guess you are already familiar with it. | |
| Jul 17, 2019 at 17:15 | comment | added | Andrej Bauer | @WillSawin: nobody knows because nobody's ever formalized any decent amount of mathematics in ZFC (extended with definitions of new symbols and operations, say), as far as I know. Who knows, perhaps it's enjoyable. | |
| Jul 17, 2019 at 15:46 | comment | added | Will Sawin | @AndrejBauer I don't think anyone claimed that formalizing mathematics in ZFC was a fun and relaxing experience. | |
| Jul 17, 2019 at 15:40 | comment | added | François G. Dorais | Also keep in mind that the point is not to move into $V(A)$. The point is to transfer a statement $\phi(A)$ to a statement $\phi(A')$ where $A$ and $A'$ are isomorphic structures in $V$. The point of $V(A)$ is to do this in three easy steps: the transfer from $\phi(A)$ in $V$ to $\phi(A)$ in $V(A)$ is literal (modulo some cosmetic stuff implementing the parenthetical note in the second paragraph), the transfer from $\phi(A)$ in $V(A)$ to $\phi(A')$ in $V(A')$ is through the isomorphism $V(A) \cong V(A')$, and the transfer from $\phi(A')$ in $V(A')$ to $\phi(A')$ in $V$ is again literal. | |
| Jul 17, 2019 at 15:24 | comment | added | François G. Dorais | @WillSawin is right, there is no need to atomize any external structure. Any set theoretic construct on top of $A$ is literally in $V(A)$, no matter how complex that construct is. Everything about $A$ in $V$ transfers exactly to $V(A)$. That's the point of going to the length of building the entire hierarchy on top of $A$ rather than stopping after 15 steps, or selecting what you want or don't want, or doing anything specific to the statement to be transferred. | |
| Jul 17, 2019 at 15:24 | comment | added | Andrej Bauer | I feel like I am programming in a mix of assembly and COBOL. | |
| Jul 17, 2019 at 15:12 | comment | added | Will Sawin | @AndrejBauer i.e. a topological space is a set $A$ with a distinguished element of $\mathcal P (\mathcal P(A))$ satisfying some axioms, and all statements in the language of $V(A)$ with an extra constant symbol for this distinguished element are invariant under the usual notion of isomorphism of topological spaces. | |
| Jul 17, 2019 at 15:06 | comment | added | Will Sawin | @AndrejBauer This seems very similar to the Bourbaki structured set approach, which can handle topological spaces but not certain other stuff like sheaves IIRC. One doesn't view the open sets as elements of the structured set $A$, but rather as part of the structure. | |
| Jul 17, 2019 at 14:08 | comment | added | Andrej Bauer | There is a general problem with any suggestion that tailors the formal system, the language, or the model, to the theorem or structure at hand, namely, that it becomes unclear how we're going to combine all these custom-made gadgets together into a beautiful cathedral of mathematics. A computer scientists would say that such solutions are not modular or composable. I would be deligthed to be wrong about this point. | |
| Jul 17, 2019 at 14:05 | comment | added | Andrej Bauer | Does your theorem cover topological spaces as structures? The topology is a family of opens, and there will be theorems that look at elements of those opens, so will have "$\Box \in a$" thingy in them, no? | |
| Jul 16, 2019 at 17:42 | comment | added | François G. Dorais | Ok. What's the issue with $V(A,B,C)$? You can iterate the construction as much as you want. But that's not necessary, the Theorem proved by this argument is that if you have any set theoretic statement about a structure $A$ that doesn't contain $\in a$ for $a \in A$, then the statement holds for any isomorphic structure $A'$. You can apply this to all the parameters of a statement. | |
| Jul 16, 2019 at 15:55 | comment | added | Andrej Bauer | I am afraid that does not answer my question. If my theorem and proof mention structures $A$, $B$ and $C$, then I need $V(A,B,C)$ so that I can replace either one with an isomorphic copy. If you are suggesting that I should use $V(A)$, inside of which I can find $B$ and $C$ as elements of $V$, then I cannot vary $B$ and $C$ isomorphically. | |
| Jul 16, 2019 at 14:34 | comment | added | François G. Dorais | @AndrejBauer: The pure set part of any $V(A)$ is a copy of $V$. So $V(A)$ knows everything that happens in $V$. | |
| Jul 16, 2019 at 14:03 | comment | added | Andrej Bauer | But what if the mathematical statement, in addition to mentioning $A$, mentions some other mathematical structures, such as the integers, and some sheaf cohomology, and half of Lange's algebra book? Will you just keep accummulating stuff and build $V(\mathrm{stuff})$? If so, how are we ever going to relate theorems stated in $V(\mathrm{stuff}_1)$ from Paper 1 to theorems stated in $V(\mathrm{stuff}_2)$ from Paper 2? | |
| Jul 16, 2019 at 1:27 | history | edited | François G. Dorais | CC BY-SA 4.0 |
typos
|
| Jul 16, 2019 at 1:15 | history | answered | François G. Dorais | CC BY-SA 4.0 |