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 | editar código-fonte]Definição
[editar | editar código-fonte]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 | editar código-fonte]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 | editar código-fonte]Na lógica de primeira ordem, uma substituição é um mapeamento total σ: V → T de variáveis a termos; a notação { x1 ↦ t1, ..., xk ↦ tk } [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 { x1 ↦ t1, ..., xk ↦ tk }; 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 { 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 ↦ x1, y ↦ y2+4 } é uma substituição não-básica e não-plana, porém linear, { x ↦ y2, y ↦ y2+4 } é não-linear e não-plana, { x ↦ y2, y ↦ y2 } é plana, mas não-linear, { x ↦ x1, y ↦ y2 } é 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 é { x ↦ x1, x1 ↦ y, y ↦ y2, y2 ↦ x }, se ela tem inversa { x ↦ y2, y2 ↦ y, y ↦ x1, x1 ↦ 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 σ = { x1 ↦ t1, ..., xk ↦ tk } e τ = { y1 ↦ u1, ..., yl ↦ ul } é obtida ao se remover da substituição { x1 ↦ t1τ, ..., xk ↦ tkτ, y1 ↦ u1, ..., yl ↦ ul } os pares yi ↦ ui 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 { x1 ↦ t1, ..., xk ↦ tk } é 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 { 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 }.
Ver também
[editar | editar código-fonte]- Propriedade de substituição em Igualdade Matemática
- Lógica de Primeira Ordem
- Regra da Substituição Universal
- Lambda calculus
- Semântica de Valor Verdade
- Unificação
- Metavariável
- Mutatis mutandis
- Regra de Troca
Notas
[editar | editar código-fonte]- ↑ 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;
- ↑ 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 σ: V → T existem um homomorfismo unico σ: T → T que está de acordo com σ em V ⊆ T; a aplicação definida acima de σ a um termo t é vista como aplicar a função σ ao argumento t.
Referências
[editar | editar código-fonte]- 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
- ↑ David A. Duffy (1991). Principles of Automated Theorem Proving. [S.l.]: Wiley; here: p.73-74
- ↑ 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 | editar código-fonte]- Substituição no nLab