This is a pdf file. The system NFUB is a variant of Quine's New Foundations introduced by Randall Holmes. We show that its consistency strength is precisely that of ZFC- [ZFC minus the power set axiom] plus the assertion that there is a weakly compact cardinal.

The current version is a preliminary draft. We hope to replace it by a more polished version "real soon now".

This link leads to another web page which contains a series of files that present my computation of the consistency strength of NFU_star, This system is another varient of NFU proposed by Randall Holmes. We show that the consistency strength of this system is precisely that of ZC plus Sigma_2 Replacement.

A version of the Barwise compactness theorem plays an essential role in the proof.

This is a proof in the formal system Mizar of the fact that one of the usual ways of defining a bijection between the non-negative integers and the set of pairs of non-negative integers does indeed work.

My reason for doing this was that Raph Levien did a similar treatment of the same topic in the system Metamath and I wanted to have this available for a comparison of the two systems.