At the meeting here in Konstanz, Giorgo Venturi and I considered the sentence $\sigma$, which asserts its own non-forceability by nontrivial forcing. That is, $\sigma$ asserts that there is no nontrivial forcing notion forcing $\sigma$. $$\sigma\quad\iff\quad \neg\exists\mathbb{B}\ \Vdash_{\mathbb{B}}\sigma.$$ The sentence $\sigma$ would be a fixed-point of the predicate for not being nontrivially forceable.
In any model of set theory $V$ in which $\sigma$ is true, then in light of what it asserts, it would not be forceable by nontrivial forcing, and so it would be false in all nontrivial forcing extensions of that model $V[G]$. And in any model $W$ where it is false, then because of what it asserts, it would be nontrivially forceable, and so it would be true in some forcing extension of that model $W[G]$.
But this is a contradiction! It cannot ever be true, since if it were true in $V$, it would have to be false in all extensions $V[G]$, and therefore true in some subsequent extension $V[G][H]$. But that model is a forcing extension of $V$, contradicting the claim that it is false in all such extensions.
So it must always be false, but this can’t happen, since then in any given model, in light of what it asserts, it would have to be true. So it cannot ever be true or false.
Conclusion: there is no such sentence σ that asserts its own nontrivial forceability. This is no fixed-point for not being nontrivially forceable.
But doesn’t this contradict the fixed-point lemma? After all, the fixed-point lemma shows that we can produce fixed points for any expressible assertion.
The resolution of the conundrum is that although for any given assertion $\varphi$, we can express “$\varphi$ is forceable”, we cannot express “x is the Gödel code of a forceable sentence”, for reasons similar to those for Tarski’s theorem on the nondefinability of truth.
Therefore, we are not actually in a situation to apply the fixed-point lemma. And ultimately the argument shows that there can be no sentence $\sigma$ that asserts “$\sigma$ is not forceable by nontrivial forcing”.
Ultimately, I find the logic of this sentence $\sigma$, asserting its own non-nontrivial forceability, to be a set-theoretic forcing analogue of the Yablo paradox. The sentence holds in a model of set theory whenever it fails in all subsequent models obtained by forcing, and that relation is exactly what arises in the Yablo paradox.
