# Natural Deduction

• Jun 8th 2011, 04:45 PM
Makall
Natural Deduction
1) What did I do wrong here? Or how do I go about solving it?
http://img848.imageshack.us/img848/6078/122g.png

2) We say that "statement P is stronger than statement Q" if Q is true whenever P is true, but not conversely.
http://img641.imageshack.us/img641/8162/programq.png

Thanks.
• Jun 8th 2011, 05:18 PM
emakarov
Quote:

Originally Posted by Makall
1) What did I do wrong here? Or how do I go about solving it?
http://img848.imageshack.us/img848/6078/122g.png

There are two options: either you closed the assumption 2 in step 6 or you did not. There is a variant of ND where you have to close all open assumptions A when you use implication introduction to derive A -> B, and there is a variant where you can close any number, including zero, of such assumptions. The latter variant is more prevalent. If you closed 2 in step 6 (which is probably the case because of the rectangle), then you can't use it in step 7. If you did not close it, then 2 is still open at the end.

Quote:

2) We say that "statement P is stronger than statement Q" if Q is true whenever P is true, but not conversely.
http://img641.imageshack.us/img641/8162/programq.png
I think it is clearer to say that P is stronger than Q if P implies Q.

If a program made 15 steps, then B is false, contrary to what you wrote. It is clear that if a program terminates within a day, then it terminates within a year.

For the last question, it is incorrect to write B ⊂ A because B and A are propositions, not sets. (Some textbooks use ⊃ to denote implication, but in any case it should be different from set inclusion.) You write that when the return value is -1, A is true and B is false. Therefore, A does not imply B, which means that A is not stronger than B.

Note, by the way, that falsehood (or a contradiction) is the strongest possible proposition because it implies everything. Similarly, a tautology is the weakest proposition because it is implied by everything.
• Jun 9th 2011, 12:18 AM
Makall
• Jun 9th 2011, 01:18 AM
emakarov
First, some discussion about vacuous assumptions. How do we derive q -> (p -> q) when p and q are different variables? We assume q, then derive p -> q by implication introduction closing a nonexistent open assumption p, and then derive q -> (p -> q) by implication introduction closing q. As I said earlier, implication introduction deriving A -> B allows closing any number of open assumptions A. Here we close zero open assumptions p.

Similarly, in negation introduction deriving ~A, we can close any number (including none) of open assumptions A.

Whether your derivation is correct depends on the assumptions you close in step 11. If #7 is a copy of #6, then it is not an assumption, so you can't close it. There are two possibilities: either make #7 an assumption and close it in step 11, or remove #7 altogether and don't close anything in step 11.

In fact, you can omit the whole first hypothetical block if in the second block you assume the negation of the whole conclusion, i.e., ~(~(r -> q) /\ (r -> q)).

ND usually has a rule that any formula is derivable from _|_. This rule is derivable using double-negation elimination (assume ~A, from _|_ derive ~~A and thus A, or from _|_ derive ~~A by closing a vacuous assumption ~A and thus A). With this rule, the whole derivation takes only 5 lines.
• Jun 9th 2011, 01:23 AM
Ackbeet
I could be wrong, but isn't the assumption a contradiction already? I'm seeing a proof with only 3 lines, assuming you're allowed to use contradiction intro and elim.
• Jun 9th 2011, 01:54 AM
Makall
I thought you need to enclose the _|_ in a box to be able to use it to negate the assumption. I've only seen examples where the _|_ is used in a box. You're saying I can apply line 10 to line 6 without the box?

Also, I can assume ~(~(r -> q) /\ (r -> q)) get a _|_ from p /\ ~p and derive ~(r -> q) /\ (r -> q) just like that? Don't I have to prove each part of a conjunction separately then use /\ i ?
• Jun 9th 2011, 02:26 AM
emakarov
Quote:

Originally Posted by Ackbeet
I could be wrong, but isn't the assumption a contradiction already? I'm seeing a proof with only 3 lines, assuming you're allowed to use contradiction intro and elim.

This depends on which rules are primitive and which are derived. I guess the OP is working with the primitive rule

$\frac{\neg A\qquad A}{\bot}$

It would require breaking $p\land\neg p$ apart. If $\neg A$ is considered to be an abbreviation for $A\to\bot$, then the rule above is just an instance of implication elimination.
• Jun 9th 2011, 02:38 AM
emakarov
Quote:

Originally Posted by Makall
I thought you need to enclose the _|_ in a box to be able to use it to negate the assumption.

I agree.
Quote:

You're saying I can apply line 10 to line 6 without the box?
I am not sure what you mean by applying line 10 to line 6. I suggest either changing the note in line 7 to "assumption" (since you can't close a derived formula in line 11), or removing line 7 altogether.

Quote:

Also, I can assume ~(~(r -> q) /\ (r -> q)) get a _|_ from p /\ ~p and derive ~(r -> q) /\ (r -> q) just like that?
Yes. You don't have to prove conjuncts individually.
• Jun 9th 2011, 03:01 AM
Makall
Quote:

Originally Posted by emakarov
I am not sure what you mean by applying line 10 to line 6. I suggest either changing the note in line 7 to "assumption" (since you can't close a derived formula in line 11), or removing line 7 altogether.

I thought you meant to remove line 7 and the box surrounding it. Then on line 11, change ~i 7, 10 to ~i 6, 10 meaning to apply _|_ directly on line 6 to get ~~(r -> q) with no boxes.
http://img820.imageshack.us/img820/3852/122gl.png

If not then I'll just use ~(~(r -> q) /\ (r -> q)).

Thanks for the help.
• Jun 9th 2011, 03:15 AM
emakarov
Quote:

Then on line 11, change ~i 7, 10 to ~i 6, 10 meaning to apply _|_ directly on line 6 to get ~~(r -> q) with no boxes.
You can't apply ~i to line 6 because it is derived; it is not an open assumption. The rules ->i and ~i only close open assumptions. I agree, to have ~i, you need a box. The only thing is that you have to either turn line 7 into an open assumption or remove it and thus pretend to close a vacuous assumption in line 11.

Quote:

If not then I'll just use ~(~(r -> q) /\ (r -> q)).
Yes, this is a better approach.