Predicate Calculus Proofs (1)

Pr1.) x does not occur free in P, ∀x(P ⇒ Q) ⊨ P ⇒ ∀x(Q)
1.)  ⊨ ∀x(P ⇒ Q)                                                                       Hyp
2.)  ⊨ [∀x (P ⇒ Q)] ⇒ {P ⇒ [∀x(Q)]}                                      Z5
3.)  ⊨ P ⇒ ∀x(Q)                                                                       MP 1,2

Pr2.) ⊨ ∃x(P) ⇔ [¬∀x(¬P)]
1.) ⊨ ¬∃x(P) ⇔ ∀x(¬P)                                              Z6
2.) ⊨ ¬[¬∃x(P)] ⇔ ¬∀x(¬P)                                     Th53
3.) ⊨ ¬∀x(¬P) ⇔ ¬[¬∃x(P)]                                     Th41
4.) ⊨ ¬[¬∃x(P)] ⇔ ∃x(P)                                          Th49
5.) ⊨ ¬∀x(¬P) ⇔ ∃x(P)                                             Th42
6.) ⊨  ∃x(P) ⇔ ¬∀x(¬P)                                            Th41

Pr3.) ⊨ ∀x(P) ⇔ [¬∃x(¬P)]
1.) ⊨ [¬∀x(P)] ⇔ ∃X(¬P)                        Z7
2.) ⊨ {¬[¬∀x(P)]} ⇔ [¬∃X(¬P)]            Th53
3.) ⊨  [¬∃X(¬P)] ⇔ {¬[¬∀x(P)]}            Th41
4.) ⊨ {¬[¬∀x(P)]} ⇔ ∀x(P)                     Th49
5.) ⊨ [¬∃X(¬P)] ⇔ ∀x(P)                        Th42
6.) ⊨ ∀x(P) ⇔ [¬∃X(¬P)]                        Th41

Pr4.) ⊨  ∀x(P ⇒ Q) ⇒ [∀x(P) ⇒ Q]

1.) ⊨ ∀x(P ⇒ Q) ⇒ (P ⇒ Q)                      Z4

2.) ⊨ ∀x(P) ⇒ P                                         Z4
3.) ⊨ ∀x(P ⇒ Q) ⇒ [∀x(P) ⇒ Q]              Th13