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.
This is a pdf file. The paper in question summarizes my results on Gleason's theorem in non-separable Hilbert spaces. There are no proofs.
This writes up an unpublished proof of mine concerning ultrafilters. I'm not sure whether the result in question is due to me. The write up is at the request of someone who wanted a citation for the proof.