7 ms·

Why is dependent type theory more suitable than set theory for proof assistants?

221 points by pgustafs 6y ago

tlringer 6y ago
The idea of Lean being suitable for all of math is sensationalist and Kevin knows it. Lean being committed to UIP already rules out many kinds of mathematics. Furthermore, the kind of automation possible in Lean is also possible in univalent theorem provers with the right implementation (e-graphs). They are actually easier in cubical than in Lean (see the 2 pager by Bas Spitters and his masters student). The difference is that no cubical proof assistant has been implemented by Leo de Moura. Get Leo de Moura to implement cubical, and you will have a proof assistant more powerful than you could ever imagine, built on extremely satisfying foundations.
- JoeCamel 6y ago
  I'm a beginner in proof assistents, can you give some examples of many kinds of math ruled out? And what is UIP?
  - bollu 6y ago
    UIP is "unicity of identity proofs". I think this will rule proofs where we wish to talk about proofs of equality of two objects. I don't know off the top of my head any math that wants to do such a thing, but I'm far from an expert.
  - TheAsprngHacker 6y ago
    UIP is uniqueness of identity proofs. It's an axiom that says that all proofs of x = y (that two terms are propositionally equal) are the same. Now, UIP is valid if the only way of proving an equality is to show that the two terms are definitionally equal. However, there are various type theories, such as Homotopy Type Theory, in which this axiom does not hold because propositional equality can have other proofs.
- ianandrich 6y ago
  Are you talking along the lines of the red family of provers? What makes the cubical approach more powerful? What makes lean weak?
  - tlringer 6y ago
    There is RedPRL, there is also cubical Agda. I think cubical Agda is the best developed so far. It lacks automation. But that is not fundamental, it is thanks to the philosophies of the people involved. Lean is not weak, it just commits to something called Uniqueness of Identity Proofs (UIP). This is inconsistent with Univalence, a property that cubical type theories have. Necessarily, neither system can express "all of math." So it goes. Leo chose UIP to get a novel way to get really powerful automation of equality proofs. Leo is very, very good at this; this is his whole shindig. But he had to hack around things a bit in order to get what he wanted. The paper by Bas and his student shows that in cubical, you don't have to hack around things; this automation of equality proofs arises in the natural way. The gap is not fundamental, and it irritates me when it is attributed to the choice of UIP. The reason Lean is so useful is because the people working on it are good at building automation. The people working on cubical are much more interested in foundations. We need people who are interested in automating cubical; once we get that, the proof assistant that arises from it will be better than anything we have ever seen.
    - creata 6y ago
      Do you have any introductory material on cubical type theory, suitable for the average mathematician? The type theory in Lean feels dead simple to me, but all the online resources on cubical type theory feel impenetrable.
      - tlringer 6y ago
        I like these lecture notes: https://staff.math.su.se/anders.mortberg/papers/cubicalmethods.pdf https://staff.math.su.se/anders.mortberg/papers/cubicalmetho... But if that is too hard to read, I recommend telling Anders directly when you get confused. He is open to improving the notes.
- lakecresva 6y ago
  Can you give a practical example of how denying UIP helps with tasks like writing a proof or a definition rather than defining a really exotic inductive type?
- voxl 6y ago
  Lean is a classical theory, I don't see how any intuitionistic theory can hope to possibly compete. A mathematician would laugh you out of the store if you tried to get them to used cubical Lean (Lean 2 by the way implemented HoTT ideas) and give up classical logic. The HoTT people are doing good work and I don't doubt that automation can help with the _significant_ additional complexity of higher dimensional cubes, but that's not really all that would be missing. Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical logic seriously (postulating an axiom doesn't count).
  - logicchains 6y ago
    >Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical logic seriously (postulating an axiom doesn't count). Correct me if I'm wrong (I may well be), but couldn't one work classically just by sticking to (-1)-truncated types ("mere prepositions") in a HOTT based system, for which LEM is true by default?
    - hejsansvejsan 6y ago
      LEM for mere propositions is not "true by default", but it is consistent with univalence. So you can take it as an axiom.
  - zozbot234 6y ago
    Proving "classical" propositions in an intuitionistic system is trivial. Intuitionistic logic can be viewed as an extension of classical logic with new "constructive OR" and "constructive EXISTS" operators. The classical operators are recovered via negation: NOT (NOT a AND NOT b) is classical OR, whilst NOT FORALL x (NOT p) is a classical existential quantifier.
  - hejsansvejsan 6y ago
    I'm confused by "postulating an axiom doesn't count". Are you aware that choice is an axiom in Lean? https://github.com/leanprover-community/lean/blob/master/library/init/classical.lean#L13 https://github.com/leanprover-community/lean/blob/master/lib...
- throwaway45434 6y ago
  At least 99% of all mathematicians in academia work with classical logic only, and a good fraction hasn't even heard of anything else. So yeah, Lean might not be suitable for some of the remaining 1%, but that doesn't make Kevin's claim "sensationalist".
  - tlringer 6y ago
    It does. And if classical logic is what they like, they can use Isabelle/HOL just as nicely. It is classical. It has wonderful automation. Kevin gets attention because he is bold, not because he is correct. Anonymous comments are cowardly; please show yourself. If you stay anonymous I am not aware of power dynamics, and I cannot adjust my response accordingly.
    - JoeCamel 6y ago
      Saying Lean "rules out many kinds of mathematics" and not giving a single example, sounds more sensationalist to me. I also don't see what's wrong with anonymous comments as long as they are constructive and people are nice. I don't know Kevin as well as you do (apparently) but maybe he is just ignorant on the topics you know so much about. Why something gets attention of media (Quanta Magazine?) is complicated. From your comments, you also seem very "bold".
      - tlringer 6y ago
        I'm a woman though, and women rarely get positive attention for anything in CS. I'm bold because as a woman in the field you need to be bold to survive as a researcher. In the type theory and proof assistant worlds there are only a handful of us. A typical ratio at a conference for proof assistant research is 1 woman for every 40 men. Anonymous comments scare me because there are (a few, thankfully not many) abusive people in the PL community I am afraid of engaging with. I don't want to accidentally find myself arguing with one of them. I need to know when to exit the conversation. Proof relevant mathematics, higher category theory, lots of topology. Sorry. I don't spend all of time on HackerNews, I sometimes don't get around to responding to things. I am talking to Kevin about this framing so we can figure out how to make it healthier in the future. Some of my comments about Kevin were likewise out of line because I interpreted some of our previous interactions as rooted in a gender-based power dynamic when they were actually just rooted in something Kevin finds difficult and wants to do better at, and that is my honest mistake.
jakear 6y ago
> A set 𝑋 is jaberwocky when for every 𝑥∈𝑋 there exists a bryllyg 𝑈⊆𝑋 and an uffish 𝐾⊆X such that 𝑥∈𝑈 and 𝑈∈𝐾. Anyone know how this relates to Lewis Carrol?
- creata 6y ago
  Jabberwocky is a poem by Lewis Carroll. https://en.wikipedia.org/wiki/Jabberwocky https://en.wikipedia.org/wiki/Jabberwocky
  - schoen 6y ago
    And the idea in the context of the original post is that this is supposed to be a parody of a formal math definition in a paper or textbook (using Jabberwocky vocabulary instead of real math vocabulary).
    - newen 6y ago
      Not that it makes sense anyway. Somehow 𝑈⊆𝑋 and 𝑈∈𝑋.
      - leanuser83 6y ago
        That is exactly the point being made. That you can spot right away that something "doesn't make sense".
      - skissane 6y ago
        No, the point was that 𝑈∈𝑋 is a typo and 𝑈⊆𝑋 is what was intended. Type theory will reject the mistake but set theory will accept it. This is then presented as a reason why mathematicians should prefer type-theory-based proof assistants to set-theory-based ones, since the former will catch these kinds of mistakes while the later won't.
      - bobbylarrybobby 6y ago
        That’s possible. For instance, X = {{}} and U = {}. Or in general, if X_0 = {} and X_{i+1} = {X_0, ..., X_i}, then X_i is both an element and a subset of X_j whenever i < j.
auggierose 6y ago
Here is a plan to improve proof assistants, and it is based on set theory: https://www.practal.com https://www.practal.com
robinzfc 6y ago
The current tittle of the original MathOverflow question is "What makes dependent type theory more suitable than set theory for proof assistants?", I don't know why is it different than here. The actual question makes more sense because the one on HN suggests that proof assistants exclusively formalize mathematics in dependent type theory (rather than set theory) which is not true. In fact, some proof assistants use dependent type theory (LEAN), some use simple type theory (Isabelle/HOL), some use simple type theory to encode untyped set theory (Isabelle/ZF), some implement kind of "soft typing" on top of untyped set theory (Mizar) and some are completely generic and can encode all of the above (Metamath). As for the question why type theory seems to be more popular in formalization of mathematics recently than set theory Jeremy Avigad wrote a rare compelling explanation [1] of why this is the case. I personally prefer the opinion of Lawrence Paulson [2], the original author of Isabelle and its ZF logic (he also implemented a formalization of ZFC set theory in Isabelle/HOL recently). [1] https://cs.nyu.edu/pipermail/fom/2016-January/019441.html https://cs.nyu.edu/pipermail/fom/2016-January/019441.html [2] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html https://cs.nyu.edu/pipermail/fom/2018-June/021032.html
- OJFord 6y ago
  > The current tittle of the original MathOverflow question is "What makes dependent type theory more suitable than set theory for proof assistants?", I don't know why is it different than here. It's too long for HN, OP presumably reworded to fit. If you have a better suggestion one of the mods might see and change it, I think OP's chance to edit it has passed though.
  - edjrage 6y ago
    "Why is dependent type theory more suitable than set theory for proof assistants?” has 80 characters, which seems to be exactly HN's limit.
    - pgustafs 6y ago
      Yep, that would be a better rewording. I missed it in my search for a <80 character title.
octoberfranklin 6y ago
Program extraction. In dependent type theory if you've proved "A implies B" you can extract from that proof a program that takes an argument of type A and always halts, returning a value of type B. Moreover if you prove some property about proofs that A implies B, you've also proved the corresponding proposition about programs. This means your proofs get to deal with programs directly, rather than having to formalize them as something like Turing machines whose tapes are set-theoretic encodings of lists of integers. It's excruciatingly painful to write non-hand-wavy proofs of anything that way. Hand-wavy proofs that can't be machine-checked aren't so bad of course; complexity theory folks have been doing that for decades. If you aren't proving things about programs or homotopy then there really aren't any obvious reasons to prefer dependent type theory. I say this as somebody who loves programming with dependent types. But I'm being honest here, and I wish more people in the mechanized mathematics world would be honest about this.
- alisonkisk 6y ago
  > there really aren't any obvious reasons to prefer dependent type theory The OP gives a reason, and it's the same reason programs use types. Untyped proofs are usually wrong, like untyped programs.
  - octoberfranklin 6y ago
    Er, no. Even Coq proofs are written in an untyped language (Ltac). You've got your levels mixed up.
  - GregarianChild 6y ago
    HOL is typed, but not a dependent type theory. HOL is also a classical logic. HOL is essentially Alonzo Church's simply typed lambda-calculus [1] from 1940. Classical, rather than constructive logic tends to give shorter proofs. [1] A. Church, A Formulation of the Simple Theory of Types. https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b...
adrian_b 6y ago
Slightly off-topic, but in any mathematical theory concerning a certain restricted domain and also in any theory attempting to cover the entire mathematics there are many possible choices for the primitive concepts and rules. In most cases it is not possible to have an objective criterion for deciding which is the best choice, so the choice remains based on personal preferences. For example, I could never accept the idea that set theory can be considered to belong to the foundations of mathematics. I have always believed that it is more convenient to view the sets not as primitives, but as classes of equivalence of the ordered sequences, which in turn are constructed from ordered pairs, which are a primitive concept. So instead of using set theory as a base, I believe it to be more convenient to start from some primitives that include some of the concepts and operations on which LISP was also based, plus some definitions, which normally are introduced using sets, modified to use ordered sequences instead. All the set theory (and the number theory) can be constructed from these alternative primitive concepts.
- devit 6y ago
  That doesn't work as written for uncountable sets.
  - kmill 6y ago
    That's true, but there's an amusingly odd theorem (downwards Lowenheim-Skolem) that implies that if set theory has a model, it has a countable model. So, in a sense, all sets are countable. I think this just leads you to the next problem, which is that (I think) it would be undecidable normalizing and sorting these sets.

221 points by pgustafs 6y ago

The idea of Lean being suitable for all of math is sensationalist and Kevin knows it. Lean being committed to UIP already rules out many kinds of mathematics. Furthermore, the kind of automation possible in Lean is also possible in univalent theorem provers with the right implementation (e-graphs). They are actually easier in cubical than in Lean (see the 2 pager by Bas Spitters and his masters student). The difference is that no cubical proof assistant has been implemented by Leo de Moura. Get Leo de Moura to implement cubical, and you will have a proof assistant more powerful than you could ever imagine, built on extremely satisfying foundations.

JoeCamel 6y ago
I'm a beginner in proof assistents, can you give some examples of many kinds of math ruled out? And what is UIP?
- bollu 6y ago
  UIP is "unicity of identity proofs". I think this will rule proofs where we wish to talk about proofs of equality of two objects. I don't know off the top of my head any math that wants to do such a thing, but I'm far from an expert.
- TheAsprngHacker 6y ago
  UIP is uniqueness of identity proofs. It's an axiom that says that all proofs of x = y (that two terms are propositionally equal) are the same. Now, UIP is valid if the only way of proving an equality is to show that the two terms are definitionally equal. However, there are various type theories, such as Homotopy Type Theory, in which this axiom does not hold because propositional equality can have other proofs.
ianandrich 6y ago
Are you talking along the lines of the red family of provers? What makes the cubical approach more powerful? What makes lean weak?
- tlringer 6y ago
  There is RedPRL, there is also cubical Agda. I think cubical Agda is the best developed so far. It lacks automation. But that is not fundamental, it is thanks to the philosophies of the people involved. Lean is not weak, it just commits to something called Uniqueness of Identity Proofs (UIP). This is inconsistent with Univalence, a property that cubical type theories have. Necessarily, neither system can express "all of math." So it goes. Leo chose UIP to get a novel way to get really powerful automation of equality proofs. Leo is very, very good at this; this is his whole shindig. But he had to hack around things a bit in order to get what he wanted. The paper by Bas and his student shows that in cubical, you don't have to hack around things; this automation of equality proofs arises in the natural way. The gap is not fundamental, and it irritates me when it is attributed to the choice of UIP. The reason Lean is so useful is because the people working on it are good at building automation. The people working on cubical are much more interested in foundations. We need people who are interested in automating cubical; once we get that, the proof assistant that arises from it will be better than anything we have ever seen.
  - creata 6y ago
    Do you have any introductory material on cubical type theory, suitable for the average mathematician? The type theory in Lean feels dead simple to me, but all the online resources on cubical type theory feel impenetrable.
    - tlringer 6y ago
      I like these lecture notes: https://staff.math.su.se/anders.mortberg/papers/cubicalmethods.pdf https://staff.math.su.se/anders.mortberg/papers/cubicalmetho... But if that is too hard to read, I recommend telling Anders directly when you get confused. He is open to improving the notes.
lakecresva 6y ago
Can you give a practical example of how denying UIP helps with tasks like writing a proof or a definition rather than defining a really exotic inductive type?
voxl 6y ago
Lean is a classical theory, I don't see how any intuitionistic theory can hope to possibly compete. A mathematician would laugh you out of the store if you tried to get them to used cubical Lean (Lean 2 by the way implemented HoTT ideas) and give up classical logic. The HoTT people are doing good work and I don't doubt that automation can help with the _significant_ additional complexity of higher dimensional cubes, but that's not really all that would be missing. Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical logic seriously (postulating an axiom doesn't count).
- logicchains 6y ago
  >Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical logic seriously (postulating an axiom doesn't count). Correct me if I'm wrong (I may well be), but couldn't one work classically just by sticking to (-1)-truncated types ("mere prepositions") in a HOTT based system, for which LEM is true by default?
  - hejsansvejsan 6y ago
    LEM for mere propositions is not "true by default", but it is consistent with univalence. So you can take it as an axiom.
- zozbot234 6y ago
  Proving "classical" propositions in an intuitionistic system is trivial. Intuitionistic logic can be viewed as an extension of classical logic with new "constructive OR" and "constructive EXISTS" operators. The classical operators are recovered via negation: NOT (NOT a AND NOT b) is classical OR, whilst NOT FORALL x (NOT p) is a classical existential quantifier.
- hejsansvejsan 6y ago
  I'm confused by "postulating an axiom doesn't count". Are you aware that choice is an axiom in Lean? https://github.com/leanprover-community/lean/blob/master/library/init/classical.lean#L13 https://github.com/leanprover-community/lean/blob/master/lib...
throwaway45434 6y ago
At least 99% of all mathematicians in academia work with classical logic only, and a good fraction hasn't even heard of anything else. So yeah, Lean might not be suitable for some of the remaining 1%, but that doesn't make Kevin's claim "sensationalist".
- tlringer 6y ago
  It does. And if classical logic is what they like, they can use Isabelle/HOL just as nicely. It is classical. It has wonderful automation. Kevin gets attention because he is bold, not because he is correct. Anonymous comments are cowardly; please show yourself. If you stay anonymous I am not aware of power dynamics, and I cannot adjust my response accordingly.
  - JoeCamel 6y ago
    Saying Lean "rules out many kinds of mathematics" and not giving a single example, sounds more sensationalist to me. I also don't see what's wrong with anonymous comments as long as they are constructive and people are nice. I don't know Kevin as well as you do (apparently) but maybe he is just ignorant on the topics you know so much about. Why something gets attention of media (Quanta Magazine?) is complicated. From your comments, you also seem very "bold".
    - tlringer 6y ago
      I'm a woman though, and women rarely get positive attention for anything in CS. I'm bold because as a woman in the field you need to be bold to survive as a researcher. In the type theory and proof assistant worlds there are only a handful of us. A typical ratio at a conference for proof assistant research is 1 woman for every 40 men. Anonymous comments scare me because there are (a few, thankfully not many) abusive people in the PL community I am afraid of engaging with. I don't want to accidentally find myself arguing with one of them. I need to know when to exit the conversation. Proof relevant mathematics, higher category theory, lots of topology. Sorry. I don't spend all of time on HackerNews, I sometimes don't get around to responding to things. I am talking to Kevin about this framing so we can figure out how to make it healthier in the future. Some of my comments about Kevin were likewise out of line because I interpreted some of our previous interactions as rooted in a gender-based power dynamic when they were actually just rooted in something Kevin finds difficult and wants to do better at, and that is my honest mistake.

jakear 6y ago

> A set 𝑋 is jaberwocky when for every 𝑥∈𝑋 there exists a bryllyg 𝑈⊆𝑋 and an uffish 𝐾⊆X such that 𝑥∈𝑈 and 𝑈∈𝐾. Anyone know how this relates to Lewis Carrol?

creata 6y ago
Jabberwocky is a poem by Lewis Carroll. https://en.wikipedia.org/wiki/Jabberwocky https://en.wikipedia.org/wiki/Jabberwocky
- schoen 6y ago
  And the idea in the context of the original post is that this is supposed to be a parody of a formal math definition in a paper or textbook (using Jabberwocky vocabulary instead of real math vocabulary).
  - newen 6y ago
    Not that it makes sense anyway. Somehow 𝑈⊆𝑋 and 𝑈∈𝑋.
    - leanuser83 6y ago
      That is exactly the point being made. That you can spot right away that something "doesn't make sense".
    - skissane 6y ago
      No, the point was that 𝑈∈𝑋 is a typo and 𝑈⊆𝑋 is what was intended. Type theory will reject the mistake but set theory will accept it. This is then presented as a reason why mathematicians should prefer type-theory-based proof assistants to set-theory-based ones, since the former will catch these kinds of mistakes while the later won't.
    - bobbylarrybobby 6y ago
      That’s possible. For instance, X = {{}} and U = {}. Or in general, if X_0 = {} and X_{i+1} = {X_0, ..., X_i}, then X_i is both an element and a subset of X_j whenever i < j.

auggierose 6y ago

Here is a plan to improve proof assistants, and it is based on set theory: https://www.practal.com https://www.practal.com

robinzfc 6y ago

The current tittle of the original MathOverflow question is "What makes dependent type theory more suitable than set theory for proof assistants?", I don't know why is it different than here. The actual question makes more sense because the one on HN suggests that proof assistants exclusively formalize mathematics in dependent type theory (rather than set theory) which is not true. In fact, some proof assistants use dependent type theory (LEAN), some use simple type theory (Isabelle/HOL), some use simple type theory to encode untyped set theory (Isabelle/ZF), some implement kind of "soft typing" on top of untyped set theory (Mizar) and some are completely generic and can encode all of the above (Metamath). As for the question why type theory seems to be more popular in formalization of mathematics recently than set theory Jeremy Avigad wrote a rare compelling explanation [1] of why this is the case. I personally prefer the opinion of Lawrence Paulson [2], the original author of Isabelle and its ZF logic (he also implemented a formalization of ZFC set theory in Isabelle/HOL recently). [1] https://cs.nyu.edu/pipermail/fom/2016-January/019441.html https://cs.nyu.edu/pipermail/fom/2016-January/019441.html [2] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html https://cs.nyu.edu/pipermail/fom/2018-June/021032.html

OJFord 6y ago
> The current tittle of the original MathOverflow question is "What makes dependent type theory more suitable than set theory for proof assistants?", I don't know why is it different than here. It's too long for HN, OP presumably reworded to fit. If you have a better suggestion one of the mods might see and change it, I think OP's chance to edit it has passed though.
- edjrage 6y ago
  "Why is dependent type theory more suitable than set theory for proof assistants?” has 80 characters, which seems to be exactly HN's limit.
  - pgustafs 6y ago
    Yep, that would be a better rewording. I missed it in my search for a <80 character title.

octoberfranklin 6y ago

Program extraction. In dependent type theory if you've proved "A implies B" you can extract from that proof a program that takes an argument of type A and always halts, returning a value of type B. Moreover if you prove some property about proofs that A implies B, you've also proved the corresponding proposition about programs. This means your proofs get to deal with programs directly, rather than having to formalize them as something like Turing machines whose tapes are set-theoretic encodings of lists of integers. It's excruciatingly painful to write non-hand-wavy proofs of anything that way. Hand-wavy proofs that can't be machine-checked aren't so bad of course; complexity theory folks have been doing that for decades. If you aren't proving things about programs or homotopy then there really aren't any obvious reasons to prefer dependent type theory. I say this as somebody who loves programming with dependent types. But I'm being honest here, and I wish more people in the mechanized mathematics world would be honest about this.

alisonkisk 6y ago
> there really aren't any obvious reasons to prefer dependent type theory The OP gives a reason, and it's the same reason programs use types. Untyped proofs are usually wrong, like untyped programs.
- octoberfranklin 6y ago
  Er, no. Even Coq proofs are written in an untyped language (Ltac). You've got your levels mixed up.
- GregarianChild 6y ago
  HOL is typed, but not a dependent type theory. HOL is also a classical logic. HOL is essentially Alonzo Church's simply typed lambda-calculus [1] from 1940. Classical, rather than constructive logic tends to give shorter proofs. [1] A. Church, A Formulation of the Simple Theory of Types. https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b...

adrian_b 6y ago

Slightly off-topic, but in any mathematical theory concerning a certain restricted domain and also in any theory attempting to cover the entire mathematics there are many possible choices for the primitive concepts and rules. In most cases it is not possible to have an objective criterion for deciding which is the best choice, so the choice remains based on personal preferences. For example, I could never accept the idea that set theory can be considered to belong to the foundations of mathematics. I have always believed that it is more convenient to view the sets not as primitives, but as classes of equivalence of the ordered sequences, which in turn are constructed from ordered pairs, which are a primitive concept. So instead of using set theory as a base, I believe it to be more convenient to start from some primitives that include some of the concepts and operations on which LISP was also based, plus some definitions, which normally are introduced using sets, modified to use ordered sequences instead. All the set theory (and the number theory) can be constructed from these alternative primitive concepts.

devit 6y ago
That doesn't work as written for uncountable sets.
- kmill 6y ago
  That's true, but there's an amusingly odd theorem (downwards Lowenheim-Skolem) that implies that if set theory has a model, it has a countable model. So, in a sense, all sets are countable. I think this just leads you to the next problem, which is that (I think) it would be undecidable normalizing and sorting these sets.