An Axiomatic Proof

[egg3000]

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.

[Arising_uk]

Hi egg3000,

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 could be wrong as its been a long time but I don't think this, ~((~P → Q) → Q) → P)), is a tautology as its false when P and Q are true? Its also false when P is true and Q is false and when both are false. I think it can be deduced tho' as its true when P is false and Q is true but I haven't done this in a long time and to my shame I've forgotten how and my logic books are in storage so I'll have to get back to you.

[egg3000]

Hi Arising_uk, thanks for replying,

I could be wrong as its been a long time but I don't think this, ~((~P → Q) → Q) → P)), is a tautology

'~((~P → Q) → Q) → P))' is not technically a well-formed formula, as the furthermost two parentheses on the right (just after 'P') do not have matching left parentheses. I think you might have meant '~(((~P→Q)→Q)→P)', and indeed '~(((~P→Q)→Q)→P)' is not a tautology, which therefore means that it cannot be proved (if a proposition can be proved from axioms, then it is a theorem and must be a tautology). However, '~(((~P→Q)→Q)→P)' is not the proposition I am trying to prove; I'm trying to prove '~((~P → Q) → Q) → P'. In your proposition, '~(((~P→Q)→Q)→P)', the entire conditional is negated; in my proposition, '~((~P → Q) → Q) → P', only the antecedent of the conditional is negated.

-Egg3000

[Arising_uk]

Damn those pesky brackets.

'~((~P → Q) → Q) → P))' is not technically a well-formed formula, as the furthermost two parentheses on the right (just after 'P') do not have matching left parentheses. I think you might have meant '~(((~P→Q)→Q)→P)', and indeed '~(((~P→Q)→Q)→P)' is not a tautology, ...

That was the proposition I was assuming.

which therefore means that it cannot be proved (if a proposition can be proved from axioms, then it is a theorem and must be a tautology). However, '~(((~P→Q)→Q)→P)' is not the proposition I am trying to prove; ...

I'm interested in this as I'd either forgotten or not understood it the first time, are you saying that if there is a valuation in a truth table that makes a proposition true but its not a tautology then Natural Deduction cannot prove it? I find this unsatisfying in some way, is it a problem with the rules or a rule? Would you consider tableau methods axiomatic? And does the same problem apply to them?

I'm trying to prove '~((~P → Q) → Q) → P'. In your proposition, '~(((~P→Q)→Q)→P)', the entire conditional is negated; in my proposition, '~((~P → Q) → Q) → P', only the antecedent of the conditional is negated.

Given what you've said I think your problem is that is also not a tautology as isn't it false when P and Q are false?

[HexHammer]

So, all this amazing tautology, why don't we just use machines to determined if the criminal at a police investigation is telling the truth or not, or a witness in a court is telling the truth too?

..well, we can't! Simple as that, you can't define truth by tautology, it's simply superstition!

[egg3000]

I'm interested in this as I'd either forgotten or not understood it the first time, are you saying that if there is a valuation in a truth table that makes a proposition true but its not a tautology then Natural Deduction cannot prove it?

Natural deduction is a different kind of proof method to the sort of axiomatic proofs I'm referring to. Nevertheless, natural deduction can only prove a proposition (in the sense that the proposition in question lies outside of the scope of any assumptions) if that proposition is a tautology. For example, if you were to assume 'P∧~P' as the first line in a natural deduction proof, then you could use the elimination rule for '∧' to show that 'P' and '~P', but only under the assumption of 'P∧~P'. Hence, you can show that P∧~P ⊢ P, and you can show that P∧~P ⊢ ~P, but it is not possible to show that ⊢P by itself or ⊢~P by itself. On the other hand, a proposition such as '(P∧~P)→Q' is a tautology, and so you can indeed use natural deduction to prove that ⊢(P∧~P)→Q. It's not a problem with any of the rules of natural deduction, to prove that something is a theorem just means to demonstrate that a particular proposition is in fact a logical truth and must therefore be true in all possible valuations (and must therefore be a tautology).

Would you consider tableau methods axiomatic? And does the same problem apply to them?

The tableaux method is not axiomatic, as it does not make use of axioms. Instead, the tableaux method is one in which a general set of rules are applied to a particular set of propositions, either until it is impossible to apply any more rules, or until a contradiction has been extrapolated from the aforementioned set. Bear in mind that none of this is problematic; proof methods can only show propositions to be theorems if they are logical truths, and that is exactly what we want. My problem is not that I am having trouble proving a proposition that is not a tautology, my problem is rather that I am having trouble proving a proposition that is a tautology.

I'm trying to prove '~((~P → Q) → Q) → P'. In your proposition, '~(((~P→Q)→Q)→P)', the entire conditional is negated; in my proposition, '~((~P → Q) → Q) → P', only the antecedent of the conditional is negated.

Given what you've said I think your problem is that is also not a tautology as isn't it false when P and Q are false?

The proposition '~((~P → Q) → Q) → P' certainly is a tautology, and it is precisely this proposition that I am trying to prove. Let me show you.

Suppose that '~((~P → Q) → Q) → P' is false. Well, then (i) '~((~P → Q) → Q)' is true and (ii) 'P' is false.
Now, the proposition '~((~P → Q) → Q)' is just the negation of '((~P → Q) → Q)', and according to (i) the proposition '~((~P → Q) → Q)' is true.
It follows that (iii) '((~P → Q) → Q)' is false.
Moving on, if the proposition '((~P → Q) → Q)' is false, then '~P → Q' is true and 'Q' is false. According to (iii), '((~P → Q) → Q)' is indeed false. It follows that (iv) '~P → Q' is true and (v) 'Q' is false.
Next, if the proposition '~P → Q' is true, then either '~P' is false or 'Q' is true. According to (iv), '~P → Q' is true. It follows that either (vi) '~P' is false or (vii) 'Q' is true. Now, (vii) contradicts (v), so the only option left is (vi), that '~P' false.
Well, '~P' is just the negation of 'P', so if '~P' is false then 'P' is true. According to (vi), '~P' is false. It follows that (viii) 'P' is true. However, (viii) contradicts (ii). Those are all the possibilities. Therefore, '~((~P → Q) → Q) → P' is a tautology.

[Impenitent]

true conclusions do not follow from false premises

-Imp

[HexHammer]

true conclusions do not follow from false premises

-Imp

How do you know it's true in the first place?

[Arising_uk]

The proposition '~((~P → Q) → Q) → P' certainly is a tautology, and it is precisely this proposition that I am trying to prove. Let me show you.

Damn, my apologies egg3000, I think I need new glasses as I didn't see the negated P

Natural deduction is a different kind of proof method to the sort of axiomatic proofs I'm referring to. Nevertheless, natural deduction can only prove a proposition (in the sense that the proposition in question lies outside of the scope of any assumptions) if that proposition is a tautology. For example, if you were to assume 'P∧~P' as the first line in a natural deduction proof, then you could use the elimination rule for '∧' to show that 'P' and '~P', but only under the assumption of 'P∧~P'. Hence, you can show that P∧~P ⊢ P, and you can show that P∧~P ⊢ ~P, but it is not possible to show that ⊢P by itself or ⊢~P by itself. On the other hand, a proposition such as '(P∧~P)→Q' is a tautology, and so you can indeed use natural deduction to prove that ⊢(P∧~P)→Q. It's not a problem with any of the rules of natural deduction, to prove that something is a theorem just means to demonstrate that a particular proposition is in fact a logical truth and must therefore be true in all possible valuations (and must therefore be a tautology).

Ah! I'd forgotten what a logical truth was.

The tableaux method is not axiomatic, as it does not make use of axioms. Instead, the tableaux method is one in which a general set of rules are applied to a particular set of propositions, either until it is impossible to apply any more rules, or until a contradiction has been extrapolated from the aforementioned set. Bear in mind that none of this is problematic; proof methods can only show propositions to be theorems if they are logical truths, and that is exactly what we want. My problem is not that I am having trouble proving a proposition that is not a tautology, my problem is rather that I am having trouble proving a proposition that is a tautology.

I understand and until I get my books back and revise what I've forgotten I don't think I can help Although since you say what you are doing is not ND I probably can't as I wasn't taught anything else with respect to PL.

[Arising_uk]

-Imp How do you know it's true in the first place?

If its a contingent proposition then Empiricism appears best, for the others Logic rules.

[HexHammer]

Each year there's big lawsuit against advisor companies because they have made grave miscalculations, each month I see science articles rewritten because new evidence contradicts the prior beliefs.

Contingent propositions are fairytale nonsense, wake up to reality, we shouldn't deal with theoretical babble, but reality!

[Blaggard]

Hex you never know truth you just know yourself. That's what impenitent said if you would listen to anyone for 5 minutes.

Science at least is a preposition. Religion is not, know thy self.

"wake up with a hypothesis and destroy it over breakfast."

Anon Scientist. Don't wake up believing you KNOW anything, even yourself.

I hate to be pedantic but for someone who has all the answers, you clearly know a lot about everything, and not too much about that.

I don't know formal logic, can't be assed to try, but I don't post on threads where someone knows it, oh no wait! lol

-Imp

How do you know it's true in the first place?

If its a contingent proposition then Empiricism appears best, for the others Logic rules.

Or H...
ex's mum perhaps?

Always check your results/

Each year there's big lawsuit against advisor companies because they have made grave miscalculations, each month I see science articles rewritten because new evidence contradicts the prior beliefs.

Contingent propositions are fairytale nonsense, wake up to reality, we shouldn't deal with theoretical babble, but reality!

IU am an angry angry man. But each year there is no truth but right. The dexter is as sinister as the sinister though.

C15: from Latin sinister on the left-hand side, considered by Roman augurs to be the unlucky one

I of course prefer old English rather than Middle English, there's now so queer as bullshit.

[Arising_uk]

Each year there's big lawsuit against advisor companies because they have made grave miscalculations, each month I see science articles rewritten because new evidence contradicts the prior beliefs.

That'll be Empiricism applied to the contingent propositions then.

Contingent propositions are fairytale nonsense, wake up to reality, we shouldn't deal with theoretical babble, but reality!

You know that you type your nonsense and babble upon a machine based upon this theoretical babble don't you? How much more real do you wish it.

[HexHammer]

Each year there's big lawsuit against advisor companies because they have made grave miscalculations, each month I see science articles rewritten because new evidence contradicts the prior beliefs.

That'll be Empiricism applied to the contingent propositions then.

Contingent propositions are fairytale nonsense, wake up to reality, we shouldn't deal with theoretical babble, but reality!

You know that you type your nonsense and babble upon a machine based upon this theoretical babble don't you? How much more real do you wish it.

What you areally are saying is that this is a premise for religion.

[Blaggard]

No he was mocking you Hex, but as usual you were a little too sure to see it. It was a clever jibe, I think clever jibes sail right over your overly "knowledgeable" heads, as no doubt this one will. As you don't really read anything you disagree with, and are far too sharp and quick with your own inexplicable exactitude.