Logic 1, WS 2007. Homework 4, given Nov 8, due Nov 15.

1. Show how to transform a sequent which has an universally quantified formula in the goal, by moving the quantifier in front of the sequent (analoguous to the transformation of the sequent which has an existentially quantified formula in the assumptions, which was shown during the lecture).

2. For the inference rule for the sequents having an existentially quantified formula in the goal, prove the equivalence of the two sequents using the definition of the semantics.

3. For the inference rule for the sequents having an existentially quantified formula in the goal, prove the equivalence of the two sequents using the rule for the universal goal in the assumptions and the appropriate propositional rules.

4. Prove by definition that

P [a], ∀_{x}(P [x] ⇒ P [f[x]]) ⊧ P [f[f[a]]].