Vamos estabelecer duas regras para cada quantificador: uma para removê-lo e outra para inserí-lo na derivação.
Temos que ser muito cautelosos na aplicação destas regras, pois elas tem muitas restrições. Algumas regras terão a restrição de substitualidade, a qual cabe definir agora:
Dada uma constante c {\displaystyle \mathrm {c} } , uma variável x {\displaystyle x} e uma fórmula α {\displaystyle \alpha } quantificada, se c {\displaystyle \mathrm {c} } não ocorre em α {\displaystyle \alpha } no escopo do quantificador para x {\displaystyle x} , então dizemos que c {\displaystyle \mathrm {c} } é substituível por x {\displaystyle x} em α {\displaystyle \alpha } .Eliminação do Universal
editar
∀ x ( α ) α [ x / c ] {\displaystyle {\frac {\forall x(\alpha )}{\alpha \left[x/\mathrm {c} \right]}}} Ou seja, dada uma fórmula ∀ x α {\displaystyle \forall x\alpha } , aplica-se a eliminação do universal, derivando uma fórmula α {\displaystyle \alpha } tal que a variável x {\displaystyle x} dá lugar a uma constante c {\displaystyle \mathrm {c} } .
{ ∀ x ( H x → M x ) , H s } ⊢ M s {\displaystyle \left\{\forall x\left(Hx\to Mx\right),Hs\right\}\vdash Ms}
1.
∀ x ( H x → M x ) {\displaystyle \forall x\left(Hx\to Mx\right)}
Premissa
2.
H s {\displaystyle Hs}
Premissa
3.
H s → M s {\displaystyle Hs\to Ms}
1 E ∀ {\displaystyle {\mathcal {E}}\forall }
4.
M s {\displaystyle Ms}
3,2 MP
CUIDADO Lembre-se que esta regra é aplicável a fórmulas quantificadas universalmente, e não a quaisquer fórmulas que contém o quantificador universal. Por exemplo, a eliminação do universal não é aplicável à fórmula ∀ x H x → M s {\displaystyle \forall xHx\to Ms} .
Introdução do Universal
editar
α ( c ) ∀ x α ( c / x ) {\displaystyle {\frac {\alpha \left(\mathrm {c} \right)}{\forall x\alpha \left(\mathrm {c} /x\right)}}} Ou seja, dada uma fórmula α {\displaystyle \alpha } na qual ocorre a constante c {\displaystyle \mathrm {c} } , aplica-se a introdução do universal, derivando uma fórmula ∀ x α {\displaystyle \forall x\alpha } tal que a constante c {\displaystyle \mathrm {c} } dá lugar à variável x {\displaystyle x} . A esta regra coloca-se as seguintes restrições:
a constante c {\displaystyle \mathrm {c} } não pode ocorrer em premissa ou hipótese vigente .
c {\displaystyle \mathrm {c} } deve ser substituível por x {\displaystyle x} em α {\displaystyle \alpha } .{ ∀ x ( A x → B x ) , ∀ x ( B x → C x ) } ⊢ ∀ x ( A x → C x ) {\displaystyle \left\{\forall x\left(Ax\to Bx\right),\forall x\left(Bx\to Cx\right)\right\}\vdash \forall x\left(Ax\to Cx\right)}
1.
∀ x ( A x → B x ) {\displaystyle \forall x\left(Ax\to Bx\right)}
Premissa
2.
∀ x ( B x → C x ) {\displaystyle \forall x\left(Bx\to Cx\right)}
Premissa
3.
A c → B c {\displaystyle Ac\to Bc}
1 E ∀ {\displaystyle {\mathcal {E}}\forall }
4.
B c → C c {\displaystyle Bc\to Cc}
2 E ∀ {\displaystyle {\mathcal {E}}\forall }
5.
A c → C c {\displaystyle Ac\to Cc}
3,4 SH
6.
∀ x ( A x → C x ) {\displaystyle \forall x\left(Ax\to Cx\right)}
5 I ∀ {\displaystyle {\mathcal {I}}\forall }
∀ x ∀ y P x y ⊢ ∀ y ∀ x P y x {\displaystyle \forall x\forall yPxy\vdash \forall y\forall xPyx}
1.
∀ x ∀ y P x y {\displaystyle \forall x\forall yPxy}
Premissa
2.
∀ x P x b {\displaystyle \forall xPxb}
1 E ∀ {\displaystyle {\mathcal {E}}\forall }
3.
P a b {\displaystyle Pab}
2 E ∀ {\displaystyle {\mathcal {E}}\forall }
4.
∀ x P a x {\displaystyle \forall xPax}
3 I ∀ {\displaystyle {\mathcal {I}}\forall }
5.
∀ y ∀ x P y x {\displaystyle \forall y\forall xPyx}
4 I ∀ {\displaystyle {\mathcal {I}}\forall }
CUIDADO O desrespeito à primeira restrição acarretará em derivações falaciosas. Por exemplo:
1.
L f {\displaystyle Lf}
Premissa
2.
∀ x L x {\displaystyle \forall xLx}
1 I ∀ {\displaystyle {\mathcal {I}}\forall }
Algo como "Frege é lógico. Logo, todos são lógicos ". O que é obviamente inválido.
O desrespeito à segunda restrição também acarretará em derivações absurdas, tais como:
1.
∀ x ∃ y A x y {\displaystyle \forall x\exists yAxy}
Premissa
2.
∃ y A b y {\displaystyle \exists yAby}
1 E ∀ {\displaystyle {\mathcal {E}}\forall }
3.
∀ y ∃ y A y y {\displaystyle \forall y\exists yAyy}
2 I ∀ {\displaystyle {\mathcal {I}}\forall }
Introdução do Existencial
editar
α ( c ) ∃ x α ( c / x ) {\displaystyle {\frac {\alpha \left(\mathrm {c} \right)}{\exists x\alpha \left(\mathrm {c} /x\right)}}} Ou seja, dada uma fórmula α {\displaystyle \alpha } na qual ocorre a constante c {\displaystyle \mathrm {c} } , aplica-se a introdução do existencial, derivando uma fórmula ∃ x α {\displaystyle \exists x\alpha } tal que a constante c {\displaystyle \mathrm {c} } dá lugar à variável x {\displaystyle x} . A esta regra coloca-se a restrição de que c {\displaystyle \mathrm {c} } deve ser substituível por x {\displaystyle x} em α {\displaystyle \alpha } .
∀ x P x ⊢ ∃ x P x {\displaystyle \forall xPx\vdash \exists xPx}
1.
∀ x P x {\displaystyle \forall xPx}
Premissa
2.
P a {\displaystyle Pa}
1 E ∀ {\displaystyle {\mathcal {E}}\forall }
3.
∃ x P x {\displaystyle \exists xPx}
2 I ∃ {\displaystyle {\mathcal {I}}\exists }
A c ∧ L a ⊢ ∃ x A x ∧ ∃ y L y {\displaystyle Ac\land La\vdash \exists xAx\land \exists yLy}
1.
A c ∧ L a {\displaystyle Ac\land La}
Premissa
2.
A c {\displaystyle Ac}
1 S
3.
∃ x A x {\displaystyle \exists xAx}
2 I ∃ {\displaystyle {\mathcal {I}}\exists }
4.
L a {\displaystyle La}
1 S
5.
∃ y L y {\displaystyle \exists yLy}
4 I ∃ {\displaystyle {\mathcal {I}}\exists }
6.
∃ x A x ∧ ∃ y L y {\displaystyle \exists xAx\land \exists yLy}
3,5 C
CUIDADO Lembre-se que apenas uma constante por vez pode ser substituída pela variável. Caso o contrário, ter-se-ia derivações absurdas como:
1.
A c ∧ L a {\displaystyle Ac\land La}
Premissa
2.
∃ x ( A x ∧ L x ) {\displaystyle \exists x\left(Ax\land Lx\right)}
1 I ∃ {\displaystyle {\mathcal {I}}\exists }
Algo como "Colombo descobriu a América e Armstrong andou sobre a Lua. Logo, alguém descobriu a América e andou sobre a Lua ". O que é obviamente inválido.
Eliminação do Existencial
editar
Trataremos aqui a eliminação do existencial como uma regra de inferência hipotética:
Dada uma fórmula ∃ x α {\displaystyle \exists x\alpha } , levanta-se como hipótese uma fórmula α {\displaystyle \alpha } tal que a variável x {\displaystyle x} dá lugar a uma constante c {\displaystyle \mathrm {c} } . Desta hipótese, deriva-se uma fórmula β {\displaystyle \beta } . Ao aplicar a eliminação do existencial, descarta-se a hipótese e β {\displaystyle \beta } é inserida na derivação. A esta regra coloca-se a seguinte restrição: a constante c {\displaystyle \mathrm {c} } não pode ocorrer em premissa, hipótese vigente, em α {\displaystyle \alpha } ou β {\displaystyle \beta } .
{ ∃ x P x , ( ∃ x ¬ ¬ P x ) → Q b } ⊢ Q b {\displaystyle \left\{\exists xPx,\left(\exists x\neg \neg Px\right)\to Qb\right\}\vdash Qb}
1.
∃ x P x {\displaystyle \exists xPx}
Premissa
2.
( ∃ x ¬ ¬ P x ) → Q b {\displaystyle \left(\exists x\neg \neg Px\right)\to Qb}
Premissa
3.
P a {\displaystyle Pa}
Hipótese para E ∃ {\displaystyle {\mathcal {E}}\exists }
4.
¬ ¬ P a {\displaystyle \neg \neg Pa}
3 DN
5.
∃ x ¬ ¬ P x {\displaystyle \exists x\neg \neg Px}
4 I ∃ {\displaystyle {\mathcal {I}}\exists }
6.
Q b {\displaystyle Qb}
2,5 MP
7.
Q b {\displaystyle Qb}
1,3-5 E ∃ {\displaystyle {\mathcal {E}}\exists }
{ ∀ x ( A x → B x ) , ¬ ∃ ( B x ∧ C x ) } ⊢ ¬ ∃ x ( A x ∧ C x ) {\displaystyle \left\{\forall x\left(Ax\to Bx\right),\neg \exists \left(Bx\land Cx\right)\right\}\vdash \neg \exists x\left(Ax\land Cx\right)}
01.
∀ x ( A x → B x ) {\displaystyle \forall x\left(Ax\to Bx\right)}
Premissa
02.
¬ ∃ ( B x ∧ C x ) {\displaystyle \neg \exists \left(Bx\land Cx\right)}
Premissa
03.
∃ x ( A x ∧ C x ) {\displaystyle \exists x\left(Ax\land Cx\right)}
Hipótese
04.
A d ∧ C d {\displaystyle Ad\land Cd}
Hipotese para E ∃ {\displaystyle {\mathcal {E}}\exists }
05.
A d → B d {\displaystyle Ad\to Bd}
1 E ∀ {\displaystyle {\mathcal {E}}\forall }
06.
A d {\displaystyle Ad}
4 S
07.
B d {\displaystyle Bd}
5,6 MP
08.
C d {\displaystyle Cd}
4 S
09.
B d ∧ C d {\displaystyle Bd\land Cd}
7,8 C
10.
∃ x ( B x ∧ C x ) {\displaystyle \exists x\left(Bx\land Cx\right)}
9 I ∃ {\displaystyle {\mathcal {I}}\exists }
11.
∃ x ( B x ∧ C x ) {\displaystyle \exists x\left(Bx\land Cx\right)}
3,4-10 E ∃ {\displaystyle {\mathcal {E}}\exists }
12.
∃ x ( B x ∧ C x ) ∧ ¬ ∃ x ( B x ∧ C x ) {\displaystyle \exists x\left(Bx\land Cx\right)\land \neg \exists x\left(Bx\land Cx\right)}
11,2 C
13.
¬ ∃ x ( A x ∧ C x ) {\displaystyle \neg \exists x\left(Ax\land Cx\right)}
3,12 RAA
Demonstre:
{ ∀ x ( P x ∨ Q x ) , ¬ Q a } ⊢ P a {\displaystyle \left\{\forall x\left(Px\lor Qx\right),\neg Qa\right\}\vdash Pa}
{ ∀ x ( A x ∧ B x ) , ∀ x ( C x ∧ D x ) } ⊢ ∀ x ( A x ∧ C x ) {\displaystyle \left\{\forall x\left(Ax\land Bx\right),\forall x\left(Cx\land Dx\right)\right\}\vdash \forall x\left(Ax\land Cx\right)}
{ ∀ x ( A x → B x ) , A l } ⊢ ∃ x B x {\displaystyle \left\{\forall x\left(Ax\to Bx\right),Al\right\}\vdash \exists xBx}
∃ x ( P x ∧ Q x ) ⊢ ∃ x P x ∧ ∃ x Q x {\displaystyle \exists x\left(Px\land Qx\right)\vdash \exists xPx\land \exists xQx}
{ ∃ x P x , ∀ x Q x } ⊢ ∃ x ( P x ∧ Q x ) {\displaystyle \left\{\exists xPx,\forall xQx\right\}\vdash \exists x\left(Px\land Qx\right)} Confira aqui as respostas
A única regra derivada para quantificadores que trataremos aqui é o Intercâmbio de Quantificadores (IQ ):
¬ ∀ x α ∃ x ¬ α ¯ {\displaystyle {\frac {\neg \forall x\alpha }{\overline {\exists x\neg \alpha }}}} ¬ ∃ x α ∀ x ¬ α ¯ {\displaystyle {\frac {\neg \exists x\alpha }{\overline {\forall x\neg \alpha }}}} Vamos provar cada caso deste regra:
Intercâmbio de Quantificadores 1
editar
∀ x ¬ α ⊢ ¬ ∃ x α {\displaystyle \forall x\neg \alpha \vdash \neg \exists x\alpha }
1.
∀ x ¬ α {\displaystyle \forall x\neg \alpha }
Premissa
2.
¬ α ( c ) {\displaystyle \neg \alpha \left(\mathrm {c} \right)}
1 E ∀ {\displaystyle {\mathcal {E}}\forall }
3.
∃ x α {\displaystyle \exists x\alpha }
Hipótese
4.
α ( c ) {\displaystyle \alpha \left(\mathrm {c} \right)}
Hipótese para E ∃ {\displaystyle {\mathcal {E}}\exists }
5.
α ( c ) ∧ ¬ α ( c ) {\displaystyle \alpha \left(\mathrm {c} \right)\land \neg \alpha \left(\mathrm {c} \right)}
4,2 C
6.
∀ x ( α ∧ ¬ α ) {\displaystyle \forall x\left(\alpha \land \neg \alpha \right)}
5 I ∀ {\displaystyle {\mathcal {I}}\forall }
7.
∀ x ( α ∧ ¬ α ) {\displaystyle \forall x\left(\alpha \land \neg \alpha \right)}
3,4-6 E ∃ {\displaystyle {\mathcal {E}}\exists }
8.
α ( c ) ∧ ¬ α ( c ) {\displaystyle \alpha \left(\mathrm {c} \right)\land \neg \alpha \left(\mathrm {c} \right)}
7 E ∀ {\displaystyle {\mathcal {E}}\forall }
9.
¬ ∃ x α {\displaystyle \neg \exists x\alpha }
3,8 RAA
Intercâmbio de Quantificadores 2
editar
¬ ∃ x α ⊢ ∀ x ¬ α {\displaystyle \neg \exists x\alpha \vdash \forall x\neg \alpha }
1.
¬ ∃ x α {\displaystyle \neg \exists x\alpha }
Premissa
2.
α ( c ) {\displaystyle \alpha \left(\mathrm {c} \right)}
Hipótese
3.
∃ x α {\displaystyle \exists x\alpha }
2 I ∃ {\displaystyle {\mathcal {I}}\exists }
4.
∃ x α ∧ ¬ ∃ x α {\displaystyle \exists x\alpha \land \neg \exists x\alpha }
3,1 C
5.
¬ α ( c ) {\displaystyle \neg \alpha \left(\mathrm {c} \right)}
2,4 RAA
6.
∀ x ¬ α {\displaystyle \forall x\neg \alpha }
5 I ∀ {\displaystyle {\mathcal {I}}\forall }
Intercâmbio de Quantificadores 3
editar
¬ ∀ x α ⊢ ∃ x ¬ α {\displaystyle \neg \forall x\alpha \vdash \exists x\neg \alpha }
01.
¬ ∀ x α {\displaystyle \neg \forall x\alpha }
Premissa
02.
¬ ∃ x ¬ α {\displaystyle \neg \exists x\neg \alpha }
Hipótese
03.
¬ α ( c ) {\displaystyle \neg \alpha \left(\mathrm {c} \right)}
Hipótese
04.
∃ x ¬ α {\displaystyle \exists x\neg \alpha }
3 I ∃ {\displaystyle {\mathcal {I}}\exists }
05.
∃ x ¬ α ∧ ¬ ∃ x ¬ α {\displaystyle \exists x\neg \alpha \land \neg \exists x\neg \alpha }
2,4 C
06.
¬ ¬ α ( c ) {\displaystyle \neg \neg \alpha \left(\mathrm {c} \right)}
3,5 RAA
07.
α ( c ) {\displaystyle \alpha \left(\mathrm {c} \right)}
6 DN
08.
∀ x α {\displaystyle \forall x\alpha }
7 I ∀ {\displaystyle {\mathcal {I}}\forall }
09.
∀ x α ∧ ¬ ∀ x α {\displaystyle \forall x\alpha \land \neg \forall x\alpha }
1,8 C
10.
¬ ¬ ∃ x ¬ α {\displaystyle \neg \neg \exists x\neg \alpha }
2,9 RAA
11.
∃ x ¬ α {\displaystyle \exists x\neg \alpha }
10 DN
Intercâmbio de Quantificadores 4
editar
∃ x ¬ α ⊢ ¬ ∀ x α {\displaystyle \exists x\neg \alpha \vdash \neg \forall x\alpha }
1.
∃ x ¬ α {\displaystyle \exists x\neg \alpha }
Premissa
2.
¬ α ( c ) {\displaystyle \neg \alpha \left(\mathrm {c} \right)}
Hipótese E ∃ {\displaystyle {\mathcal {E}}\exists }
3.
∀ x α {\displaystyle \forall x\alpha }
Hipótese
4.
α ( c ) {\displaystyle \alpha \left(\mathrm {c} \right)}
3 E ∀ {\displaystyle {\mathcal {E}}\forall }
5.
α ( c ) ∧ ¬ α ( c ) {\displaystyle \alpha \left(\mathrm {c} \right)\land \neg \alpha \left(\mathrm {c} \right)}
2,4 C
6.
¬ ∀ x α {\displaystyle \neg \forall x\alpha }
3,5 RAA
7.
¬ ∀ x α {\displaystyle \neg \forall x\alpha }
1,2-6 E ∃ {\displaystyle {\mathcal {E}}\exists }
Aplicando o Intercâmbio de Quantificadores
editar
Segue abaixo alguns exemplos que ilustram o quanto a regra de intercâmbio de quantificadores é útil.
⊢ ∃ x ( P x ∨ Q x ) → ( ∃ x P x ∨ ∃ x Q x ) {\displaystyle \vdash \exists x\left(Px\lor Qx\right)\to \left(\exists xPx\lor \exists xQx\right)}
01.
∃ x ( P x ∨ Q x ) {\displaystyle \exists x\left(Px\lor Qx\right)}
Hipótese
02.
¬ ( ∃ x P x ∨ ∃ x Q x ) {\displaystyle \neg \left(\exists xPx\lor \exists xQx\right)}
Hipótese
03.
¬ ∃ x P x ∧ ¬ ∃ x Q x {\displaystyle \neg \exists xPx\land \neg \exists xQx}
2 DM
04.
¬ ∃ x P x {\displaystyle \neg \exists xPx}
3 S
05.
¬ ∃ x Q x {\displaystyle \neg \exists xQx}
3 S
06.
∀ x ¬ P x {\displaystyle \forall x\neg Px}
4 IQ
07.
∀ x ¬ Q x {\displaystyle \forall x\neg Qx}
5 IQ
08.
¬ P a {\displaystyle \neg Pa}
6 E ∀ {\displaystyle {\mathcal {E}}\forall }
09.
¬ Q a {\displaystyle \neg Qa}
7 E ∀ {\displaystyle {\mathcal {E}}\forall }
10.
¬ P a ∧ ¬ Q a {\displaystyle \neg Pa\land \neg Qa}
8,9 C
11.
¬ ( P a ∨ Q a ) {\displaystyle \neg \left(Pa\lor Qa\right)}
10 DM
12.
∀ x ¬ ( P x ∨ Q x ) {\displaystyle \forall x\neg \left(Px\lor Qx\right)}
11 I ∀ {\displaystyle {\mathcal {I}}\forall }
13.
¬ ∃ x ( P x ∨ Q x ) {\displaystyle \neg \exists x\left(Px\lor Qx\right)}
12 IQ
14.
∃ x ( P x ∨ Q x ) ∧ ¬ ∃ x ( P x ∨ Q x ) {\displaystyle \exists x\left(Px\lor Qx\right)\land \neg \exists x\left(Px\lor Qx\right)}
1,13 C
15.
¬ ¬ ( ∃ x P x ∨ ∃ x Q x ) {\displaystyle \neg \neg \left(\exists xPx\lor \exists xQx\right)}
2,14 RAA
16.
∃ x P x ∨ ∃ x Q x {\displaystyle \exists xPx\lor \exists xQx}
15 DN
17.
∃ x ( P x ∨ Q x ) → ( ∃ x P x ∨ ∃ x Q x ) {\displaystyle \exists x\left(Px\lor Qx\right)\to \left(\exists xPx\lor \exists xQx\right)}
1,16 RPC
⊢ ( ∃ x P x ∨ ∃ x Q x ) → ∃ x ( P x ∨ Q x ) {\displaystyle \vdash \left(\exists xPx\lor \exists xQx\right)\to \exists x\left(Px\lor Qx\right)}
01.
∃ x P x ∨ ∃ x Q x {\displaystyle \exists xPx\lor \exists xQx}
Hipótese
02.
¬ ∃ x ( P x ∨ Q x ) {\displaystyle \neg \exists x\left(Px\lor Qx\right)}
Hipótese
03.
∀ x ¬ ( P x ∨ Q x ) {\displaystyle \forall x\neg \left(Px\lor Qx\right)}
2 IQ
04.
¬ ( P a ∨ Q a ) {\displaystyle \neg \left(Pa\lor Qa\right)}
3 E ∀ {\displaystyle {\mathcal {E}}\forall }
05.
¬ P a ∧ ¬ Q a {\displaystyle \neg Pa\land \neg Qa}
4 DM
06.
¬ ∃ x P x {\displaystyle \neg \exists xPx}
Hipótese
07.
∃ x Q x {\displaystyle \exists xQx}
1,6 SD
08.
¬ Q a {\displaystyle \neg Qa}
5 S
09.
∀ x ¬ Q x {\displaystyle \forall x\neg Qx}
8 I ∀ {\displaystyle {\mathcal {I}}\forall }
10.
¬ ∃ x Q x {\displaystyle \neg \exists xQx}
9 IQ
11.
∃ x Q x ∧ ¬ ∃ x Q x {\displaystyle \exists xQx\land \neg \exists xQx}
6,10 C
12.
¬ ¬ ∃ x P x {\displaystyle \neg \neg \exists xPx}
6,11 RAA
13.
∃ x P x {\displaystyle \exists xPx}
12 DN
14.
¬ P a {\displaystyle \neg Pa}
5 S
15.
∀ x ¬ P x {\displaystyle \forall x\neg Px}
14 I ∀ {\displaystyle {\mathcal {I}}\forall }
16.
¬ ∃ x P x {\displaystyle \neg \exists xPx}
15 IQ
17.
∃ x P x ∧ ¬ ∃ x P x {\displaystyle \exists xPx\land \neg \exists xPx}
13,16 C
18.
¬ ¬ ∃ x ( P x ∨ Q x ) {\displaystyle \neg \neg \exists x\left(Px\lor Qx\right)}
2,17 RAA
19.
∃ x ( P x ∨ Q x ) {\displaystyle \exists x\left(Px\lor Qx\right)}
18 DN
20.
( ∃ x P x ∨ ∃ x Q x ) → ∃ x ( P x ∨ Q x ) {\displaystyle \left(\exists xPx\lor \exists xQx\right)\to \exists x\left(Px\lor Qx\right)}
1,19 RPC
{ ∀ x ( A x → B x ) , ∀ x ( A x → ¬ B x ) } ⊢ ¬ ∃ A x {\displaystyle \left\{\forall x\left(Ax\to Bx\right),\forall x\left(Ax\to \neg Bx\right)\right\}\vdash \neg \exists Ax}
01.
∀ x ( A x → B x ) {\displaystyle \forall x\left(Ax\to Bx\right)}
Premissa
02.
∀ x ( A x → ¬ B x ) {\displaystyle \forall x\left(Ax\to \neg Bx\right)}
Premissa
03.
A d {\displaystyle Ad}
Hipótese
04.
A d → B d {\displaystyle Ad\to Bd}
1 E ∀ {\displaystyle {\mathcal {E}}\forall }
05.
A d → ¬ B d {\displaystyle Ad\to \neg Bd}
4 E ∀ {\displaystyle {\mathcal {E}}\forall }
06.
B d {\displaystyle Bd}
3,4 MP
07.
¬ B d {\displaystyle \neg Bd}
3,5 MP
08.
B d ∧ ¬ B d {\displaystyle Bd\land \neg Bd}
6,7 C
09.
¬ A d {\displaystyle \neg Ad}
3,8 RAA
10.
∀ x ¬ A x {\displaystyle \forall x\neg Ax}
9 I ∀ {\displaystyle {\mathcal {I}}\forall }
11.
¬ ∃ x A x {\displaystyle \neg \exists xAx}
10 IQ