Benes' partial model of NF: an old result revisited

A paper by Beneˇs, published in 1954, was an attempt to prove the consistency of NF (Quine’s set theory “New Foundations”) via a partial model of Hailperin’s finite axiomatization of NF. Here, I offer an analysis of Beneˇs’ proof in a De Giorgi-style setting for set theory. This approach leads to an abstract version of Beneˇs’ theorem that emphasizes the monotone and invariant content of the axioms proved to be consistent, in a sense of monotony and invariance that this paper intends to state rigorously and to help clarify. Moreover, some tentative speculation will be made about possible developments of the topic in the following two directions: (1) which set theories can be proved to be consistent via Beneˇs-like constructions? and (2) how can we elaborate on Beneˇs’ model to get a consistency proof for full NF?