1. Let L = {f,g,R,S, c} where f is a unary function symbol,g is a binary function symbol, R is a binary relation symbol, S is a ternary relation symbol, and c is a constant symbol.  Show that each of the following L-formulas are axioms of our proof system.

(a)  (Rx1 x2  → (Scx1 x2  → Rx1 x2 ))

(b)  (Ax2 ∃x3 fx2  ≈ x3  → ∃x3 fgcx1  ≈ x3 )

(c) Ax7Ax3 (Ax1 (∃x7 Rcx7  → Sx1 x7 c) → (Ax1 ∃x7 Rcx7  → Ax1 Sx1 x7 c))

(d) Ax3Ax1Ax4 (x2  ≈ x5  → (gx2 x1  ≈ x5  → gx5 x1  ≈ x5 ))

2.  Let x, y, and z denote first order variables.

(a) Provide the justifications for each line of the following derivation, which shows that {x ≈ y} ⊢ y ≈ x.

(1)   x ≈ y

(2)   x ≈ x

(3)   (x ≈ y → (x ≈ x → y ≈ x))

(4)   (x ≈ x → y ≈ x)

(5)   y ≈ x

(b)  Show that ⊢ (x ≈ y → y ≈ x), without appealing to the Com- pleteness Theorem.

(c)  Show that {x ≈ y, y  ≈ z} ⊢ x ≈ z, without appealing to the Completeness Theorem.