Timeline for Can Tychonoff's theorem be applied to topological spaces generated by program output in ZFC?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 17, 2021 at 19:13 | comment | added | Asaf Karagila♦ | @Kevin: Yes. That's correct. And now, arguably, you do need a bit of Replacement. | |
| Mar 17, 2021 at 18:42 | comment | added | Kevin Buzzard | Right. All I know about the code is that it is an algorithm which eats a natural number and spits out a term in some first order logic with constants appropriate for ZFC (like power set or notation for products etc), and that this term is guaranteed to represent a unique set. And now I guess that one now does some kind of induction on the (size of the) program to show that this is corresponds to some propositional formula in set theory and now finally you can use replacement to get your actual function. | |
| Mar 17, 2021 at 18:24 | comment | added | Asaf Karagila♦ | @Kevin: So you're asking how to formalise the Haskell program inside set theory? | |
| Mar 17, 2021 at 16:11 | comment | added | JoshuaZ | This makes sense except for the analogy involving the professor at the end which leaves me feeling more confused. | |
| Mar 17, 2021 at 15:29 | comment | added | Kevin Buzzard | Many thanks for these comments. Ok I understand now. I can confirm that the output of my program is a sequence of tokens which can be interpreted as a term in the underlying logic in a sane way. I will edit my question to clarify what I am asking. Just to be clear -- the point I am not clear on is how to make a function (in the sense of ZFC) from my Haskell program. | |
| Mar 17, 2021 at 11:30 | comment | added | Asaf Karagila♦ | The meta-theory is where you prove statements about ZFC. If you are formalising ZFC inside type theory, e.g. as requiring that objects of type $\mathtt{Set}$ have certain properties, then your computer program is in the meta-theory. If you're formalising type theory internal to ZFC, then your computer program is an algorithm that runs inside a universe of ZFC, in which case you can consider its outputs as "completed" (since the universe is static, all the results are already there), and just apply Tychonoff's theorem. | |
| Mar 17, 2021 at 11:14 | comment | added | Kevin Buzzard | It's just a computer program takes in a number and prints out a string. How do I know whether what it's doing is taking place in a metatheory? I'm still confused :-( | |
| Mar 16, 2021 at 13:59 | history | answered | Asaf Karagila♦ | CC BY-SA 4.0 |