You should now Launch Deriver and do the 1 exercises of Predicate Exercise 15 (Predex15).
Most experienced logicians are pretty familiar with the following theorems. Although the theorems are stated in terms of Fx and Gx etc. most of them hold of most formulas. Derive them
a) ∴ ((∀x)F)≡F
(*this is true for any formula F provided that x is not free in F*)
b) ∴ ((∀x)Fx)≡((∀y)Fy)
(*change of variables*)
c) ∴ ((∀x)(∀y)Fxy)≡((∀y)(∀x)Fxy)
(*permuting universal quantifiers*)
d) ∴ ((∃x)(∃y)Fxy)≡((∃y)(∃x)Fxy)
(*permuting existential quantifiers*)
e) ∴ ((∃x)(∀y)Fxy)⊃((∀y)(∃x)Fxy)
f) Note that the following is not a theorem, see if you can produce a counter example
∴((∀y)(∃x)Fxy)⊃((∃x)(∀y)Fxy)
(*this is the 'everything has a cause therefore some (one) thing is the cause of everything' fallacy*)
g) ∴ ((∃x)Fx)≡(∼(∀x)∼Fx)
(*equivalence of connectives*)
h) ∴ (∼(∃x)∼Fx)≡((∀x)Fx)
(*equivalence of connectives*)
i) ∴ (∀x)(Fx≡Gx)⊃((∀x)Fx≡(∀x)Gx)
(*but j) note that (or prove that)
∴(∀x)(Fx≡Gx)≡((∀x)Fx≡(∀x)Gx)
is invalid*)
k) ∴ (∀x)(Fx≡Gx)⊃((∃x)Fx≡(∃x)Gx)
l) ∴ (∀x)(Fx⊃Gx)⊃((∀x)Fx⊃(∀x)Gx)
m) ∴ (∀x)(Fx⊃Gx)⊃((∃x)Fx⊃(∃x)Gx)
n) ∴ ((∀x)Fx⊃(∀x)Gx)⊃(∃x)(Fx⊃Gx)
o) ∴ (∀x)(Fx∧Gx)≡((∀x)Fx∧(∀x)Gx)
p) ∴ (∀x)(Fx∨Gx)⊃((∀x)Fx∨(∃x)Gx)
q) ∴ ((∀x)Fx∨(∀x)Gx)⊃(∀x)(Fx∨Gx)
r) ∴ ((∃x)Fx∨(∃x)Gx)≡(∃x)(Fx∨Gx)