Igualdade
$$\Huge \ndIEqual \qquad \ndEEqual $$
Introdução da Igualdade
Introdução da Igualdade ($\ndIEqual$)
$$\Large \ndIEqual: ~ \vdash t = t $$ ou $$\Large \ndrule{}{t = t}{\ndIEqual} $$ onde $t$ é um termo fechado (sem variáveis).
Eliminação da Igualdade
Eliminação da Igualdade ($\ndEEqual$)
$$\Large \ndEEqual: \cbr{t_1 = t_2, p\subst{x}{t_1}} \vdash p\subst{x}{t_2} $$ ou $$\Large \ndrule{t_1 = t_2 & p\subst{x}{t_1}}{p\subst{x}{t_2}}{\ndEEqual} $$ desde que $t_1, t_2$ sejam livres para $x$ em $p$.
Exemplo Informal: Eliminação da Igualdade
| Linha | Fórmula | Justificação |
|---|---|---|
| 1 | $x > 1$ | $p(x)$ |
| 2 | $42 > 1$ | $42$ satisfaz $p(x)$. Isto é, $p\subst{x}{42}$ |
| 3 | $42 = 40 + 2$ | Aritmética ($t_1 = t_2$) |
| 4 | $40 + 2 > 1$ | $p\subst{x}{40 + 2}$ |