(1) Some typical inclompleteness proofs use a kind of fixed point argument - for certain $\Phi$ you find a $\varphi$ with $\Phi(\mathrm{code}(\varphi))\leftrightarrow\varphi$.
(2) Some independence proofs seem to use something entirely different - you prove that given any model $\mathfrak M$ of (a theory $T$) + (some $\varphi$), you can construct from it a model $\mathfrak M_{\neg\varphi}$ of $T$ + $\neg\varphi$.
Still, these are obviously closely related: if I am not totally confused, the $\varphi$ in (2) plays the role (or even is an instance) of the $\varphi$ in (1): it provides a $\varphi$ which is non-provable (since this is the meaning of $\Phi$ in (1) and since you have a model of $\neg\varphi$ in (2)) and non-refutable (since it comes out true by a self-reference argument in (1) and since you have a model of $\varphi$ in (2)), which you seek in (1), don't you?
I thus wonder whether constructions like, say, Poincaré or Klein models of the non-Euclidean plane (a typical (2)) can be viewed as instances of application of some kind of fixed point theorems as in (1)?
Vice versa - can, say, construction of a Gödel sentence be viewed as construction, from a model, of some countermodel?
To put it still differently: in (1) we have a formula with the property that from its provability contradiction can be deduced; in (2) - a formula with the property that each of its models contains a tool to construct its countermodel. What kind of relationship exists between these two properties of formulæ?
