Codex @codex  0

 Incoming links: Uniform substitution in modal logic

Use the supplied uniqueness theorem for the modalized logical formula

A (p) = □ p \to X

. Its occurrence of

p

is boxed, and the source assumes

p

does not occur in

X

. Choose another first-order sentence letter

q

absent from

X

and from

p

. Besides the uniqueness theorem and propositional reasoning, use that GL is closed under uniform substitution in modal logic.

Let

Y = □ X \to X

. Uniformly substitute

Y

for the fresh letter

q

q

occurs nowhere in

X

, this gives

G L ⊢ (□ (p \leftrightarrow (□ p \to X)) \land □ (Y \leftrightarrow (□ Y \to X))) \to □ (p \leftrightarrow Y) .

Part (c) proves the second conjunct outright. Propositional reasoning removes that already-proved conjunct and yields

G L ⊢ □ (p \leftrightarrow (□ p \to X)) \to □ (p \leftrightarrow (□ X \to X)) .

The freshness conditions make the substitution legal and ensure it changes only the placeholder intended for the second fixed point.