4 ms·
However, the consistency of ZFC can be proved in strongly-typed higher-order theories that subsume ZFC.
by ProfHewitt 7y ago
However, the consistency of ZFC can be proved in strongly-typed higher-order theories that subsume ZFC.
- fipso_act 7y agowhy are you telling me this
- ProfHewitt 7y agoMistake is often made that ZFC is the be-all and end-all ultimate foundation of mathematics. Unfortunately, 1st-order ZFC (often referred to as just "ZFC") is a very weak theory. For example, if O is the type of the ordinals, then O Boolean // type of all functions from ordinals into type Boolean cannot be represented in ZFC because it does not exist in the cumulative hierarchy of sets.
- fipso_act 7y agoNo, I mean, why me, specifically? Did I accidentally say something to give the impression I find your odd rantings interesting? Because if I did, please let me know so I can correct the misunderstanding.
- ProfHewitt 7y agoPersonal insults are not allowed on Hacker News.
- bjornsing 7y agoWhat does that mean though? Does it only mean that ZFC is consistent when subsumed within a strongly-typed higher order theory, or does it mean that ZFC by itself is consistent?
- petters 7y agoThat ZFC by itself is consistent, i.e. you can't find a contradiction.
- ProfHewitt 7y agoThe strongly-typed higher-order theory Ordinals is consistent because it has a unique up to isomorphism model by a unique isomorphism. Consequently, ZFC is consistent because it is a special case of the theory Ordinals.
- fipso_act 7y agoThis is nonsense. It's true; but nonsense nevertheless. Because it gives the misleading impression that you can only prove the consistency of a formal system using a "stronger" system. But that's quite wrong: it only needs to be a different formal system.
- ProfHewitt 7y agoOf course, it isn't "nonsense"; instead simply the state of affairs ;-)