Also we do have a model of these axioms, to be clear, since it was formalized in Isabelle, routing through checking for the existence of a model. Here if you want to read it yourself :) https://www.isa-afp.org/entries/Types_Tableaus_and_Goedels_God.html
EDIT: I think the version I gave is kind of like a mix of Anderson’s or Fitting’s, not sure, I made the change myself. But they’re pretty similar anyway.
Also we do have a model of these axioms, to be clear, since it was formalized in Isabelle, routing through checking for the existence of a model. Here if you want to read it yourself :) https://www.isa-afp.org/entries/Types_Tableaus_and_Goedels_God.html
EDIT: I think the version I gave is kind of like a mix of Anderson’s or Fitting’s, not sure, I made the change myself. But they’re pretty similar anyway.