THE PROOF!!!!
"If Pat Garrett didn't shoot Billy the Kid, then somebody else did."
No Repetition Needed
The IF-THEN statement we used is:
"If Pat Garrett didn't shoot Billy the Kid, then someone else did."
... can be expressed in "Loglish" as:
"If Pat Garrett didn't shoot Billy the Kid, then there exist some x such that x did shoot Billy"
... which symbolically is:
| ¬S("Pat", "Billy") | → | ∃x:S(x, "Billy") |
We note that the consequent of the formula, ∃x:S(x, "Billy"), does not specifically state that the person who shot Billy was not Pat. The claim,though, is that the antecedent, ¬S("Pat", "Billy") precludes that possibility.
Now if you aren't convinced, there are two ways to specifically include the idea that the "x that shot Billy" was not Pat.
First you use the concept of identity. That is, you use the "equals" sign, =, with a conjunction - "and" (∧) - with the consequent.
| ¬S("Pat", "Billy") | → | ∃x:S(x, "Billy") ∧ ¬(x = "Pat") |
But identity is a whole new concept. To keep things simple we will eschew adopting this system, called First Order Logic With Identity.
Instead for the consequent we'll say that there is some x who shot Billy and Pat did not shoot Billy.
| ¬S("Pat", "Billy") | → | ∃x:[S(x, "Billy") ∧ ¬S("Pat", "Billy") |
So this is clear and definite.
But the question now is were we right the first time. That is, can we forget the second S("Pat", "Billy")?
Well, of course we wouldn't be writing this if we couldn't. And so we can provide the formal proof that our original and simpler formula was all we need. If anything seems to be uncertain, you can check with an elementary logic textbook.
| Step | Formula | Explanation | ||||
| 1 | ¬S("Pat", "Billy") → ∃x:S(x, "Billy") ∧ ¬S("Pat", "Billy") | If Pat did not shoot Billy, then there exists some x such that x did not shoot Billy and Pat did not shoot Billy. | ||||
| 2 | ¬[¬S("Pat", "Billy")] ∨ [∃x:S(x, "Billy") ∧ ¬S("Pat", "Billy")] | "IF-THEN" = "NOT-OR" A → B ≡ ¬A ∨ B | ||||
| 3 | ¬¬S("Pat", "Billy") ∨ [∃x:S(x, "Billy") ∧ ¬S("Pat", "Billy")] | Remove Unnecessary Parentheses ¬[¬A] ≡ ¬¬A | ||||
| 4 | S("Pat", "Billy") ∨ [∃x:S(x, "Billy") ∧ ¬S("Pat", "Billy")] | Two "NOTS" Cancel ¬¬A ≡ A | ||||
| 5 | [S("Pat", "Billy") ∨ ∃x:S(x, "Billy")] ∧ [S("Pat", "Billy") ∨ ¬S("Pat", "Billy")] | De Morgan's Law A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C) | ||||
| 6 | [S("Pat", "Billy") ∨ ∃x:S(x, "Billy")] ∧ TRUE | Tautology A or ¬A ≡ TRUE | ||||
| 7 | [S("Pat", "Billy") ∨ ∃x:S(x, "Billy")] | Tautology Elimination A ∧ TRUE ≡ A | ||||
| 7 | ¬S("Pat", "Billy") → ∃x:S(x, "Billy") | "OR" Equals "IF NOT-THEN" A ∨ B ≡ ¬A → B Q(uid) E(rat) D(emonstrandum) |
So you don't need the second ∃S("Pat", "Billy") and so:
| ¬S("Pat", "Billy") → ∃x:S(x, "Billy") ∧ ¬S("Pat", "Billy") | ≡ | ¬S("Pat", "Billy") → ∃x:S(x, "Billy") |
How about that?