é minha derivação de$\vdash (\forall x)(B \implies C) \implies ((\forall x)B \implies (\forall x)C)$correto?
Estou lendo Introdução à lógica matemática de Mendelson. Estou no capítulo 2 "Lógica de primeira ordem e teoria dos modelos". Os axiomas são:
($A1$):$B ⇒ (C ⇒ B)$
($A2$):$(B ⇒ (C ⇒ D)) ⇒ ((B ⇒ C) ⇒ (B ⇒ D))$
($A3$):$(¬C ⇒ ¬B) ⇒ ((¬C ⇒ B) ⇒ C)$
($A4$):$(∀x_i)B(x_i) ⇒ B(t)$E se$B(x_i)$
($A5$):$(∀x_i)(B ⇒ C) ⇒ (B ⇒ (∀x_i)C)$
As regras são:
- Modus ponens:$C$segue de$B$e$B ⇒ C$. (MP)
- Generalização:$(∀x_i)B$segue de$B$. (Gen)
O exercício 2.27a (da seção 2.4) é$⊢ (∀x)(B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C)$e notei que a derivação que Mendelson dá nas soluções difere da minha (usei o Axioma 5 uma vez e não usei a regra Gen, e Mendelson não usou o Axioma 5, mas usou a regra Gen), então queria perguntar:
- Minha derivação está correta?
- Se estiver incorreto, qual é o erro?
Minha derivação (usando o teorema da dedução) é a seguinte:
- $(∀x)(B ⇒ C)$hip
- $(∀x)B$hip
- $(∀x)(B ⇒ C) ⇒ (B ⇒ (∀x)C)$Axioma (A5)
- $B ⇒ (∀x)C$MP 1,3
- $(∀x)B ⇒ B$Axioma (A4)
- $B$MP 2,5
- $(∀x)C$MP 4,6
- $(∀x)(B ⇒ C), (∀x)B ⊢ (∀x)C$1-7
- $(∀x)(B ⇒ C) ⊢ (∀x)B ⇒ (∀x)C$1-8 corolário 2.6 (Mendelson)
- $⊢ (∀x)(B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C)$1-9 corolário 2.6 (Mendelson)
A derivação de Mendelson (usando o teorema da dedução) é a seguinte:
- $(∀x)(B ⇒ C)$hip
- $(∀x)B$hip
- $(∀x)(B ⇒ C) ⇒ (B ⇒ C)$Axioma (A4)
- $B ⇒ C$1, 3, PM
- $(∀x)B ⇒ B$Axioma (A4)
- $B$2, 5, PM
- $C$4, 6, PM
- $(∀x)C$7, Gen
- $(∀x)(B ⇒ C), (∀x)B ⊢ (∀x)C$1–8
- $(∀x)(B ⇒ C) ⊢ (∀x)B ⇒ (∀x)C$1–9, Corolário 2.6
- $⊢ (∀x)(B ⇒ C) ⇒ ((∀x)B ⇒ (∀x)C)$1–10, Corolário 2.6
Respostas
Sua tentativa de derivação está errada. De fato, no axioma$A5$, há uma condição colateral : a fórmula$B$não deve conter nenhuma ocorrência livre da variável$x$(esta condição lateral deve ser relatada no livro de Mendelson), enquanto na fórmula que você deseja provar$B$pode conter ocorrências livres de$x$. Portanto, o terceiro passo da sua derivação está errado: você não pode justificar a fórmula$∀x(B \to C) \to (B \to ∀x C)$como uma instância de axioma$A5$, Porque$x$pode ocorrer gratuitamente em$B$.
Pelo contrário, a derivação de Mendelson é, obviamente, perfeitamente correta. Em particular, não usa nenhum axioma com tais restrições.
A propósito, observe também que o uso da regra de generalização é afetado por uma condição secundária: você pode derivar$\forall x B$a partir de$B$desde que a variável$x$não ocorre livre em nenhuma hipótese da derivação. A derivação de Mendelson respeita esta condição lateral quando usa a regra de generalização.
As condições secundárias são importantes, pois evitam derivar fórmulas que não deveriam ser demonstráveis.