Thread for proofs of results claimed above (not limited to stuff not found in Lindström); contributions appreciated. Stuff not in Lindström includes the uniqueness of arithmetic fixed points in PA (found in the modal agents paper), and I think the version of the fixed point theorem with more than one Fi (the latter should be provable by iterated application of the fixed point theorem for a single F).
Suppose that Ai(p1,...,pn) are n modal sentences such that Ai is modalized in pn (possibly containing sentence letters other than pjs).
Then there exists H1,...,Hn in which no pj appears such that GL⊢∧i≤n{⊡(pi↔Ai(p1,...,pn)}↔∧i≤n{⊡(pi↔Hi)}.
We will prove it by induction.
For the base step, we know by the fixed point theorem that there is H such that GL⊢⊡(p1↔Ai(p1,...,pn))↔⊡(p1↔H(p2,...,pn))
Now suppose that for j we have H1,...,Hj such that GL⊢∧i≤j{⊡(pi↔Ai(p1,...,pn)}↔∧i≤j{⊡(pi↔Hi(pj+1,...,pn))}.
By the second substitution theorem, GL⊢⊡(A↔B)→[F(A)↔F(B)]. Therefore we have that GL⊢⊡(pi↔Hi(pj+1,...,pn)→[⊡(pj+1↔Aj+1(p1,...,pn))↔⊡(pj+1↔Aj+1(p1,...,pi−1,Hi(pj+1,...,pn),pi+1,...,pn))].
If we iterate the replacements, we finally end up with GL⊢∧i≤j{⊡(pi↔Ai(p1,...,pn)}→⊡(pj+1↔Aj+1(H1,...,Hj,pj+1,...,pn)).
Again by the fixed point theorem, there is H′j+1 such that GL⊢⊡(pj+1↔Aj+1(H1,...,Hj,pj+1,...,pn))↔⊡[pj+1↔H′j+1(pj+2,...,pn)].
But as before, by the second substitution theorem, GL⊢⊡[pj+1↔H′j+1(pj+2,...,pn)]→[⊡(pi↔Hi(pj+1,...,pn))↔⊡(pi↔Hi(H′j+1,...,pn)).
Let H′i stand for Hi(H′j+1,...,pn), and by combining the previous lines we find that GL⊢∧i≤j+1{⊡(pi↔Ai(p1,...,pn)}→∧i≤j+1{⊡(pi↔H′i(pj+2,...,pn))}.
By Goldfarb’s lemma, we do not need to check the other direction, so GL⊢∧i≤j+1{⊡(pi↔Ai(p1,...,pn)}↔∧i≤j+1{⊡(pi↔H′i(pj+2,...,pn))} and the proof is finished □
An immediate consequence of the theorem is that for those fixed points Hi and every Ai, GL⊢Hi↔Ai(H1,...,Hn).
Indeed, since GL is closed under substitution, we can make the change pi for Hi in the theorem to get that GL⊢∧i≤n{⊡(Hi↔Ai(H1,...,Hn)}↔∧i≤n{⊡(Hi↔Hi)}.
Since the righthand side is trivially a theorem of GL, 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 H′i to compute fixed points.
Let H be a fixed point on p of ϕ(p); that is, GL⊢⊡(p↔ϕ(p))↔(p↔H).
Suppose I is such that GL⊢H↔I. Then by the first substitution theorem, GL⊢F(I)↔F(H) for every formula F(q). If F(q)=⊡(p↔q), then GL⊢⊡(p↔H)↔⊡(p↔I), from which it follows that GL⊢⊡(p↔ϕ(p))↔(p↔I).
Conversely, if H and I are fixed points, then GL⊢⊡(p↔H)↔⊡(p↔I), so since GL is closed under substitution, GL⊢⊡(H↔H)↔⊡(H↔I). Since GL⊢⊡(H↔H), it follows that GL⊢(H↔I).
(Taken from The Logic of Provability, by G. Boolos.)
Thread for proofs of results claimed above (not limited to stuff not found in Lindström); contributions appreciated. Stuff not in Lindström includes the uniqueness of arithmetic fixed points in PA (found in the modal agents paper), and I think the version of the fixed point theorem with more than one Fi (the latter should be provable by iterated application of the fixed point theorem for a single F).
Generalized fixed point theorem:
Suppose that Ai(p1,...,pn) are n modal sentences such that Ai is modalized in pn (possibly containing sentence letters other than pjs).
Then there exists H1,...,Hn in which no pj appears such that GL⊢∧i≤n{⊡(pi↔Ai(p1,...,pn)}↔∧i≤n{⊡(pi↔Hi)}.
We will prove it by induction.
For the base step, we know by the fixed point theorem that there is H such that GL⊢⊡(p1↔Ai(p1,...,pn))↔⊡(p1↔H(p2,...,pn))
Now suppose that for j we have H1,...,Hj such that GL⊢∧i≤j{⊡(pi↔Ai(p1,...,pn)}↔∧i≤j{⊡(pi↔Hi(pj+1,...,pn))}.
By the second substitution theorem, GL⊢⊡(A↔B)→[F(A)↔F(B)]. Therefore we have that GL⊢⊡(pi↔Hi(pj+1,...,pn)→[⊡(pj+1↔Aj+1(p1,...,pn))↔⊡(pj+1↔Aj+1(p1,...,pi−1,Hi(pj+1,...,pn),pi+1,...,pn))].
If we iterate the replacements, we finally end up with GL⊢∧i≤j{⊡(pi↔Ai(p1,...,pn)}→⊡(pj+1↔Aj+1(H1,...,Hj,pj+1,...,pn)).
Again by the fixed point theorem, there is H′j+1 such that GL⊢⊡(pj+1↔Aj+1(H1,...,Hj,pj+1,...,pn))↔⊡[pj+1↔H′j+1(pj+2,...,pn)].
But as before, by the second substitution theorem, GL⊢⊡[pj+1↔H′j+1(pj+2,...,pn)]→[⊡(pi↔Hi(pj+1,...,pn))↔⊡(pi↔Hi(H′j+1,...,pn)).
Let H′i stand for Hi(H′j+1,...,pn), and by combining the previous lines we find that GL⊢∧i≤j+1{⊡(pi↔Ai(p1,...,pn)}→∧i≤j+1{⊡(pi↔H′i(pj+2,...,pn))}.
By Goldfarb’s lemma, we do not need to check the other direction, so GL⊢∧i≤j+1{⊡(pi↔Ai(p1,...,pn)}↔∧i≤j+1{⊡(pi↔H′i(pj+2,...,pn))} and the proof is finished □
An immediate consequence of the theorem is that for those fixed points Hi and every Ai, GL⊢Hi↔Ai(H1,...,Hn).
Indeed, since GL is closed under substitution, we can make the change pi for Hi in the theorem to get that GL⊢∧i≤n{⊡(Hi↔Ai(H1,...,Hn)}↔∧i≤n{⊡(Hi↔Hi)}.
Since the righthand side is trivially a theorem of GL, 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 H′i to compute fixed points.
Uniqueness of arithmetic fixed points:
Notation: ⊡A=□A∧A
Let H be a fixed point on p of ϕ(p); that is, GL⊢⊡(p↔ϕ(p))↔(p↔H).
Suppose I is such that GL⊢H↔I. Then by the first substitution theorem, GL⊢F(I)↔F(H) for every formula F(q). If F(q)=⊡(p↔q), then GL⊢⊡(p↔H)↔⊡(p↔I), from which it follows that GL⊢⊡(p↔ϕ(p))↔(p↔I).
Conversely, if H and I are fixed points, then GL⊢⊡(p↔H)↔⊡(p↔I), so since GL is closed under substitution, GL⊢⊡(H↔H)↔⊡(H↔I). Since GL⊢⊡(H↔H), it follows that GL⊢(H↔I).
(Taken from The Logic of Provability, by G. Boolos.)