5 ms·

Is it really true that "all of mathematics can be described with sets"?

quantumhobbit 10y ago
Yes. But true in the sense that anything computable can be computed by a Turing machine. sets are universal building blocks but most of the time you want a higher level abstraction.
- deleted 10y ago
  [deleted]
- trurl 10y ago
  "Set theory is the 'assembly language' of mathematics. Type theory is the 'functional language' of mathematics."
  - jonnybgood 10y ago
    According to who? I don't think that's a very good analogy. I think it's better to say type theory is just another language in a 'family of assembly languages'. Its superiority is very debatable and not commonly accepted as a foundation.
    - fmap 10y ago
      I think it's a nice analogy. It's a bit tongue in cheek, but it does give you the right idea when you compare it to programming languages. Set theory is a reductionistic system. It's supposed to give a foundation which is as "small" as possible. In set theory you start with almost nothing and you have to encode all useful concepts into sets before you can start proving/programming. Compare this to Turing machines, where you start with a very primitive model of computation. The first step in most treatments of Turing machines is similar to set theory, you show that some useful concepts (associative memory, high-level control flow, etc.) can be encoded into Turing machines. You then use this encoding to construct arbitrary programs. Type theory starts out with a functional programming language and you derive new concepts from free constructions. In type theory you shouldn't be encoding things at all. You should be describing concepts (~adding an API) and possibly extending your model (~the compiler). As analogies go, I'd say that this one is pretty accurate.
- fmap 10y ago
  It isn't so simple, unfortunately. The idea behind set theory was to describe some universal building blocks of mathematics. The problem is that - unlike in the case of computable functions - such a universal building block can't exist. There's a lot of mathematics which can't be formalized in classical first-order logic with the ZFC axioms. For most things you can get around this by adding enough Grothendieck universes, but this is still incomplete and always will be.

Yes. But true in the sense that anything computable can be computed by a Turing machine. sets are universal building blocks but most of the time you want a higher level abstraction.

deleted 10y ago
[deleted]
trurl 10y ago
"Set theory is the 'assembly language' of mathematics. Type theory is the 'functional language' of mathematics."
- jonnybgood 10y ago
  According to who? I don't think that's a very good analogy. I think it's better to say type theory is just another language in a 'family of assembly languages'. Its superiority is very debatable and not commonly accepted as a foundation.
  - fmap 10y ago
    I think it's a nice analogy. It's a bit tongue in cheek, but it does give you the right idea when you compare it to programming languages. Set theory is a reductionistic system. It's supposed to give a foundation which is as "small" as possible. In set theory you start with almost nothing and you have to encode all useful concepts into sets before you can start proving/programming. Compare this to Turing machines, where you start with a very primitive model of computation. The first step in most treatments of Turing machines is similar to set theory, you show that some useful concepts (associative memory, high-level control flow, etc.) can be encoded into Turing machines. You then use this encoding to construct arbitrary programs. Type theory starts out with a functional programming language and you derive new concepts from free constructions. In type theory you shouldn't be encoding things at all. You should be describing concepts (~adding an API) and possibly extending your model (~the compiler). As analogies go, I'd say that this one is pretty accurate.
fmap 10y ago
It isn't so simple, unfortunately. The idea behind set theory was to describe some universal building blocks of mathematics. The problem is that - unlike in the case of computable functions - such a universal building block can't exist. There's a lot of mathematics which can't be formalized in classical first-order logic with the ZFC axioms. For most things you can get around this by adding enough Grothendieck universes, but this is still incomplete and always will be.