6 ms·

Complementary foundations for mathematics: when do we choose? [pdf]

85 points by hackandthink 4y ago

hackandthink 4y ago
"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."
- deleted 4y ago
  [deleted]
082349872349872 4y ago
I liked the notion of only working with foundations up to isomorphism
dboreham 4y ago
Time for metafoundations.
- deleted 4y ago
  [deleted]
- klyrs 4y ago
  They do that in the Philosophy department.
zozbot234 4y ago
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.
revskill 4y ago
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".
- deleted 4y ago
  [deleted]
- hgsgm 4y ago
  RDBM is based on Set Theory.
- helpfulrander 4y ago
  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)
FranchuFranchu 4y ago
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.
layer8 4y ago
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?
- zozbot234 4y ago
  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.
  - layer8 4y ago
    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.
    - zozbot234 4y ago
      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.
      - layer8 4y ago
        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.

85 points by hackandthink 4y ago

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

deleted 4y ago
[deleted]

082349872349872 4y ago

I liked the notion of only working with foundations up to isomorphism

dboreham 4y ago

Time for metafoundations.

deleted 4y ago
[deleted]
klyrs 4y ago
They do that in the Philosophy department.

zozbot234 4y ago

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.

revskill 4y ago

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

deleted 4y ago
[deleted]
hgsgm 4y ago
RDBM is based on Set Theory.
helpfulrander 4y ago
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)

FranchuFranchu 4y ago

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.

layer8 4y ago

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?

zozbot234 4y ago
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.
- layer8 4y ago
  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.
  - zozbot234 4y ago
    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.
    - layer8 4y ago
      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.