Jaime Sevilla Molina

Toward a New Technical Explanation of Technical Explanation

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!

A primer on provability logic

**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.

A primer on provability logic

**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!