I was reading Code by Charles Petzold, and on page 86 he references a syllogism from Lewis Carroll:
- All philosophers are logical;
- An illogical man is always obstinate;
- Therefore, some obstinate persons are not philosophers.
I formalized this argument in predicate logic as follows:
- Let P(x) be the propositional function "x is a philosopher".
- Let L(x) be the propositional function "x is logical".
- Let O(x) be the propositional function "x is obstinate".
Then the premises become:
- ∀x(P(x) → L(x)), and
- ∀x(~L(x) → O(x)), respectively.
The conclusion is:
- ∃x(O(x) & ~P(x)).
I attempted deriving this conclusion, but was unable to. I then wondered if a derivation was at all possible, and used prover9 to find a proof, but the result was negative (which could mean that my input was invalid).
I then added an additional premise, ∃x~L(x) (there is at least one illogical person), and was easily able to derive the conclusion:
- ∀x(P(x) → L(x)) (premise)
- ∀x(~L(x) → O(x)) (premise)
- ∃x~L(x) (premise)
- ~L(c) (EI from 3)
- ~L(c) → O(c) (UI from 2)
- P(c) → L(c) (UI from 1)
- ~L(c) → ~P(c) (contrapositive of 6)
- O(c) (MP 4 and 5)
- ~P(c) (MP 4 and 7)
- O(c) & ~P(c) (conjunction of 8 and 9)
- ∃x(O(x) & ~P(x)) (EG of 10)
My question then is: are the original premises sufficient for deriving the conclusion, or is the additional premise necessary?