---
tag: YEHH5WV8B6
kind: statement
role: lemma
name: Uniform diagonal lemma
sources:
  - wikipedia: en:348969@r1344931050
    locator: Diagonal lemma, section Some generalizations > Uniform diagonal lemma
    note: adopted
    mention: wikipedia://en/348969#V6CD
    sections: [Statement]
inventory: [XYRZZXD0D7]
---

## Statement

Let $\psi (x, y_1, \dots , y_n)$ be any formula with free variables $x, y_1, \dots , y_n$.

Then there is a formula $\varphi (y_1, \dots y_n)$ with free variables $y_1, \dots , y_n$ such that for all $m_1 , \dots , m_n \in \mathbb{N}$, $T \vdash \varphi (\overline{m_1} , \dots , \overline{m_n}) \leftrightarrow \psi (\ulcorner \varphi (\overline{m_1} , \dots , \overline{m_n}) \urcorner, \overline{m_1} , \dots , \overline{m_n})$.