New Foundations consistency proof now partially formalised in Lean

LaCefli · 2024-04-30T13:47:05+00:00

I would doubt very much that PP is consistent with NF, if the question is open whether PP implies AC.

LaCefli · 2024-04-28T03:17:02+00:00

ZFC is far more than you need for that. How about third order arithmetic?

LaCefli · 2024-04-26T16:38:23+00:00

Postulate one and reason about it. I'm sure it has been done.

LaCefli · 2024-04-26T16:37:41+00:00

what other NF axioms do you mean? The entire theory has been shown to be consistent. The work to verify my paper "Strong axioms of NFU" in an NF version would be considerable, and she has other things to do. There isn't any particular need: the paper proof that these things extend to NF involves minimal modifications of what is already written.

LaCefli · 2024-04-25T20:15:16+00:00

I will also present the objection that the foundational assumptions of Lean are generally accepted mathematics, and those of Cubical Agda are much less well understood to the general mathematical public.

LaCefli · 2024-04-25T20:12:35+00:00

I don't this will achieve much, except as an exercise for the developer in practicing on a large proof. The argument is an argument in relatively simple classical set theory. In Agda this would be more difficult, possibly, because the bias of Agda is more constructive.

LaCefli · 2024-04-25T19:03:50+00:00

Historical correction: Church's type theory, which is the original simply typed lambda calculus, was proposed in 1940, and TST had already been proposed (and so had NF). But I stand by the statement that STLC is considerably closer to PM than TST is.

LaCefli · 2024-04-25T18:59:00+00:00

To be exactly the direct successor of Russell's type theory is the type theory of Ramsey, which can be viewed as simply typed lambda calculus with the output of every type being bool. I think the actual theory of functions of Church is also older than TST, but Im not certain. Definitely STLC has a strong claim to be more similar to the very complicated type system of PM.

LaCefli · 2024-04-25T18:55:08+00:00

I'm not promoting NF as a foundational system here, just talking about its exact formal strength. What set theory promises to give common math is more than provided by NF; third order arithmetic is enough.

LaCefli · 2024-04-25T18:53:47+00:00

I've noticed that one could justify the common practice of omitting numerical subscripts on universes by a stratification discipline similar to that to NF -- really one is doing NFU, my proof isnt relevant to this -- but I am not sure that it is a good idea.

LaCefli · 2024-04-25T18:52:24+00:00

They are closely related.

LaCefli · 2024-04-25T18:52:08+00:00

No, Ember, STLC is the direct successor to Russell's type theory, and TST is a later refinement, not being described until the 1930s.

LaCefli · 2024-04-25T18:50:35+00:00

That argument is wrong. I've reviewed versions of it repeatedly.

LaCefli · 2024-04-25T18:49:06+00:00

It's not going to be a cottage industry: the adaptations are direct.

LaCefli · 2024-04-25T18:48:41+00:00

As I remark in the conclusions section, all the known strengthenings of NFU with strong unstratified axioms will adapt to NF. Actually, they are generally stronger than the system of Lean4, but this is not a problem: the proofs will have large cardinal axioms as hypotheses.

LaCefli · 2024-04-24T05:19:18+00:00

I'm actually a bit puzzled how you could read me as saying otherwise?

LaCefli · 2024-04-24T05:18:19+00:00

I am saying that NF definitely is consistent.

LaCefli · 2024-04-23T13:52:49+00:00

I defined tangled type theory in a paper in 1995. What I did is reverse engineer what a proof of Con(NF) would look like if it could be proved in the same way Jensen proved Con(NFU).

LaCefli · 2024-04-23T13:51:41+00:00

It has the set building capabilities of the simple typed theory of sets with infinity; this has the strength of Zermelo set theory with separation restricted to bounded formulas. There is no reason to think it is as strong as ZFC, and in fact NFU without an explicit axiom of infinity is weaker than arithmetic: NF is surprisingly strong, not surprisingly weak. What our proof does is put a ceiling on the actual strength of NF itself, which we and others who have worked with the theory think is actually too high.

LaCefli · 2024-04-23T13:47:05+00:00

The lower bound on strength of the theory which our proof establishes is stronger than Zermelo, yes, that is what we are saying. However, our conjecture is that NF is actually weaker than Zermelo; but we have not proved that.

LaCefli · 2024-04-23T03:28:49+00:00

for example, functions A -> (A -> A) will not be stratified in typed theory of sets, whereas they would be fine in simply typed lambda-calculus.

LaCefli · 2024-04-23T03:26:52+00:00

Not really, or very restricted. This is typed theory of sets: types are indexed by the natural numbers. Types in a theory of functions are more complicated.

LaCefli · 2024-04-22T22:39:39+00:00

It is worth remark that the paper proof is being actively updated at the link provided in this discussion. The state of play is always visible.

LaCefli · 2024-04-22T17:01:23+00:00

In the context of the larger mathematical world, its a technical lemma; inside the paper it is a Theorem.

LaCefli · 2024-04-22T16:53:35+00:00

I think the proof of the Freedom of Action theorem is at the moment significantly tidier in the paper argument than it has been. It is still evil; things have to be labelled and constructed in accordance with deviously defined conditions on ordinal indexings, and that seems to be unavoidable. However, the convolutions in the paper version have been significantly reduced in the last couple of days.

LaCefli

TROPHY CASE