There is no predicate τ, s.t. for any sentence σ, σ is provable in T iff τ/[⌜σ⌝] is so.
2.6. Tarski's Undefinability Theorem
Tarski's undefinability theorem states that the arithmetical truth cannot be defined in arithmetic itself.
To show this, we first prove the below lemma.
This lemma states that there is no predicate τ s.t. for any sentence σ,
σ is provable in a theory T iff τ/[⌜σ⌝] is so.
theorem
LO.FirstOrder.Arithmetic.not_exists_tarski_predicate {T : Theory ℒₒᵣ} [𝗜𝚺₁ ⪯ T] [Consistent T] : ¬∃ τ, ∀ (σ : Semisentence ℒₒᵣ 0), T ⊢ σ ⭤ τ/[⌜σ⌝]LO.FirstOrder.Arithmetic.not_exists_tarski_predicate {T : Theory ℒₒᵣ} [𝗜𝚺₁ ⪯ T] [Consistent T] : ¬∃ τ, ∀ (σ : Semisentence ℒₒᵣ 0), T ⊢ σ ⭤ τ/[⌜σ⌝]
Then, the main theorem is obtained by using theory T as True Arithmetic 𝗧𝗔.
theorem
LO.FirstOrder.Arithmetic.undefinability_of_truth : ¬∃ τ, ∀ (σ : Sentence ℒₒᵣ), ℕ ⊧ₘ σ ↔ ℕ ⊧ₘ τ/[⌜σ⌝]LO.FirstOrder.Arithmetic.undefinability_of_truth : ¬∃ τ, ∀ (σ : Sentence ℒₒᵣ), ℕ ⊧ₘ σ ↔ ℕ ⊧ₘ τ/[⌜σ⌝]
Tarski's Undefinability of Truth Theorem.