[FOM] Holmes on Con(NF)

[tf at maths.cam.ac.uk]

A conversation i am having with Michael Beeson in Vienna is showing me that 
the firewall around Holmes' proof on his home page is potentially 
misleading. Holmes wants to fend off people who are not technically 
proficient, but the technical proficiency required does not extend to 
mastery of NF. This is a proof *about* NF not *in* NF. To follow Holmes' 
proof you need to understand FM models plus enough model theory to 
understand why the result about type theory that he proves is equivalent to 
the consistency of NF. I am not suggesting that the proof is an easy read, 
but at least it does not require kabbalistic knowledge or access to any 
occult forces. Worth a try.