3

How would a formal Fitch proof look like. I am given P(a) → ∀x(P(x) ∨ ¬(x = a)) to prove using Natural Deduction of predicate logic. I am confused on how to proceed with the proof. Please advice me on how to go about with this.

Thanks in advance

Moey mnm
  • 47
  • 4

1 Answers1

4

HINT: I'll sketch the derivation. Since the theorem is a conditional, try using conditional proof/conditional-introduction by assuming P(a) and trying to derive ∀x(P(x) ∨ ¬(x = a)) from it. Here, to derive it, I would try an indirect proof by assuming the negation ¬∀x(P(x) ∨ ¬(x = a)) and trying to derive a contradiction. Use quantifier equivalence rules to get ∃x¬(P(x) ∨ ¬(x = a)).

The next steps will be a little different depending on your list of rules (quantifier rules typically come with restrictions to ensure the rules are sound, and different texts will use different restrictions). Roughly, we can let y be the individual such that ¬(P(y) ∨ ¬(y = a)). Apply De Morgan's law to get ¬P(y) ∧ (y = a). Since y = a, it must be that ¬P(a), contradicting our assumption that P(a). Hence our contradiction completing the indirect proof of ∀x(P(x) ∨ ¬(x = a)).

Hope this helps!

Adam Sharpe
  • 3,764
  • 2
  • 9
  • 35
  • 1
    Just as confirmation, your suggestion for how to proceed worked using the following proof checker: http://proofs.openlogicproject.org/ – Frank Hubeny Apr 03 '19 at 02:44
  • Alternatively (but similar): assume for some arbitrary term (c) that `¬(P(x) ∨ ¬(x = a))` aiming to derive a contradiction, so you may then *introduce the universal* quantifier to deduce: `∀x (P(x) ∨ ¬(x = a))`. No need to use quantifier duality equivalences. – Graham Kemp Sep 04 '19 at 22:45