Fwd: added one more theorem

[Martin Davis]

---------- Forwarded message ---------
From: Michael Beeson <profbeeson at gmail.com>
Date: Tue, Sep 14, 2021 at 12:49 AM
Subject: added one more theorem
To:



I've added one more section to my paper on intuitionistic NF.
Section 20 contains a proof that the Church counting axiom
is equivalent to the Rosser counting axiom.   That is a new
result even with classical logic.  (Both those axioms are defined there.)

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

Now I'm  *really * done with this "pandemic project".   Thanks
to Thomas Forster for believing that it should be possible to
prove this and stimulating me to do so.   By the way, I've
checked the proof in Lean, like all the other proofs in the paper.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210914/7eab5df8/attachment.html>