4 ms·

Can someone give a rough description of what is special, or novel, in the "New Foundations" set theory formulation, relative to other formulations? Or at least,

Can someone give a rough description of what is special, or novel, in the "New Foundations" set theory formulation, relative to other formulations? Or at least, link to a description readable by, say, a math undergrad student or an engineering professional?

thefringthing 3y ago
One "nice" thing about NF is that it has only two axioms/axiom schemes: 1) sets with the same members are the same, and 2) any stratifiable property corresponds to a set off all the things which have that property. And the definition of "stratifiable" isn't very complicated. ZF, by contrast, has eight rather ad hoc axioms/axiom schemes.
Mathnerd314 3y ago
I was just editing the Wikipedia article, it should be more readable now: https://en.wikipedia.org/wiki/New_Foundations https://en.wikipedia.org/wiki/New_Foundations I think the main thing is the existence of the universal set. For my use case, the type system of a programming language, such a universal set is very useful. There are various hacks used in existing systems like cumulative universes or type-in-type which are not as satisfying - instead, I can just check that the type signature is stratified and then forget about types having numerical levels.
- randallholmes 3y ago
  It's not magic: the universe of NF and other "big" objects in this system must be handled with extreme care.
  - randallholmes 3y ago
    to the original poster, the universe is a boolean algebra in NF: sets have complements, there is a universe. The number three is the set of all sets with three elements (this is not a circular definition; it is Frege's definition from way back); in general, a cardinal number is an equivalence class under equinumerousness, defined in the usual set theoretic way, and an ordinal number is an equivalence class of well-orderings under similarity. When you look at objects which lead to paradox (the cardinality of the universe, the order type of the natural well-ordering on the ordinals) then you discover the violence inherent in the system. Very strange things happen, which are counterintuitive. None of this depends on my proof to work: these are all features of NFU (New Foundations with urelements) which has been known to be consistent since 1969, and one can explore what is happening by looking at its known models, which are far simpler than what I construct.
    - klyrs 3y ago
      > The number three is the set of all sets with three elements I can't make up my mind if this is extremely elegant, or mindbogglingly horrendous; awesome or awful. I lean towards elegant, because the mindboggle caused by traditional set theory.
      - randallholmes 2y ago
        I think the Frege definition of the natural numbers is philosophically the correct one. This is a point in favor of foundations in NFU. I also think that Zermelo-style foundations are pragmatically better, so sadly I must let go of the first preference :-)
    - einpoklum 3y ago
      So, is the article/project concerned with "just NF", or "NF with urelements"? Also, now I have to go learn about urelements too :-(
      - randallholmes 3y ago
        The project is concerned with NF itself; the status of NFU was settled by Jensen in 1969 (it can be shown to be consistent fairly easily). Showing consistency of NF is difficult. There is nothing mysterious about urelements: an urelement is simply an object which is not a set. To allow urelements is to weaken extensionality to say, objects with the same elements which are sets are equal; objects which are not sets have no elements (but may be distinct from each other and the empty set).
      - randallholmes 3y ago
        urelements aren't mysterious at all. They are simply things which are not sets. If you allow urelements, you weaken extensionality, to say that sets with the same elements are equal, while non-sets have no elements, and may be distinct from each other and the empty set. Allowing urelements can be viewed as a return to common sense :-)
        3y ago
  - randallholmes 3y ago
    to clarify, when you look at objects that lead to paradox in naive set theory; they do not lead to paradox in NF or NFU; they exist but have unexpected properties.
    - randallholmes 3y ago
      at some objects. The Russell class cannot be a set in any set theory, that is logic. The cardinality of the universe and the order type of the ordinals do exist in NF(U) and have rather unexpected properties.
  - Mathnerd314 3y ago
    While you're around, I have a question: In TST, the restriction for x^m in y^n is that n = m+1, i.e. the level must increment by 1. In TTT, the restriction is instead that m < n, there is no requirement that it only be 1. Now, in NF, the restriction for set membership in stratified formulas is also +1. Is it possible to relax this to a "Tangled NF" where the set membership restriction is only that m < n? This would resolve issues such as how many levels it takes to construct an ordered pair.
    - randallholmes 3y ago
      Jensen's consistency proof for NFU can be read as relying on the consistency of TTTU, which is actually very easy to show.
    - randallholmes 3y ago
      No, the Tangled NF you suggest would be inconsistent.
      - Mathnerd314 3y ago
        Well, there is that proof that stratified comprehension works, https://randall-holmes.github.io/head.pdf#page=41 https://randall-holmes.github.io/head.pdf#page=41, based on encoding x^(n-1) ∈ y^n as ({x}^n,y^n) ∈ [∈], where the existence of [∈] = { ({x}, y) | x ∈ y } (or its containing relation [⊆]) is an axiom. I don't see why you can't similarly encode x ∈ y as ({{x}},y) ∈ [∈2] where [∈2] = {({{x}},y) | x ∈ y }. From what I can tell, the existence of [∈2] is required by relative product, [∈2] = {(x'', y) | for some x', x'' [∈] x' and x' [∈] y }. Similarly [∈n] exist for all n>0. Then an occurrence of x ∈ y in which x has type n − k and y has type n can be replaced by ι^(N−(n-k))(x) [∈k]^ι^(N−n) ι^(N−n)(y) and the formula can be stratified. So it should just be equivalent to normal NF.
        randallholmes 3y ago
        Work out the details. It won't produce what you describe above.
- dwheeler 3y ago
  I agree, a "cool" think about NF is the universal set. Another way to be introduced to New Foundations, along with how one can use it, is the Metamath database for New Foundations: https://us.metamath.org/nfeuni/mmnf.html https://us.metamath.org/nfeuni/mmnf.html Metamath is a proof system, but unlike most alternative systems like Lean, it doesn't have a built-in set of axioms - you need to declare your axioms, and then you can prove theorems (using only previous axioms and proven theorems). So you can declare the axioms of New Foundations, and then use them to prove other things. One thing you immediately discover when you try to use New Foundations is that "the usual definition of the ordered pair, first proposed by Kuratowski in 1921 and used in the regular Metamath Proof Explorer, has a serious drawback for NF and related theories that use stratification. The Kuratowski ordered pair is defined as << x , y >> = { { x } , { x , y } }. This leads to the ordered pair having a type two greater than its arguments. For example, z in << << x , y >> , z >> would have a different type than x and y, which makes multi-argument functions extremely awkward to work with. Operations such as "1st" and complex "+" would not form sets in NF with the Kuratowski ordered pairs. In contrast, the Quine definition of ordered pairs, defined in definition df-op, is type level. That is, <. x , y >. has the same type as x and y, which means that the same holds of <. <. x , y >. , z >. This means that "1st" is a set with the Quine definition, as is complex "+". The Kuratowski ordered pair is defined (as df-opk), because it is a simple definition that can be used by the set construction axioms that follow it, but for typical uses the Quine definition of ordered pairs df-op is used instead." One eye-popping result is that the Axiom of Choice can be disproven in NF. See that site (or other pages about NF) for details.
  - seanhunter 3y ago
    > Metamath is a proof system, but unlike most alternative systems like Lean, it doesn't have a built-in set of axioms - you need to declare your axioms, and then you can prove theorems (using only previous axioms and proven theorems). So you can declare the axioms of New Foundations, and then use them to prove other things. I've only used lean a little bit but I'm pretty sure you can start lean with a blank slate, declare whatever you want and then build up from there. In fact the Natural Number Game[1] is basically this, you develop the Peano axioms etc and prove everything about the natural numbers from scratch without using the standard library (which obviously would have all that built in). [1] https://adam.math.hhu.de/#/g/leanprover-community/NNG4 https://adam.math.hhu.de/#/g/leanprover-community/NNG4
Smaug123 3y ago
The thing I find really aesthetically pleasing about NF is how it adjusts the axiom of subset selection so that "the set of all sets" doesn't cause Russell's paradox. Basically it requires that the predicates you use to select subsets must obey a certain very lightweight type system. "x is not a member of itself" is not a well-typed question under any reasonable type system, and in particular it doesn't satisfy NF's "stratifiability" requirement, so you can't use it to construct the Russell's-paradox set of all sets which do not contain themselves.
- juped 3y ago
  You just move the sorts around, you don't get rid of having to have sorts. I guess a rug with dirt swept under it is more aesthetically pleasing than a rug with dirt on top of it?
  - epgui 3y ago
    There is no notion of types in naive set theory.
    - juped 3y ago
      No one said anything about either types or naive set theory.
- psychoslave 3y ago
  That sounds extremely underwhelming to my mind. Like having a programming language sold as free of any awful metaprogramming constructions (and induced headaches) through guarantees that no metaprogramming at all can be done in it. A language that forbids to talk about its own grammatical structures is doomed to see its users abandon or extend it when they will inevitably deal with a situation where exchanging about the communication tool at hand is required to appropriately deal with its possibilities, expectable behaviors and limits.
  - epgui 3y ago
    Your comment doesn't make any sense. Also: > A language that forbids to talk about its own grammatical structures That's just not the case, and it's not what is being claimed here.

thefringthing 3y ago

One "nice" thing about NF is that it has only two axioms/axiom schemes: 1) sets with the same members are the same, and 2) any stratifiable property corresponds to a set off all the things which have that property. And the definition of "stratifiable" isn't very complicated. ZF, by contrast, has eight rather ad hoc axioms/axiom schemes.

Mathnerd314 3y ago

I was just editing the Wikipedia article, it should be more readable now: https://en.wikipedia.org/wiki/New_Foundations https://en.wikipedia.org/wiki/New_Foundations I think the main thing is the existence of the universal set. For my use case, the type system of a programming language, such a universal set is very useful. There are various hacks used in existing systems like cumulative universes or type-in-type which are not as satisfying - instead, I can just check that the type signature is stratified and then forget about types having numerical levels.

randallholmes 3y ago
It's not magic: the universe of NF and other "big" objects in this system must be handled with extreme care.
- randallholmes 3y ago
  to the original poster, the universe is a boolean algebra in NF: sets have complements, there is a universe. The number three is the set of all sets with three elements (this is not a circular definition; it is Frege's definition from way back); in general, a cardinal number is an equivalence class under equinumerousness, defined in the usual set theoretic way, and an ordinal number is an equivalence class of well-orderings under similarity. When you look at objects which lead to paradox (the cardinality of the universe, the order type of the natural well-ordering on the ordinals) then you discover the violence inherent in the system. Very strange things happen, which are counterintuitive. None of this depends on my proof to work: these are all features of NFU (New Foundations with urelements) which has been known to be consistent since 1969, and one can explore what is happening by looking at its known models, which are far simpler than what I construct.
  - klyrs 3y ago
    > The number three is the set of all sets with three elements I can't make up my mind if this is extremely elegant, or mindbogglingly horrendous; awesome or awful. I lean towards elegant, because the mindboggle caused by traditional set theory.
    - randallholmes 2y ago
      I think the Frege definition of the natural numbers is philosophically the correct one. This is a point in favor of foundations in NFU. I also think that Zermelo-style foundations are pragmatically better, so sadly I must let go of the first preference :-)
  - einpoklum 3y ago
    So, is the article/project concerned with "just NF", or "NF with urelements"? Also, now I have to go learn about urelements too :-(
    - randallholmes 3y ago
      The project is concerned with NF itself; the status of NFU was settled by Jensen in 1969 (it can be shown to be consistent fairly easily). Showing consistency of NF is difficult. There is nothing mysterious about urelements: an urelement is simply an object which is not a set. To allow urelements is to weaken extensionality to say, objects with the same elements which are sets are equal; objects which are not sets have no elements (but may be distinct from each other and the empty set).
    - randallholmes 3y ago
      urelements aren't mysterious at all. They are simply things which are not sets. If you allow urelements, you weaken extensionality, to say that sets with the same elements are equal, while non-sets have no elements, and may be distinct from each other and the empty set. Allowing urelements can be viewed as a return to common sense :-)
      - 3y ago
- randallholmes 3y ago
  to clarify, when you look at objects that lead to paradox in naive set theory; they do not lead to paradox in NF or NFU; they exist but have unexpected properties.
  - randallholmes 3y ago
    at some objects. The Russell class cannot be a set in any set theory, that is logic. The cardinality of the universe and the order type of the ordinals do exist in NF(U) and have rather unexpected properties.
- Mathnerd314 3y ago
  While you're around, I have a question: In TST, the restriction for x^m in y^n is that n = m+1, i.e. the level must increment by 1. In TTT, the restriction is instead that m < n, there is no requirement that it only be 1. Now, in NF, the restriction for set membership in stratified formulas is also +1. Is it possible to relax this to a "Tangled NF" where the set membership restriction is only that m < n? This would resolve issues such as how many levels it takes to construct an ordered pair.
  - randallholmes 3y ago
    Jensen's consistency proof for NFU can be read as relying on the consistency of TTTU, which is actually very easy to show.
  - randallholmes 3y ago
    No, the Tangled NF you suggest would be inconsistent.
    - Mathnerd314 3y ago
      Well, there is that proof that stratified comprehension works, https://randall-holmes.github.io/head.pdf#page=41 https://randall-holmes.github.io/head.pdf#page=41, based on encoding x^(n-1) ∈ y^n as ({x}^n,y^n) ∈ [∈], where the existence of [∈] = { ({x}, y) | x ∈ y } (or its containing relation [⊆]) is an axiom. I don't see why you can't similarly encode x ∈ y as ({{x}},y) ∈ [∈2] where [∈2] = {({{x}},y) | x ∈ y }. From what I can tell, the existence of [∈2] is required by relative product, [∈2] = {(x'', y) | for some x', x'' [∈] x' and x' [∈] y }. Similarly [∈n] exist for all n>0. Then an occurrence of x ∈ y in which x has type n − k and y has type n can be replaced by ι^(N−(n-k))(x) [∈k]^ι^(N−n) ι^(N−n)(y) and the formula can be stratified. So it should just be equivalent to normal NF.
      - randallholmes 3y ago
        Work out the details. It won't produce what you describe above.
dwheeler 3y ago
I agree, a "cool" think about NF is the universal set. Another way to be introduced to New Foundations, along with how one can use it, is the Metamath database for New Foundations: https://us.metamath.org/nfeuni/mmnf.html https://us.metamath.org/nfeuni/mmnf.html Metamath is a proof system, but unlike most alternative systems like Lean, it doesn't have a built-in set of axioms - you need to declare your axioms, and then you can prove theorems (using only previous axioms and proven theorems). So you can declare the axioms of New Foundations, and then use them to prove other things. One thing you immediately discover when you try to use New Foundations is that "the usual definition of the ordered pair, first proposed by Kuratowski in 1921 and used in the regular Metamath Proof Explorer, has a serious drawback for NF and related theories that use stratification. The Kuratowski ordered pair is defined as << x , y >> = { { x } , { x , y } }. This leads to the ordered pair having a type two greater than its arguments. For example, z in << << x , y >> , z >> would have a different type than x and y, which makes multi-argument functions extremely awkward to work with. Operations such as "1st" and complex "+" would not form sets in NF with the Kuratowski ordered pairs. In contrast, the Quine definition of ordered pairs, defined in definition df-op, is type level. That is, <. x , y >. has the same type as x and y, which means that the same holds of <. <. x , y >. , z >. This means that "1st" is a set with the Quine definition, as is complex "+". The Kuratowski ordered pair is defined (as df-opk), because it is a simple definition that can be used by the set construction axioms that follow it, but for typical uses the Quine definition of ordered pairs df-op is used instead." One eye-popping result is that the Axiom of Choice can be disproven in NF. See that site (or other pages about NF) for details.
- seanhunter 3y ago
  > Metamath is a proof system, but unlike most alternative systems like Lean, it doesn't have a built-in set of axioms - you need to declare your axioms, and then you can prove theorems (using only previous axioms and proven theorems). So you can declare the axioms of New Foundations, and then use them to prove other things. I've only used lean a little bit but I'm pretty sure you can start lean with a blank slate, declare whatever you want and then build up from there. In fact the Natural Number Game[1] is basically this, you develop the Peano axioms etc and prove everything about the natural numbers from scratch without using the standard library (which obviously would have all that built in). [1] https://adam.math.hhu.de/#/g/leanprover-community/NNG4 https://adam.math.hhu.de/#/g/leanprover-community/NNG4

Smaug123 3y ago

The thing I find really aesthetically pleasing about NF is how it adjusts the axiom of subset selection so that "the set of all sets" doesn't cause Russell's paradox. Basically it requires that the predicates you use to select subsets must obey a certain very lightweight type system. "x is not a member of itself" is not a well-typed question under any reasonable type system, and in particular it doesn't satisfy NF's "stratifiability" requirement, so you can't use it to construct the Russell's-paradox set of all sets which do not contain themselves.

juped 3y ago
You just move the sorts around, you don't get rid of having to have sorts. I guess a rug with dirt swept under it is more aesthetically pleasing than a rug with dirt on top of it?
- epgui 3y ago
  There is no notion of types in naive set theory.
  - juped 3y ago
    No one said anything about either types or naive set theory.
psychoslave 3y ago
That sounds extremely underwhelming to my mind. Like having a programming language sold as free of any awful metaprogramming constructions (and induced headaches) through guarantees that no metaprogramming at all can be done in it. A language that forbids to talk about its own grammatical structures is doomed to see its users abandon or extend it when they will inevitably deal with a situation where exchanging about the communication tool at hand is required to appropriately deal with its possibilities, expectable behaviors and limits.
- epgui 3y ago
  Your comment doesn't make any sense. Also: > A language that forbids to talk about its own grammatical structures That's just not the case, and it's not what is being claimed here.