Proofs and term models

Exercise 1. For the following proof tasks:

(1) ∀(x | A(x) ⇒ B(x)) ⊢ ∀(x | A(x)) ⇒ ∀(x | B(x)),

(2) ∀(x | A(x)) ⇒ ∀(x | B(x)) ⊢ ∀(x | A(x) ⇒ B(x)),

(3) A(x) ⇒ ∀(x | B(x)) ⊢ ∃(x | A(x)) ⇒ ∀(x | B(x)),

(4) ∃(x | A(x)) ⇒ ∀(x | B(x)) ⊢ A(x) ⇒ ∀(x | B(x)), find proofs, if it is possible. Otherwise, find counterexamples. Exercise 2. We have given an alphabet Σ = {a, f, g, P, Q} where a is an individual constant, f and g are unary function symbols and P, Q are unary relation symbols. We have also the theory Γ = {P (a), ∀(x | P (x) ⇒ P (f(x))), ∀(x | Q(x) ⇒ Q(f(x))), ∀(x | Q(g(x))), ∀(x | ¬(P (x) ∧ Q(x)))}.

(1) Describe ground Σ-terms (give an inductive definition).

(2) Explain why we will have that Γ ⊧ P (t) ∨ Q(t) for any ground term t. Hint: It is easiest to show this by induction on the structure of the ground terms.

(3) Describe a term model that satisfies Γ.

(4) We do not have Γ ⊧ ∀(x | P (x) ∨ Q(x)).

Justify this by providing a model for Γ which is not a model for ∀(x | P (x) ∨ Q(x)).