An Axiomatic Proof
Posted: Mon Jan 19, 2015 4:22 am
I've been trying to find a proof since last night, and I just can't seem to do it. The proposition I'm trying to prove is '~((~P → Q) → Q) → P'.
Now, of course, I've checked and this proposition is a tautology, so it must be a theorem that can be proved.
I'm using the following three axioms:
P1. a → (b → a)
P2. (a → (b → c)) → ((a → b) → (a → c))
P3. (~a → ~b) → ((~a → b) → a)
And the usual Modus Ponens (MP) inference.
I tried a few things, most recently I attempted something like this:
I would get '(P → P)' like this:
1. P → ((P → P) → P) [P1]
2. P → (P → P) [P1]
3. (P → ((P → P) → P)) → ((P → (P → P)) → (P → P)) [P2]
4. (P → (P → P)) → (P → P) [1, 3, MP]
5. (P → P) [2, 4, MP]
Then I would get to '~(~((~P → Q) → Q) → P) → (P → P)':
6. (P → P) → (~(~((~P → Q) → Q) → P) → (P → P)) [P1]
7. ~(~((~P → Q) → Q) → P) → (P → P) [5, 6, MP]
Now that I'd shown that the negation of '~((~P → Q) → Q) → P' implies '(P → P)', my plan was to then show that the negation of
'~((~P → Q) → Q) → P' also implies '~(P → P)'. If I can do this, then I can use [P3] to prove '~((~P → Q) → Q) → P'. But I just can't find a way to show that ~(~((~P → Q) → Q) → P) → ~(P → P), in spite of the fact that such a conditional must be true as both its antecedent and its consequent are always false.
If you can find another way to prove it, then please do by all means. Though I would greatly prefer if you could somehow "complete" what I've already done so far by showing that ~(~((~P → Q) → Q) → P) → ~(P → P).
Thank you so much, reply soon!
-egg3000
P.S. It's probably something absurdly simple, and I'll feel stupid for having missed it.
Now, of course, I've checked and this proposition is a tautology, so it must be a theorem that can be proved.
I'm using the following three axioms:
P1. a → (b → a)
P2. (a → (b → c)) → ((a → b) → (a → c))
P3. (~a → ~b) → ((~a → b) → a)
And the usual Modus Ponens (MP) inference.
I tried a few things, most recently I attempted something like this:
I would get '(P → P)' like this:
1. P → ((P → P) → P) [P1]
2. P → (P → P) [P1]
3. (P → ((P → P) → P)) → ((P → (P → P)) → (P → P)) [P2]
4. (P → (P → P)) → (P → P) [1, 3, MP]
5. (P → P) [2, 4, MP]
Then I would get to '~(~((~P → Q) → Q) → P) → (P → P)':
6. (P → P) → (~(~((~P → Q) → Q) → P) → (P → P)) [P1]
7. ~(~((~P → Q) → Q) → P) → (P → P) [5, 6, MP]
Now that I'd shown that the negation of '~((~P → Q) → Q) → P' implies '(P → P)', my plan was to then show that the negation of
'~((~P → Q) → Q) → P' also implies '~(P → P)'. If I can do this, then I can use [P3] to prove '~((~P → Q) → Q) → P'. But I just can't find a way to show that ~(~((~P → Q) → Q) → P) → ~(P → P), in spite of the fact that such a conditional must be true as both its antecedent and its consequent are always false.
If you can find another way to prove it, then please do by all means. Though I would greatly prefer if you could somehow "complete" what I've already done so far by showing that ~(~((~P → Q) → Q) → P) → ~(P → P).
Thank you so much, reply soon!
-egg3000
P.S. It's probably something absurdly simple, and I'll feel stupid for having missed it.