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 editar

Definição editar

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 editar

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 editar

Na lógica de primeira ordem, uma substituição é um mapeamento total σ: VT de variáveis a termos; a notação { x1t1, ..., xktk } [note 1] se refere a uma substituição que mapeia cada variável xi para o termo correspondente ti, para i=1,...,k, e todas as outras variáveis a si mesmas; os xi devem ser distintos e disjuntos. Aplicando esta substituição a um termo t é escrito em notação pós-fixa como t { x1t1, ..., xktk }; que significa trocar (simultaneamente) todas as ocorrências de cada xi em t por ti. [note 2] 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 { xz, zh(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(σ) = { xV | 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, { xx1, yy2+4 } é uma substituição não-básica e não-plana, porém linear, { xy2, yy2+4 } é não-linear e não-plana, { xy2, yy2 } é plana, mas não-linear, { xx1, yy2 } é tanto linear quanto plana, porém não renomeante, já que ela mapeia ambos y e y2 para y2; cada uma dessas substituições tem o conjunto {x,y} como seu domínio. Um exemplo de uma substituição de renomeação é { xx1, x1y, yy2, y2x }, se ela tem inversa { xy2, y2y, yx1, x1x }. A substituição planar { xz, yz } não pode ter uma inversa, já que por exemplo (x+y) { xz, yz } = 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 xV. A composição de suas substituições σ = { x1t1, ..., xktk } e τ = { y1u1, ..., yl ↦ ul } é obtida ao se remover da substituição { x1t1τ, ..., xktkτ, y1u1, ..., ylul } os pares yiui para os quais yi ∈ { x1, ..., xk }. 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 { x1t1, ..., xktk } é idempotente se e somente se nenhuma das variáveis xi ocorre em qualquer ti. Composição de substituições não é comutativa, isto é, στ pode ser diferente de τσ, mesmo se σ e τ são idempotentes.[1][2]

Por exemplo, { x ↦ 2, y ↦ 3+4 } é igual a { y ↦ 3+4, x ↦ 2 }, mas diferente de { x ↦ 2, y ↦ 7 }. A substituição { xy+y } é idempotente, ex.: ((x+y) {xy+y}) {xy+y} = ((y+y)+y) {xy+y} = (y+y)+y, enquanto que a substituição { xx+y } não é, ex.: ((x+y) {xx+y}) {xx+y} = ((x+y)+y) {xx+y} = ((x+y)+y)+y. Um exemplo de substituições não comutativas é { xy } { yz } = { xz, yz }, mas { yz} { xy} = { xy, yz }.

Ver também editar

Notas editar

  1. alguns autores usam [ t1/x1, ..., tk/xk ] para denotar esta substituição, e.g. M. Wirsing (1990). Jan van Leeuwen, ed. Algebraic Specification. Col: Handbook of Theoretical Computer Science. B. [S.l.]: Elsevier. pp. 675–788 , here: p.682;
  2. De um ponto de vista algebraico de termos, o conjunto T de termos é o termo algebraico livre sobre o conjunto V de variáveis, daqui para cada mapeamento σ: VT existem um homomorfismo unico σ: TT que está de acordo com σ em VT; a aplicação definida acima de σ a um termo t é vista como aplicar a função σ ao argumento t.

Referências editar

  • Hunter, G. (1971). Metalogic: An Introduction to the Metatheory of Standard First Order Logic. University of California Press. ISBN 0-520-01822-2
  • Kleene, S. C. (1967). Mathematical Logic. Reprinted 2002, Dover. ISBN 0-486-42533-9
  1. David A. Duffy (1991). Principles of Automated Theorem Proving. [S.l.]: Wiley ; here: p.73-74
  2. Franz Baader, Wayne Snyder (2001). Alan Robinson and Andrei Voronkov, ed. Unification Theory (PDF). [S.l.]: Elsevier. pp. 439–526 ; here: p.445-446

Ligações externas editar