3 ms·

Come on now. I just told in what sense ZFC has not been replaced, and you mentioned something different. No one ever claimed people actually wrote down their pr

Come on now. I just told in what sense ZFC has not been replaced, and you mentioned something different. No one ever claimed people actually wrote down their proofs in ZFC - again, that was never the purpose. > Are there any which don’t exclusively apply to the mechanics of set theory itself? Forcing has been applied to a variety of statements, including those about "normal" mathematics. The first example that comes to mind is the question of whether all automorphisms of the Calkin algebra are inner (Farah, 2011). There are many, many others. > That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects: You have still not given a statement an ordinary mathematician should be interested in! Type theory might good for engineering things - I'm totally on board with that. But if you claim HoTT has meta-mathematical interest, you need to give a meta-mathematical justification. That is, you need to prove something new (and interesting).

zmgsabst 4y ago
> I just told in what sense ZFC has not been replaced, and you mentioned something different. You told me your personal experience with textbooks and I told you mine. That’s how conversations work — why are you upset? You’re also factually wrong: I was pointing out areas of mathematics that (contrary to your claim) were never formalized in ZFC. > You have still not given a statement an ordinary mathematician should be interested in! I don’t think you’re being sincere at this point: the formalisms to accelerate reasoning engines and to extract semantic content of DNNs is of clear interest to many working professionals. - - - - - I think both threads have something in common: You’re dressing up your personal feelings (and ignorance) as grand statements about the field.
- spekcular 4y ago
  It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. The point of my post was not to explain my experience with textbooks, it was to note that you can check virtually any published source on this topic to find a reference for that claim. Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Again, I'll happily admit type theory can be good for engineering stuff. But you claimed it was good for metamathematical inquiry. I'm looking for a statement about things like consistency, independence, shapes, numbers, etc. Set theoretical inquiry gave us tons of those, as I pointed out above.
  - zmgsabst 4y ago
    > It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. This is factually untrue — there a portions of mathematics never formalized on ZFC and there’s not consensus around that. I listed the areas that weren’t formalized on ZFC already. You’re making bullshit up to make your personal biases sound grander than they are. - - - - > But you claimed it was good for metamathematical inquiry. No — you claimed that, as a strawman of my position. But you’re welcome to answer yourself: how do you formalize that equivalence is equivalent to equality without univalence? You’re on a huff, but never addressed the original point. From my very first post. > Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Wrong. We lacked the meta mathematical framework outlining what semantics is to enable us to do that — until HoTT told us that the semantics of a system are in its topology. In that sense, HoTT is merely a fact about topos theory: the topology of your semantic model is the interesting part.
    - spekcular 4y ago
      We've been over this. To say "It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations" is not inconsistent with your claim that "there a portions of mathematics never formalized on ZFC." Both claims are true! Also, re: the mathematical point, I asked above: "What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?" You proceeded to give examples that did not fit this description. If you agree that HoTT is not good for metamathematical inquiry, then great, we agree on something! Also, DNNs are (definitionally) not a topic in pure mathematics.
      - zmgsabst 4y ago
        Yes — we have been over that: multiple independent bases means there’s no “standard” one and you’re projecting your own biases as grand proclamations. I understand your ego doesn’t let you separate your experience from that others may have — and so anyone who doesn’t share your view is “objectively” wrong. That flaw in thinking is common in STEM personalities — but what you’re calling “objective” is your subjective bias. > Also, re: the mathematical point, I asked above: "What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?" I answered in my very first post and reiterated it in the last one, but you still haven’t addressed that: Equivalence is equivalent to equality. How do you formalize that meta mathematical notion in other frameworks? — or are you going to ignore that a third time because you don’t have an answer? > Also, DNNs are (definitionally) not a topic in pure mathematics. Definitionally, the question “what is semantics?” is meta mathematics — even if you apply the answer.

zmgsabst 4y ago

> I just told in what sense ZFC has not been replaced, and you mentioned something different. You told me your personal experience with textbooks and I told you mine. That’s how conversations work — why are you upset? You’re also factually wrong: I was pointing out areas of mathematics that (contrary to your claim) were never formalized in ZFC. > You have still not given a statement an ordinary mathematician should be interested in! I don’t think you’re being sincere at this point: the formalisms to accelerate reasoning engines and to extract semantic content of DNNs is of clear interest to many working professionals. - - - - - I think both threads have something in common: You’re dressing up your personal feelings (and ignorance) as grand statements about the field.

spekcular 4y ago
It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. The point of my post was not to explain my experience with textbooks, it was to note that you can check virtually any published source on this topic to find a reference for that claim. Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Again, I'll happily admit type theory can be good for engineering stuff. But you claimed it was good for metamathematical inquiry. I'm looking for a statement about things like consistency, independence, shapes, numbers, etc. Set theoretical inquiry gave us tons of those, as I pointed out above.
- zmgsabst 4y ago
  > It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. This is factually untrue — there a portions of mathematics never formalized on ZFC and there’s not consensus around that. I listed the areas that weren’t formalized on ZFC already. You’re making bullshit up to make your personal biases sound grander than they are. - - - - > But you claimed it was good for metamathematical inquiry. No — you claimed that, as a strawman of my position. But you’re welcome to answer yourself: how do you formalize that equivalence is equivalent to equality without univalence? You’re on a huff, but never addressed the original point. From my very first post. > Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Wrong. We lacked the meta mathematical framework outlining what semantics is to enable us to do that — until HoTT told us that the semantics of a system are in its topology. In that sense, HoTT is merely a fact about topos theory: the topology of your semantic model is the interesting part.
  - spekcular 4y ago
    We've been over this. To say "It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations" is not inconsistent with your claim that "there a portions of mathematics never formalized on ZFC." Both claims are true! Also, re: the mathematical point, I asked above: "What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?" You proceeded to give examples that did not fit this description. If you agree that HoTT is not good for metamathematical inquiry, then great, we agree on something! Also, DNNs are (definitionally) not a topic in pure mathematics.
    - zmgsabst 4y ago
      Yes — we have been over that: multiple independent bases means there’s no “standard” one and you’re projecting your own biases as grand proclamations. I understand your ego doesn’t let you separate your experience from that others may have — and so anyone who doesn’t share your view is “objectively” wrong. That flaw in thinking is common in STEM personalities — but what you’re calling “objective” is your subjective bias. > Also, re: the mathematical point, I asked above: "What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?" I answered in my very first post and reiterated it in the last one, but you still haven’t addressed that: Equivalence is equivalent to equality. How do you formalize that meta mathematical notion in other frameworks? — or are you going to ignore that a third time because you don’t have an answer? > Also, DNNs are (definitionally) not a topic in pure mathematics. Definitionally, the question “what is semantics?” is meta mathematics — even if you apply the answer.