Ax(Fx) |- Fa UQ elim
Ax(Fx -> Gx) |- Fa -> Ga
UQ
elim
Fa |- Ex(Fx) EQ int
Fa & Ga |- Ex(Fx & Gx)
EQ int
restricted use
inferences
Fa |- Ax(Fx) UQ int
Fa -> Ga |- Ax(Fx -> Gx) UQ int
(only when the name has not been assumed,
except when the assumption is discharged)
Ex(Fx) |- Fa EQ elim (x=a)
(only when the name has not been previously
used or is to be part of the conclusion)
click on the link above for a more complete
explanation of these restrictions
equivalences
(can be used anywhere inside a wff)
p
= ~~p DN
p & q = q & p
& comm
p v q = q v p
v comm
p & (q & r) = (p &
q) & r & assoc
p v (q v r) = (p v q) v r
v assoc
p & (q v r) = (p & q) v (p
& r) Distrib
p v (q & r) = (p v q) & (p
v r) Distrib
p -> q = ~q -> ~p
Contra
p -> q = ~p v q
MI
~(p & q) = ~p v ~q
DeM
~(p v q) = ~p & ~q
DeM
~Ax(Fx) = Ex(~Fx) QN
~Ax(~Fx) = Ex(Fx) QN
~Ex(Fx) = Ax(~Fx) QN
~Ex(~Fx) = Ax(Fx) QN