# Substituição (lógica)

Substituição é um conceito fundamental em lógica. Uma substituição é uma transformação sintática em uma expressão formal. Aplicar uma substituição a uma expressão significa trocar uma variável ou símbolos por outras expressões. A expressão resultante é chamada de uma instância de substituição da expressão original

## Lógica Proposicional
### Definição

Onde Ψ e Φ representam fórmulas da lógica proposicional, Ψ é uma instância de substituição de Φ se e somente se Ψ pode ser obtida de Φ ao se substituir formulas por símbolos em Φ, sempre trocando uma ocorrência do mesmo símbolo por uma ocorrência da mesma fórmula. Por exemplo:
       (R → S) & (T → S)
é uma instância de substituição de:
       P & Q
e
       (A ↔ A) ↔ (A ↔ A)
é uma instância de substituição de:
       (A ↔ A)
Em alguns sistemas de dedução para a lógica proposicional, uma nova expressão (uma proposição) pode ser introduzida numa linha de uma derivação se ela é uma instância de substituição de uma linha anterior da derivação (Hunter 1971, p. 118). É assim que novas linhas são introduzidas em alguns sistemas axiomáticos. Em sistemas que usam regras de transformação, uma regra pode incluir o uso de uma instância de substituição para propósitos de introduzir uma certa variável a uma derivação.
Na lógica de primeira ordem, toda fórmula proposicional fechada que pode ser derivada de uma fórmula proposicional aberta a por substituição é dita ser uma instância de substituição de a. Se a é uma formula proposicional fechada, dizemos que a própria a é sua única instância de substituição.

### Tautologias

Uma fórmula proposicional é uma tautologia se ela é verdadeira sob todas as valorações (ou interpretações) possíveis dos símbolos de seus predicados. Se Φ é uma tautologia, e Θ é uma instância de substituição de Φ, então Θ também é uma tautologia. Este fato implica a corretude da regra de dedução descrita na sessão anterior.

## Lógica de Primeira Ordem

Na lógica de primeira ordem, uma substituição é um mapeamento total σ: V → T de variáveis a termos; a notação { x$_1$ ↦ t$_1$, ..., x$_k$ ↦ t$_k$ }
se refere a uma substituição que mapeia cada variável x$_i$ para o termo correspondente t$_i$, para i=1,...,k, e todas as outras variáveis a si mesmas; os x$_i$ devem ser distintos e disjuntos. Aplicando esta substituição a um termo t é escrito em notação pós-fixa como t { x$_1$ ↦ t$_1$, ..., x$_k$ ↦ t$_k$ }; que significa trocar (simultaneamente) todas as ocorrências de cada x$_i$ em t por t$_i$. O resultado tσ de aplicar uma substituição σ a um termo t é chamada uma instância daquele termo t. Por exemplo, aplicando a substituição { x ↦ z, z ↦ h(a,y) } ao termo
    f( z , a,g( x ),y) produz f( h(a,y) , a,g( z ),y) .
O domínio dom(σ) de uma substituição σ é comumente definido como o conjunto de variáveis realmente trocadas, ex.: dom(σ) = { x ∈ V | xσ ≠ x }. Uma substituição é chamada substituição básica se ela mapeia todas as variáveis do seu domínio para um termo sem variável, ex.: livre de variáveis, termos. A instância de substituição tσ de uma substituição básica é um termo básico se todas as variáveis de t estão no domínio de σ, ex.: se vars(t) ⊆ dom(σ). Uma substituição σ é chamada uma substituição linear se tσ é um termo linear para algum (e portanto todos) termo t contendo apenas as variáveis do domínio de σ, ex.: com vars(t) = dom(σ). Uma substituição σ é dita substituição plana se xσ é uma variável para cada variável x. Uma substituição σ é chamada de substituição de renomeação se ela é uma permutação no conjunto de todas as variáveis. Como todas permutações, uma substituição de renomeação σ sempre tem uma substituição inversa σ$^{−1}$, tal que tσσ$^{−1}$ = t = tσ$^{−1}$σ para todo termo t. Contudo, não é possível definir uma inversa para uma substituição arbitrária.
Por exemplo, { x ↦ 2, y ↦ 3+4 } é uma substituição básica, { x ↦ x$_1$, y ↦ y$_2$+4 } é uma substituição não-básica e não-plana, porém linear, { x ↦ y$_2$, y ↦ y$_2$+4 } é não-linear e não-plana, { x ↦ y$_2$, y ↦ y$_2$ } é plana, mas não-linear, { x ↦ x$_1$, y ↦ y$_2$ } é tanto linear quanto plana, porém não renomeante, já que ela mapeia ambos y e y$_2$ para y$_2$; cada uma dessas substituições tem o conjunto {x,y} como seu domínio. Um exemplo de uma substituição de renomeação é { x ↦ x$_1$, x$_1$ ↦ y, y ↦ y$_2$, y$_2$ ↦ x }, se ela tem inversa { x ↦ y$_2$, y$_2$ ↦ y, y ↦ x$_1$, x$_1$ ↦ x }. A substituição planar { x ↦ z, y ↦ z } não pode ter uma inversa, já que por exemplo (x+y) { x ↦ z, y ↦ z } = z+z, e o termo posterior não pode ser transformado de volta para x+y, pois a informação sobre a origem de onde z decorre é perdida. A substituição básica { x ↦ 2 } não pode ter uma inversa devido a uma similar perda de informação ex.: em (x+2) { x ↦ 2 } = 2+2, mesmo que trocar constantes por variáveis tenha fosse permitido por algum tipo fictício de "substituição generalizada".
Duas substituições são consideradas iguais se elas mapeiam cada variável a termos resultando estruturalmente iguais, formalmente: σ = τ se xσ = xτ para toda variável x ∈ V. A composição de suas substituições σ = { x$_1$ ↦ t$_1$, ..., x$_k$ ↦ t$_k$ } e τ = { y$_1$ ↦ u$_1$, ..., y$_l$ ↦ u$_l$ } é obtida ao se remover da substituição { x$_1$ ↦ t$_1$τ, ..., x$_k$ ↦ t$_k$τ, y$_1$ ↦ u$_1$, ..., y$_l$ ↦ u$_l$ } os pares y$_i$ ↦ u$_i$ para os quais y$_i$ ∈ { x$_1$, ..., x$_k$ }. A composição de σ e τ é denotada por στ. Composição é uma operação associativa, e é compatível com a aplicação de substituições, ex.: (ρσ)τ = ρ(στ), w (tσ)τ = t(στ), respectivamente, para todas as substituições ρ, σ, τ, e todo termo t. A substituição identidade, que mapeia todas as variáveis a sí mesmas, é o elemento neutro na composição de substituições. Uma substituição σ é dita idempotente se σσ = σ, e portanto tσσ = tσ para todo termo t. A substituição { x$_1$ ↦ t$_1$, ..., x$_k$ ↦ t$_k$ } é idempotente se e somente se nenhuma das variáveis x$_i$ ocorre em qualquer t$_i$. Composição de substituições não é comutativa, isto é, στ pode ser diferente de τσ, mesmo se σ e τ são idempotentes.
Por exemplo, { x ↦ 2, y ↦ 3+4 } é igual a { y ↦ 3+4, x ↦ 2 }, mas diferente de { x ↦ 2, y ↦ 7 }. A substituição { x ↦ y+y } é idempotente, ex.: ((x+y) {x↦y+y}) {x↦y+y} = ((y+y)+y) {x↦y+y} = (y+y)+y, enquanto que a substituição { x ↦ x+y } não é, ex.: ((x+y) {x↦x+y}) {x↦x+y} = ((x+y)+y) {x↦x+y} = ((x+y)+y)+y. Um exemplo de substituições não comutativas é { x ↦ y } { y ↦ z } = { x ↦ z, y ↦ z }, mas { y ↦ z} { x ↦ y} = { x ↦ y, y ↦ z }.