Fwd: Some results about NF set theory

[Martin Davis]

---------- Forwarded message ---------
From: Michael Beeson <profbeeson at gmail.com>
Date: Mon, Aug 2, 2021 at 7:31 AM
Subject: Some results about NF set theory

Dear friends and colleagues,

I've completed my pandemic project about the Church numerals in
Quine's NF set theory,  and I've ensured that the proofs are correct
by formalizing them in the Lean proof-checker.  Therefore I can
state with high confidence that there are no errors in the papers
linked below (there could be typos, since the correspondence to the
formal proof is manually managed).

I proved that the set N of Church numbers is finite,  using intuitionistic
NF set theory plus the "Church counting axiom"  (iterating Church successor
n times from 0  results in n).   That is a new result even with classical
logic.
I could not prove it without the Church counting axiom,  so the original
goal of
proving infinity in intuitionistic NF is still an open question.

There are two papers, linked below.

The first link contains the result about the Church
numbers;  it relies on the second for basic results about finite sets.  The
second link contains those results,  as well as constructive versions of
the theories of finite cardinals and arithmetic and T  from Rosser's book
and
Specker's paper.

http://www.michaelbeeson.com/research/papers/nf.pdf

http://www.michaelbeeson.com/research/papers/inf-basics.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210802/5cd2d9f3/attachment.html>