RE: added one more theorem

[Kreinovich, Vladik]

FYI

---------- Forwarded message ---------
From: Michael Beeson <profb...@gmail.com>
Date: Tue, Sep 14, 2021 at 12:49 AM

 

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.