Let L(0) be Zermelo set theory (or the axioms for an elementary topos).
For each n, let L(n+1) be L(n) plus as much of the axiom-scheme of replacement as is needed to justify the gluing construction that shows that
L(n+1) |- ``L(n) is consistent.''
Now let L(infinity) be the union of L(n) over n:N.
If L(infinity) |- false then L(n) |- false for some n.
But L(infinity) |- ``L(n) is consistent,''
so L(infinity) proves its OWN consistency, contradicting Godel's theorem.
However, L(infinity) has a standard non-trivial interpretation in Zermelo--Fraenkel set theory, which is therefore inconsistent.
i think there is a gap is in the step L(infinity) |- "L(n) is consistent" so L(infinity) proves its OWN consistency formalized in a suitable category of theories and interpretations, paul's construction, if i understand it correctly, refers to the colimit of the tower L(0) --> FL(0) --> FFL(0) -->... where FX = X + replacement_X, so that FX |- "X is consistent". IF the colimit of this tower, paul's L(infinity), were a fixpoint of F, THEN it would indeed prove its own consistency. but it doesn't seem to be a fixpoint: the restrictions of the replacement to L(0), FL(0) etc. do not imply the replacement for L(infinity). btw, i bought paul's book and warmly recommend it. -- dusko