This is rather random, but I really appreciate the work made by the moderators when explaining their reasons for curating an article. Keep this up please!
Generalized fixed point theorem:
Suppose that are modal sentences such that is modalized in (possibly containing sentence letters other than ).
Then there exists in which no appears such that .
We will prove it by induction.
For the base step, we know by the fixed point theorem that there is such that
Now suppose that for we have such that .
By the second substitution theorem, . Therefore we have that .
If we iterate the replacements, we finally end up with .
Again by the fixed point theorem, there is such that .
But as before, by the second substitution theorem, .
Let stand for , and by combining the previous lines we find that .
By Goldfarb's lemma, we do not need to check the other direction, so and the proof is finished
An immediate consequence of the theorem is that for those fixed points and every , .
Indeed, since is closed under substitution, we can make the change for in the theorem to get that .
Since the righthand side is trivially a theorem of , we get the desired result.
One remark: the proof is wholly constructive. You can iterate the construction of fixed point following the procedure implied by the construction of the to compute fixed points.
Uniqueness of arithmetic fixed points:
Notation:
Let be a fixed point on of ; that is, .
Suppose is such that . Then by the first substitution theorem, for every formula . If , then , from which it follows that .
Conversely, if and are fixed points, then , so since is closed under substitution, . Since , it follows that .
(Taken from The Logic of Provability, by G. Boolos.)
I appreciate that in the example it just so happens that the person assigning a lower probability ends up assigning a higher probability that the other person at the beginning, because it is not intuitive that this can happen but actually very reasonable. Good post!