▲ 85 points
back
16 comments
I really enjoyed reading this. It was mind-opening.
I wonder if in the future, something useful with practical applications will come out from this philosophy, and we'll look back to 2022 the same way we look back to geometers who tried to prove Euclid's fifth postulate.
Very interesting work. It's worth noting that "synthetic" mathematics, in a way, is essentially the math that's easiest to encode and reason about in a proof assistant. So there's a lot of consilience between this and any project aiming at "well-motivated" formal proofs. Understanding what makes proofs "well-motivated" in a subfield of mathematics really does seem to require building its rules of reasoning "synthetically", as if from scratch.
I’m not sure I agree with the analogy between mathematical foundations and programming languages. Arguably, programming languages can be reduced either to a turing machine model or to lambda calculus, plus type systems. Those are the actual foundations, not the individual programming languages. What would be the mathematical-foundation analogy to either turing machines or lambda calculus?
Any Turing-complete programming language can be reduced to any other Turing-complete programming language. A "reduction" is just an implementation. And we don't care about how efficient the reduction is, only that it exist. Efficiency enters afterwards as a separate concern.
Not sure what point you’re making. My concern has nothing to do with efficiency, and the fact of Turing equivalence is exactly part of my point: There doesn’t seem to be an analogous common underlying model like Turing equivalence for the mathematical foundations.
Of course there is; that's what the slide deck ends up discussing at length. What one might say is that there's not a single underlying model; the logical expressiveness of Peano Arithmetic is not the same as ZF set theory, or ZFC which adds choice to ZF. But even in CS we care about sub-Turing computational models.
Yeah, but that lack of a single underlying model is why I don’t agree about the analogy. There is no disagreement about what “computation” means or of what is computationally possible, because we have a single model for that (and the Church–Turing thesis). And that single model is what constitutes the foundation, not the programming languages — which however are presented as foundations in the analogy made in the slides. In comparison, the situation is much less clear-cut and unanimous for the foundations of mathematics.
> Yeah, but that lack of a single underlying model is why I don’t agree about the analogy.
There is no single underlying model for mathematics either. This is a consequence of Godel incompleteness. It holds for both programming languages and math because they're all formal systems, just with different properties.
This is a fair point. The analogy in the slides doesn't say anything about the veracity of mathematical propositions. While the notion of computable is mostly agreed on, it's unclear, for instance, if we should be doing mathematics in a world where the continuum hypothesis is true, false, or independent of our theory.
With that said, one can still adopt the programming language analogy for particular models that the various foundations capture. So you don't have to solve the multiverse problem to use the analogy.[0]
I liked the notion of only working with foundations up to isomorphism
Set is ugly to me, in the meaning of "it's useless in programming".
Function is helpful, but morphism is almost "invisible" in programming course. Noone tells you this is just the morphism in the category of X....
I prefer the pragmatic approach with tons of examples, tutorials, lectures first before teaching purely theoretic "foundation".
sets provide the "identity" function.
essentially, sets underlie the formalism to compute (or not, i.e. not-necessarily compute) whether some X == Y by value (i.e. with reading the content of memory-address (pointer semantics)) and by the memory address as a value (by object in memory)
RDBM is based on Set Theory.
"Coders have individual preferences about programming languages.
So do mathematicians for their foundations.
But still, some programming languages are objectively better at some things. Likewise for mathematical foundations."
Time for metafoundations.
They do that in the Philosophy department.