1) What did I do wrong here? Or how do I go about solving it?
2) We say that "statement P is stronger than statement Q" if Q is true whenever P is true, but not conversely.
Thanks.
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.
I think it is clearer to say that P is stronger than Q if P implies Q.2) We say that "statement P is stronger than statement Q" if Q is true whenever P is true, but not conversely.
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.
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.
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 ?
This depends on which rules are primitive and which are derived. I guess the OP is working with the primitive ruleOriginally Posted by Ackbeet
$\displaystyle \frac{\neg A\qquad A}{\bot}$
It would require breaking $\displaystyle p\land\neg p$ apart. If $\displaystyle \neg A$ is considered to be an abbreviation for $\displaystyle A\to\bot$, then the rule above is just an instance of implication elimination.
I agree.
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.You're saying I can apply line 10 to line 6 without the box?
Yes. You don't have to prove conjuncts individually.Also, I can assume ~(~(r -> q) /\ (r -> q)) get a _|_ from p /\ ~p and derive ~(r -> q) /\ (r -> q) just like that?
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.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.
Yes, this is a better approach.If not then I'll just use ~(~(r -> q) /\ (r -> q)).