Comment by spekcular | Hacker News Reader

Comment by spekcular | Hacker News Reader

Parent Full thread

> I came to a different conclusion: they very much meant to ground mathematics in ZFC formalisms — and went to the effort of projects like Principia trying to achieve that. ZFC was a failure in this regard, almost immediately replaced by category theory and type theory.

ZFC hasn't been "replaced" by anything. The standard line in all published textbooks that I'm aware of is that ZFC is the accepted (by the professional mathematical community) foundation for doing mathematics (assuming this question is even raised). Even the type theorists admit this!

> That’s why we replaced Turing machines with type theories, lambda calculus, automata, etc. Our modern research uses these formalisms because they’re outright better.

The Turing machine is a fundamental concept in theoretical CS that isn't going anywhere. Consider that the standard textbook on the theory of computation (Sipser's) has three parts, and the second is entirely devoted to studying computability using the Turing machine concept. Or that the strength of pushdown automata is usually explained in relation to Turing machines.

> OK, so what are the concrete fruits of this?

The first two things you listed are not metamathematical statements. I'm not sure what you mean by the third. (Sure, many things can be recognized as special cases of category-specific concepts. But that's a claim about category theory, not HoTT.)

> This is also a weird demand while leading off with how people don’t actually work in ZFC.

People do not write their papers in first order logic starting from the ZFC axioms, that's true. But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.

> Nevertheless, topos theory is what explains the algebra-geometry duality: you have two languages (type theories) that map to isomorphic categories. You can then extend that idea to things like the Curry-Howard square.

OK, so what's the actual concrete statement an ordinary mathematician should be interested in?

> ZFC hasn't been "replaced" by anything.

My experience is the opposite: ZFC hasn’t been “replaced” in the sense that it never was - we always used an intermediate language of established theory which we compiled to ZFC. ZFC never formalized all of mathematics, as the high level congruences that drove category theory were always developed on an independent framework. Further, computers always were grounded in type theory and diagram equivalence (literally, the correspondence between circuit diagrams and type theories).

> But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.

Are there any which don’t exclusively apply to the mechanics of set theory itself?

> The first two things you listed are not metamathematical statements.

I noted fruits ranging from applied mathematics (eg, computer products) to meta mathematics; I think it’s important to understand applications as well.

> OK, so what's the actual concrete statement an ordinary mathematician should be interested in?

That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects:

- we can encode proof engines as difference equations to run in GPUs

- we can extract some “effective type theory” from difference equations interpreted as diagrams, which preliminary results suggest also relates to convolutions

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).

> 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.

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.

> 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.

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.

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.

What's accepted by mathematicians as the foundation of mathematics is an objective fact about the mathematical community. You can look up the answer to the question "What is the standard, commonly accepted foundation for mathematics?" in any number of reference books. Some options to get you started: Kunen's Foundations of Mathematics; Jech's Set Theory (super common books for graduate students).

My challenge to you: find a single book written in the last, say 50 years, where the answer to this question is not ZFC (or ZF with some equivocation about whether we should accept choice).

Re: "Equivalence is equivalent to equality," first of all, most mathematicians would take this to be false. Like, if "x" stands for cartesian product, they would say (A x B) x C and A x (B x C) are different objects. (This is a point commonly made in undergraduate algebra classes, and the reason they would say this is of course they they implicitly think of everything as sets, since set theory is the standard foundation!) They are isomorphic objects, but not equal ones. Second, to the extent that mathematicians suppress isomorphisms like this in their writing, this is not a new observation. We've known that mathematicians do this for decades, and in principle we could always unravel such isomorphisms when writing things down carefully if we needed to. This is not some special insight of HoTT. Compare to the forcing example I gave - this is a genuinely new insight about the Calkin algebra facilitated by "classical" methods of mathematical logic.

Re: DNNs, the question of what is a semantics for DNN does not count as an example, no. What would count: statements about things like consistency, independence, shapes, numbers, etc. It's cool that you can use HoTT for engineering things but it's not an application to discovering new pure mathematics or the consistency/proof strength/independence/etc. of that mathematics. The latter is the usual definition of "metamathematics."

Here's an example of a (true) metamathematical statement: HoTT is consistent if ZFC plus two inaccessible cardinals is consistent. (Interestingly, this is the best argument I'm aware of for the claim that HoTT is consistent, and its power derives largely from the fact that ZFC is the Gold Standard for foundations.)

Facilitating metamathematical inquiry of this kind is perhaps the primary reason mathematicians are still interested in set theory and classical logic. (I include here large cardinals, model theory, etc. For further discussion, see the books I mentioned above.)

Is there actually any proof system running on GPUs?! I'd love to read about that. Afaict it must be super hard because tree manipulation is not great on GPUs...

Nope — research only I’m afraid; and currently just migrating to difference equations in numpy (with a focus on Numba GPU upgrades later).

Currently moving shape types to digital image transforms; next up is Zn.

https://www.zmgsabstract.com/whitepapers/shapes-as-digital-i...

https://www.zmgsabstract.com/whitepapers/shapes-have-operati...

Do not nerd snipe me!

There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's able to check the entire Metamath proof database in a few hundred milliseconds. This is orders of magnitude faster than most other proof systems.

If you did want to manipulate trees on the GPU, then my stack monoid work[1] might be a good basis for it.

Of course, a whole nother direction is to use AI to develop proofs, which is a fascinating and growing area (see Holophrasm[2] and DeepMind work[3]). That of course runs on the GPU.

[1]: https://arxiv.org/abs/2205.11659

[2]: https://arxiv.org/abs/1608.02644

[3]: https://www.deepmind.com/publications/proving-theorems-using...

Would you be willing to elaborate on what you find to be strengths of Metamath Zero?

Reply on news.ycombinator.com