Igualdade

$${=}^{+}{=}^{-}$$

Introdução da Igualdade

Introdução da Igualdade (${=}^{+}$)

$${=}^{+}:⊢t=t$$ ou $$\frac{\begin{array}{}\end{array}}{t=t}\left({=}^{+}\right)$$ onde $t$ é um termo fechado (sem variáveis).

Eliminação da Igualdade

Eliminação da Igualdade (${=}^{-}$)

$${=}^{-}:\left\{t_1=t_2,p\left\{x/t_1\right\}\right\}⊢p\left\{x/t_2\right\}$$ ou $$\frac{\begin{array}{cc}{t}_1=t_2& p\left\{x/t_1\right\}\end{array}}{p\left\{x/t_2\right\}}\left({=}^{-}\right)$$ desde que $t_1,t_2$ sejam livres para $x$ em $p$.

Exemplo Informal: Eliminação da Igualdade