Resolution proof: contradicting premises, what exactly can we conclude?

30 Views Asked by At

Doing a proof by contradiction and resolution with the following premises:

1) ∀P,S ∶ Born(P,S) -> Home(P,S)

2) ∀X ∶ Person(X) -> Walks(X)

3) Born(Mike,NY)

4) Born(John,CA)

5) Person(John)

6) ¬Walks(John)

Prove by contradiction that Home(Mike, CA).

I know to negate the desired conclusion and I know to put the first two premises in disjunctive form:

¬Person(X) ∨ Walks(X) AND

¬Born(P,S) ∨ Home(P,S)

Where I run into trouble is with the contradicting premises. If John is a person then he should be able to walk. We could resolve the first of the disjunctive sentences with Person(John) to get Walks(John), but this directly contradicts the last premise ¬Walks(John).

I've looked online at the "Principle of Explosion" which states that if P and ¬P both exist (ie, inconsistent or contradicting premises), then a separate Q is true. I don't know how I could possibly use these contradicting premises though to prove that Mike's home is somehow CA when he was born in NY.

Am I on the right track with the principle of explosion, or are there other things I can resolve here that I am just not seeing?