Аксиомы равенства

Аксио́мы ра́венства, аксиомы, регулирующие употребление отношения равенства в математических доказательствах. Аксиомы эти утверждают рефлексивность отношения равенства и возможность замены равного равным. Символически аксиомы равенства записываются так:

${\displaystyle x=x}$
${\displaystyle x=y\wedge \varphi (y/v)\Rightarrow \varphi (y/v)}$
${\displaystyle x=y\Rightarrow t(y/v)=t(x/v),}$

где ${\displaystyle \varphi }$ – произвольная формула, a ${\displaystyle t}$ – произвольный терм рассматриваемого языка; ${\displaystyle x}$, ${\displaystyle y}$, ${\displaystyle v}$ – переменные, имеющие одну и ту же непустую область изменения; выражения вида ${\displaystyle \varphi (x/v)}$ и ${\displaystyle t(x/v)}$ обозначают результат замены всех свободных вхождений переменной ${\displaystyle v}$ в формуле ${\displaystyle \varphi }$ или терме ${\displaystyle t}$ на ${\displaystyle x}$.

С помощью аксиом равенства можно доказать симметричность и транзитивность отношения равенства. Для этого в качестве ${\displaystyle \varphi }$ надо взять формулу ${\displaystyle y=v}$ в первом случае и формулу ${\displaystyle v=z}$ во втором.

Если формулы и термы рассматриваемого языка строятся из атомарных формул и термов с помощью логических связок и суперпозиций, то приведённые аксиомы равенства можно вывести из их частных случаев, когда в качестве ${\displaystyle \varphi }$ и ${\displaystyle t}$ берутся атомарные формулы и термы. Символически:

${\displaystyle x_{i}=y_{i}\wedge P(x_{1},\ldots ,x_{i}\ldots ,x_{n})\Rightarrow \ P(x_{1},\ldots y_{i},\ldots x_{n})}$
${\displaystyle x_{i}=y_{i}\Rightarrow f(x_{1},\ldots x_{i},\ldots x_{n})=f(x_{1},\ldots y_{i},\ldots x_{n}),}$

где ${\displaystyle P}$ и ${\displaystyle f}$ суть ${\displaystyle n}$-местные предикатный и функциональный символы.