FW: Some results about NF set theory
Kreinovich, Vladik
FYI
---------- Forwarded message ---------
From: Michael Beeson <profb...@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 infinite, 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.