Convert this solution to inference notation

Question

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.

Answer 1

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

Answer 2

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.