Fixpoints of models constructions

Sergei Tupailo


We start with Specker’s result that NF is equiconsistent with SCA + Ext + Amb (SCA is the Simple (intensional) Type Theory). First, there is a model M0 of SCA (simple). We define 2 operations A1 and A2 acting on models of SCA (A2 will be parametrized by a finite list of LTT-statements, but this is enough by compactness):


The Axiom of Choice of ZFC is used for defining the operations A1 and A2.
To conclude, NF is consistent assuming that such a fixpoint always exists.

Full Text:



  • There are currently no refbacks.