Exercise set #1, 1st-order [Jun 6, 2012]

• These are the most bascic problems. Construct a Fitch derivation for the following.
① ∀x(A(x) → B(x)), A(c) ├ B(c) (Hint: There's no need for new lines. Just give a suitable annotation. If you do not use extended inference rules and stick to the primitive rules, then you should insert a line.)
② ∀x(A(x) → B(x)), ¬B(c) ├ ¬A(c)
③ ∀x(A(x) → B(x)), ∃x A(x)├ ∃x B(x) (Hint: Use ∃-elim rule.)
④ ∀x(A(x) ∨ B(x)), ∃x¬A(x)├ ∃x B(x)
⑤ ∀x(A(x) → B(x)), ∀x A(x)├ ∀x B(x)
⑥ ∃x(A(x) → B(x)), ∀x A(x)├ ∃x B(x)
• Show that neither of the two proof relation holds. (Hint: For each proof relation, you should construct a model that serves as a counterexample.)
∃x(A(x) → B(x)), ∃x A(x)├ ∃x B(x)
∃x(A(x) → B(x)), A(c)├ B(c)
• ∀x(∃y R(x,y) → P(x) ∨ ∀z R(z,x)), ¬(R(d,a) → R(c,d)) ├ ∃x P(x)
Hint: Here is a half-done proof. [ @x(#y R(x,y) \$ P(x) | @z R(z,x)) ; ~(R(d,a) \$ R(c,d)) entails #y R(d,y) \$ P(d) | @z R(z,d) :Rule ? ; R(d,a) :Rule ? ; ~R(c,d) :Rule ? ; #y R(d,y) :Rule ? ; P(d) | @z R(z,d) :Rule ? ; #z~R(z,d) :Rule ? ; ~@z R(z,d) :demorgan 8 ; P(d) :Rule ? ; #x P(x) :Rule ? ] !line_cnc11
• ∀x(A(x) ∧ ∃y R(x,y) → B(x)), ∀x(B(x) → C(x)), ∀x(B(x) ∨ R(x,x)) ├ ∀x(A(x) → C(x))
Hint: [ @x(A(x) & #y R(x,y) \$ B(x)) ; @x(B(x) \$ C(x)) ; @x(B(x) | R(x,x)) entails [ {c} entails [ A(c) entails B(c) | R(c,c) :Rule ? ;[ B(c) entails C(c) :@ elim 2,7 ] ;[ R(c,c) entails #y R(c,y) :# intro 9 ; :Rule ? ; B(c) :tautcnsq 5,10,11 ; C(c) :Rule ? ] ; C(c) :Rule ? ] ] ; @x(A(x) \$ C(x)) :@ intro 4,5-14 ] !line_cnc15
• ∃x A(x) ∧ ¬∃x B(x)├ ∃x(A(x) ∧ ¬B(x))
Hint: If you replace the hypothesis with x A(x) ∧ ∃x¬B(x), this├ relation doesn't hold. Why? You should use the DeMorgan extended rule at one place.