Exercício 13:
Defina substituição simultânea em uma
-fórmula
por indução na complexidade.
Defina substituição simultânea em uma
Passo 1
Estamos lidando com Lógica de Primeira Ordem: queremos definir a substituição simultânea de termos
pelas variáveis
em uma fórmula
, usando indução na complexidade da fórmula.
Definimos a medida de complexidade recursivamente:
Definimos a medida de complexidade
- Se
é atômica (da forma ) ou , então . -
. -
, onde . -
, onde .
Passo 2
Fazemos indução em
. Caso base (
):
- Se
, definimos
- Se
Passo 3
Passo indutivo para conectivos (
):
- Se
,
- Se
Passo 4
Passo indutivo para quantificadores: seja
, com
.
- Se
e não ocorre em nenhum , então
- Caso
Passo 5
Dessa forma cobrimos todos os casos na indução sobre a complexidade de
.
Resposta
A substituição simultânea de termos
pelas variáveis
na fórmula
, denotada
é definida por indução na complexidade de
- Caso base (
): - Se
, então
- Se
$$\varphi[x_1/t_1,\dots,x_n/t_n]=R\bigl(s_1[x_1/t_1,\dots,x_n/t_n],\dots,s_m[x_1/t_1,\dots,x_n/t_n]\bigr).
$$
- Conectivos (
): - Se
, então
- Se
$$\varphi[x_1/t_1,\dots,x_n/t_n]=\lnot\bigl(\psi[x_1/t_1,\dots,x_n/t_n]\bigr).
$$
- Quantificadores: se
com : - Se
e não ocorre em nenhum , então
- Se
$$\varphi[x_1/t_1,\dots,x_n/t_n]=Qy\bigl(\psi[x_1/t_1,\dots,x_n/t_n]\bigr).
$$
- Caso contrário, renomeie para uma variável fresca
(
-conversão), escreva
e aplique o caso anterior.
- Caso contrário, renomeie
Assim temos a definição completa por indução na complexidade de
.