4 ms·

Sure. Most mathematicians think it's true that ZFC is consistent; but that can't be proved in ZFC. mic drop/Halmos block

ProfHewitt 7y ago
However, the consistency of ZFC can be proved in strongly-typed higher-order theories that subsume ZFC.
- fipso_act 7y ago
  why are you telling me this
  - ProfHewitt 7y ago
    Mistake 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 ago
      No, 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 ago
        Personal insults are not allowed on Hacker News.
- bjornsing 7y ago
  What 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 ago
    That ZFC by itself is consistent, i.e. you can't find a contradiction.
  - ProfHewitt 7y ago
    The 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 ago
  This 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 ago
    Of course, it isn't "nonsense"; instead simply the state of affairs ;-)
bjornsing 7y ago
Most mathematicians probably think the Riemann conjecture is true, but that wasn’t what I meant. I should probably have said “consider proven”.
- fipso_act 7y ago
  Okay, well that's easy, too. ZFC has been proven consistent in other formal systems. For instance, you can prove ZFC consistent using Morse-Kelley theory: https://en.wikipedia.org/wiki/Morse%E2%80%93Kelley_set_theory https://en.wikipedia.org/wiki/Morse%E2%80%93Kelley_set_theor.... Which is a "stronger" theory than ZFC; but you can also prove ZFC consistent in a system consisting of ZFC plus the axiom that "ZFC is consistent"; or indeed, in weaker theories than ZFC, augmented with the axiom that "ZFC is consistent".
  - bjornsing 7y ago
    Doesn’t your example of an axiom that “ZFC is consistent” show of how little use proofs within stronger systems are? I at least feel tempted to say that proofs of ZFCs consistency within stronger systems tell you nothing about ZFCs consistency.
    - fipso_act 7y ago
      They most certainly do, though! They do tell you something about the consistency of ZFC; they tell you that if the system you're working in is consistent, then so is ZFC. Is that not worth knowing? It does sound a bit like you want something out of formal systems that they just can't give you, which is "absolute" truth. edited to add: It's also worth noting that very, very few mathematicians care about actually formalising proofs in a formal system - it's a niche area. The vast majority of mathematicians go on about their business without giving much thought to ZFC and its axioms at all. Many can't even name them all. (I know this, because they are quite surprised when you tell them what some of the axioms are. Especially the Axiom of Infinity.) Lol, I probably can't either,I suspect I would miss a few if I did it off the top of my head.
      - 7y ago

ProfHewitt 7y ago

However, the consistency of ZFC can be proved in strongly-typed higher-order theories that subsume ZFC.

fipso_act 7y ago
why are you telling me this
- ProfHewitt 7y ago
  Mistake 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 ago
    No, 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 ago
      Personal insults are not allowed on Hacker News.
bjornsing 7y ago
What 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 ago
  That ZFC by itself is consistent, i.e. you can't find a contradiction.
- ProfHewitt 7y ago
  The 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 ago
This 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 ago
  Of course, it isn't "nonsense"; instead simply the state of affairs ;-)

bjornsing 7y ago

Most mathematicians probably think the Riemann conjecture is true, but that wasn’t what I meant. I should probably have said “consider proven”.

fipso_act 7y ago
Okay, well that's easy, too. ZFC has been proven consistent in other formal systems. For instance, you can prove ZFC consistent using Morse-Kelley theory: https://en.wikipedia.org/wiki/Morse%E2%80%93Kelley_set_theory https://en.wikipedia.org/wiki/Morse%E2%80%93Kelley_set_theor.... Which is a "stronger" theory than ZFC; but you can also prove ZFC consistent in a system consisting of ZFC plus the axiom that "ZFC is consistent"; or indeed, in weaker theories than ZFC, augmented with the axiom that "ZFC is consistent".
- bjornsing 7y ago
  Doesn’t your example of an axiom that “ZFC is consistent” show of how little use proofs within stronger systems are? I at least feel tempted to say that proofs of ZFCs consistency within stronger systems tell you nothing about ZFCs consistency.
  - fipso_act 7y ago
    They most certainly do, though! They do tell you something about the consistency of ZFC; they tell you that if the system you're working in is consistent, then so is ZFC. Is that not worth knowing? It does sound a bit like you want something out of formal systems that they just can't give you, which is "absolute" truth. edited to add: It's also worth noting that very, very few mathematicians care about actually formalising proofs in a formal system - it's a niche area. The vast majority of mathematicians go on about their business without giving much thought to ZFC and its axioms at all. Many can't even name them all. (I know this, because they are quite surprised when you tell them what some of the axioms are. Especially the Axiom of Infinity.) Lol, I probably can't either,I suspect I would miss a few if I did it off the top of my head.
    - 7y ago