Convert this solution to inference notation

This is a proof for De Morgan's Law.

Could you help me convert this to inference notation so I can understand the proof better? I find it hard reading this, specifically, which line each assumption is supposed to go and who deduces who.

• In line 10 you try to use assumption from line 8 which was already discharged. This is error. – Trismegistos Mar 11 '14 at 11:04

We have to prove that $\lnot p \land \lnot q \Leftrightarrow \lnot (p \lor q)$ (1). You exhibit the right implication.

1. Is the assumption (the left hand side of (1))

2. It is applied the $\land$-elimination rule to 1

3. The same as in 2, but inferring the other term in the conjunction

4. It is assumed the negation of the conclusion 13, that is the disjunction $p \lor q$ (here it is started a sub-derivation 1)

5. It is assumed $p$ in the preceding disjunction (opening of sub-derivation 1.1)

6. It is (trivially) inferred $p$ from 5 (closure of (/ exit from) sub-derivation 1.1)

7. It is now assumed $q$, the other term of the disjunction (open sub-derivation 1.2)

8. It is assumed the negation of $p$ (opening of sub-derivation 1.2.1, in view of $\lnot$-intrduction, line 10)

9. It is (trivially) inferred $\lnot p$ form 8 (closure of (/ exit from) 1.2.1 with the formula $\lnot \lnot p$, in the following line 10)

10. Because of 3 and 7, in the closure of the sub-deduction 1.2.1 we have $q \land \lnot q$; this implies, by $\lnot$-intro the negation of 1.2.1 assumption, that is $\lnot \lnot p$

11. It is applied to 10 $\lnot$-elimination (in your system there should be a rule which say that if in the deduction there is a formula $\lnot \lnot A$ the deduction can continue by adding the formula $A$ by $\lnot$-elimination (closure of (/ exit from) 1.2 with the formula $p$ in the following line 12)

12. By $\lor$-elimination it is inferred $p$ (there should be a rule of the kind: it is possible open a deduction assuming a disjunction $A \lor B$ (the 4); if in a sub-deduction of that, assuming $A$ (5) we obtain $A$ (6), and in a second sub-deduction, assuming $B$ (7) we obtain again $A$ (11), we can infer $A$); closure of (/ exit from) sub-deduction 1, returning to the main deduction

13. Applying again $\lnot$-intro, by contraposition of 2 and 12 (an embryo of "ex falso quodlibet"), having supposed 4 in sub-deduct. 1, the desired conclusion is obtained

• line 10 is error you can not use line 8 because it was already discharged -- box start on line 8 and ends on 9. – Trismegistos Mar 11 '14 at 11:10
• I had never seen this box-rappresentation before, but it is obviously equivalent to a deduction with labelled lines. I find a purely formal convention (i.e. not necessary) the fact we cannot mention the assumption line of a preceding discharged deduction, when that assumption has to do with a rule definition (in this case the $\lnot$-intro). Indeed, I think that, for the sake of clarity, it is good to refer to it in the line where the rule is being applied. (Using this argument, also line 13 would be wrong...) – Bento Mar 11 '14 at 12:31
• I don't understand what you mean but my book about Fitch system says that you can not reference part of subproof that already ended. It shows example that such reference can lead to proving contradiction. In other worlds you can only reference lines from superproofs not from subproofs. – Trismegistos Mar 11 '14 at 13:39
• @Trismegistos, Please, can you tell me if in Fitch's layout there are inference rules such as, for example, $\lnot$-introduction (I have interpreted this way the $\lnot I$ in the question) presented in the form I mentioned? It seems to me that the Fitch's form and the one I know are specular. If there is, I will show you the reason I consider this aspect irrelevant. – Bento Mar 11 '14 at 15:57
• I have seen on Wikipedia this system, and just as I imagined it is specular. What I meant was: The rule is: (1) We can open a sub-deduction assuming a formula A (2) If in this sub-deduction we obtain any formula B and $\lnot$B, sub-deduction can end and (3) the (sub-)deduction in which that one closing is nested, continue with the adjunction of $\lnot$A, justified by $\lnot$-itroduction. Well, having said that, can you see some sort of risk in putting a reference to the line where A has been introduced by assumption in the current line in which we apply the rule? (I am conscious.......... – Bento Mar 11 '14 at 16:32

It is a quite nice notation , not sure which other notation you mean (but i would like to know , please give me a reference)

the layout is called the Fitch or Graphical style of natural deduction

Lets start with that there is an error: Line 1 ia a premisse not an assumption (some writers don't make any difference between them, but assumptions are discharged, premmisses are not)

then:

• The Assumptions are market with (A) after the formula so the assumptions are on line 4,5,7,and 8

• An assumption starts a box and where the box ends/ closes the assumption that opened the box is discharged.

• Boxes can be nested, fully within other boxes, but boxes may not "overlap", so outer boxes are always bigger than inner boxes and so you can always say which box needs to close first.
• you may refer to formula's in open boxes but not to formula's in closed boxes

in the example:

• the box of assumption 4 ends at line 12
• the box of assumption 8 ends at line 9
• box 4-12 is the most outer box
• box 8-9 is within box 4-12 and 7-11

lines 6 and 9 are a bit a unusual rule they are reiterations, the reiteration rule allows you to copy a formula on an earlier lines. (but it may not be from within an allready closed box)

hopes this helps, but am intrigeud by what your prefered scheme is.