Comment by dwheeler | Hacker News Reader

Comment by dwheeler | Hacker News Reader

Parent Full thread

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

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.

> 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

How is that not a problem? The type of a set needs to be higher than its elements to prevent the construction of a set containing itself. If a tuple is the same type as an elements, then can't you construct a tuple that contains itself as its first element, i.e. "x.0 = x" is a stratified formula so x exists.

How is that a problem that a set contains itself? It's allowed in NF.

The Quine pair works in ordinary set theory (Zermelo or ZFC); it has a mildly baroque definition but there is no problem with it. Look at the machinery and you will see why a pair (as opposed to a general set) doesnt strictly speaking need to be of higher type than its components.

> 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

No, Lean is not suitable for axiomatic investigations, it comes with too much baggage from "classical foundations". As Randall said above, Lean is axiomatically much stronger than NF, and that's even with "no axioms"! You can use Lean to prove things about axiom systems, but you have to model the axiom system explicitly as a "deep embedding" with syntax and a typing judgment. For metatheory work like the one reported on here this is exactly what you want, but if you want to actually work in the theory then it's an extra layer of indirection which makes things a lot more cumbersome compared to using Lean's own logic.

Metamath is much more configurable in this regard, you just directly specify the axiom system you want to work in and there is no special status given to first order logic or anything like that.

Reply on news.ycombinator.com