Hacker News Reader

Comment by runeblaze | Hacker News Reader

ZF(w or w/o C)/type theory/other foundations of maths are "equally" right? My argument is that even if we are trying to build PAs from scratch, type theory provides tangible benefits to the working mathematician because we can just borrow CS research in many stuffs like proof checking and synthesis.

Of course that is a benefit in the "meta" level, but it is not like ZFC is a better foundation than topoi/types/etc..

View on HN

There is nothing wrong with learning from CS research, but mathematicians are just better at thinking about mathematics than computer scientists are. Would you think in types if you didn't have to do it on a computer in a system designed by computer scientists? No way. Would you think in ZFC? Not really, either. We are now in a moment that might decide for the foreseeable future how we think about math, and we better get it right.

idgi tho. The average working mathematician seldomly thinks about proof theory or how proofs "work". Proof theory if must be put in a single box it is an logician's art, and at that point it is niche enough in both CS and maths that it becomes meaningless to say mathematicians know more about it. Logicians are better at thinking about proofs than either maths people or CS people.

I mean I don't know what you mean by right, but given how type theory/ZFC/categorical foundations there is no clear winner (unless you can make a good argument for set theory as our foundation, because again, the average mathematician seldomly thinks in ZFC), I'd say type theory is quite nice in its computational interpretations so let's go with that.

I also don't want to go there, but obviously research drains manpower and money. If we can get CS people to write PAs we really should do that. They're filthy rich in the grand scheme of research.

How proofs work is really simple. The question is, how do you work inside a proof assistant, which kind of math is easy to express, and what is difficult? If you leave that to the CS people, math will become computer science. The ultimate logician was Gödel, and he clearly was a mathematician.

What do you have to say about Curry-Howard?

Most overrated isomorphism in the history of machine-assisted proof.

> How proofs work is really simple

idgi. If you do your 101 logic class often you learn natural deduction, and how do you formalize natural deduction in a computer system? (Hint: type theory is "natural" for this).

Also how proofs work is far from simple.

How proofs work is pretty simple, and you don't need types to do natural deduction. As usual, types only complicate the picture. Here is a more straightforward and natural way to treat natural deduction: http://abstractionlogic.com .

sure of course one does not need types to do natural deduction… if you throw what you showed me to your average maths undergrad in the US they will get confused — I truly don’t see how proofs are simple

It is a matter of presentation and what people are used to. In particular, in abstraction logic, in the simplest (and most general!) case, you only have these proof rules: Axiom, Assume, AddAnte, BindAnte, FreeAnte, InferAnte. If we just focus on this case, we can choose simpler names for these rules: Axiom, Assume, Add, Bind, Free, Infer. That's it. That is all there is to proof.

Reply on news.ycombinator.com