The diagonal lemma states that: ∀Φ∃Ψ (Ψ<—>Φ(⌜Ψ⌝))
A classic use of this lemma/theorem is to prove Löb’s theorem in provability logic. In that case, the theorem is instantiated to Q<—>(Prv(Q)—>P).
Take the following argument in which the theorem is instantiated in a similar way to the use in the proof of Löb’s theorem where ‘~’ is Classical negation:
- ∀Φ∃Ψ (Ψ<—>Φ(⌜Ψ⌝))
- ∃Ψ (Ψ<—>(Ψ—>P))
- ∃Ψ (Ψ<—>(Ψ—>~P))
- Q<—>(Q—>P) Hypothesis for Existential Elim
-
R<—>(R—>~P) Hypothesis for Existential Elim -
R & ~P 5, Prop Logic -
Q & P 4, Prop Logic - ⊥ 6,7 Prop Logic
- ⊥ 4,5 6-8 Existential Elim x2
What is wrong here? Is this just a re-statement of Gödel’s theorems? Clearly, both uses of ‘P’ come from a universal quantifier, so it should be ok to use it twice. Any clarification is appreciated.
The error is at line 2. As indicated by the Quine corners, $\Phi$ is supposed to be a statement about the Gödel number of $\Psi$, but you take it to be $\Psi\to P$, which involves the truth value of $\Psi$. There's no way to define the truth value from the Gödel number; that's Tarski's theorem on undefinability of truth.