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} }
x
{\displaystyle x}
α
{\displaystyle \alpha }
c
{\displaystyle \mathrm {c} }
α
{\displaystyle \alpha }
x
{\displaystyle x}
c
{\displaystyle \mathrm {c} }
x
{\displaystyle x}
α
{\displaystyle \alpha }
.
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 }
α
{\displaystyle \alpha }
x
{\displaystyle x}
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}
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 }
c
{\displaystyle \mathrm {c} }
∀
x
α
{\displaystyle \forall x\alpha }
c
{\displaystyle \mathrm {c} }
x
{\displaystyle x}
a constante
c
{\displaystyle \mathrm {c} }
.
c
{\displaystyle \mathrm {c} }
x
{\displaystyle x}
α
{\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 }
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 }
c
{\displaystyle \mathrm {c} }
∃
x
α
{\displaystyle \exists x\alpha }
c
{\displaystyle \mathrm {c} }
x
{\displaystyle x}
c
{\displaystyle \mathrm {c} }
x
{\displaystyle x}
α
{\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.
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 }
α
{\displaystyle \alpha }
x
{\displaystyle x}
c
{\displaystyle \mathrm {c} }
β
{\displaystyle \beta }
β
{\displaystyle \beta }
a constante
c
{\displaystyle \mathrm {c} }
α
{\displaystyle \alpha }
β
{\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:
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
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 }
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
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 }
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
![{\displaystyle {\frac {\forall x(\alpha )}{\alpha \left[x/\mathrm {c} \right]}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0b07911997f605a08c7121b5079a47a4a1884c0b)
