Natural Deduction — Read

1. Premise: $A$
   How to say this

   Read as: formula A

   Means: The metavariable A denotes an arbitrary formula.

2. Premise: $B$
   How to say this

   Read as: formula B

   Means: The metavariable B denotes an arbitrary formula.

3. conjunction introduction rule: $A \land B$
   How to say this

   Read as: A and B

   Means: The conjunction of formulas A and B.

Diagram description: Step 1 states formula A as a premise. Step 2 states formula B as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes A and B. The final conclusion is A and B.

Source: derivations.tex, line 50

1. Premise: $C$
   How to say this

   Read as: formula C

   Means: The metavariable C denotes an arbitrary formula.

2. Premise: $D$
   How to say this

   Read as: formula D

   Means: The metavariable D denotes an arbitrary formula.

3. conjunction introduction rule: $C \land D$
   How to say this

   Read as: C and D

   Means: The conjunction of formulas C and D.

Diagram description: Step 1 states formula C as a premise. Step 2 states formula D as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes C and D. The final conclusion is C and D.

Source: derivations.tex, line 59

1. Premise: $D$
   How to say this

   Read as: formula D

   Means: The metavariable D denotes an arbitrary formula.

2. Premise: $C$
   How to say this

   Read as: formula C

   Means: The metavariable C denotes an arbitrary formula.

3. conjunction introduction rule: $D \land C$
   How to say this

   Read as: D and C

   Means: The conjunction of formulas D and C, in that order.

Diagram description: Step 1 states formula D as a premise. Step 2 states formula C as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes D and C. The final conclusion is D and C.

Source: derivations.tex, line 68

1. Premise: $[C]^1$
   How to say this

   Read as: assumption C, labeled one for discharge

   Means: An occurrence of assumption C marked with discharge label one.

2. Premise: $D$
   How to say this

   Read as: formula D

   Means: The metavariable D denotes an arbitrary formula.

3. conjunction introduction rule: $C \land D$
   How to say this

   Read as: C and D

   Means: The conjunction of formulas C and D.

4. conditional introduction rule: $C \to (C \land D)$
   How to say this

   Read as: if C, then C and D

   Means: The conditional with antecedent C and consequent the conjunction of C and D.

Diagram description: Step 1 states assumption C, labeled one for discharge as a premise. Step 2 states formula D as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes C and D. Step 4 applies the conditional introduction rule to 3 and concludes if C, then C and D. The final conclusion is if C, then C and D.

Source: derivations.tex, line 80

1. Premise: $C$
   How to say this

   Read as: formula C

   Means: The metavariable C denotes an arbitrary formula.

2. Premise: $[D]^1$
   How to say this

   Read as: assumption D, labeled one for discharge

   Means: An occurrence of assumption D marked with discharge label one.

3. conjunction introduction rule: $C \land D$
   How to say this

   Read as: C and D

   Means: The conjunction of formulas C and D.

4. conditional introduction rule: $D \to (C \land D)$
   How to say this

   Read as: if D, then C and D

   Means: The conditional with antecedent D and consequent the conjunction of C and D.

Diagram description: Step 1 states formula C as a premise. Step 2 states assumption D, labeled one for discharge as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes C and D. Step 4 applies the conditional introduction rule to 3 and concludes if D, then C and D. The final conclusion is if D, then C and D.

Source: derivations.tex, line 80

1. Premise: $B$
   How to say this

   Read as: formula B

   Means: The metavariable B denotes an arbitrary formula.

2. conditional introduction rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

Diagram description: Step 1 states formula B as a premise. Step 2 applies the conditional introduction rule to 1 and concludes if A, then B. The final conclusion is if A, then B.

Source: derivations.tex, line 103

1. Premise: No explicit premise is printed for this inference rule.
2. inference rule: $(A \land B) \to A$
   How to say this

   Read as: if A and B, then A

   Means: The conditional whose antecedent is the conjunction A and B and whose consequent is A.

Diagram description: Step 1 has no printed premise. Step 2 applies the inference rule to 1 and concludes if A and B, then A. The final conclusion is if A and B, then A.

Source: proving-things.tex, line 20

1. Premise: $[A \land B]^1$
   How to say this

   Read as: the single assumption that is the conjunction of A and B, labeled one for discharge

   Means: An occurrence of the conjunctive assumption A and B marked with discharge label one.

2. Subderivation conclusion: $A$
   How to say this

   Read as: formula A

   Means: The metavariable A denotes an arbitrary formula.

3. conditional introduction rule: $(A \land B) \to A$
   How to say this

   Read as: if A and B, then A

   Means: The conditional whose antecedent is the conjunction A and B and whose consequent is A.

Diagram description: Step 1 states the single assumption that is the conjunction of A and B, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes formula A. Step 3 applies the conditional introduction rule to 2 and concludes if A and B, then A. The final conclusion is if A and B, then A.

Source: proving-things.tex, line 32

1. Premise: $[A \land B]^1$
   How to say this

   Read as: the single assumption that is the conjunction of A and B, labeled one for discharge

   Means: An occurrence of the conjunctive assumption A and B marked with discharge label one.

2. conjunction elimination rule: $A$
   How to say this

   Read as: formula A

   Means: The metavariable A denotes an arbitrary formula.

3. conditional introduction rule: $(A \land B) \to A$
   How to say this

   Read as: if A and B, then A

   Means: The conditional whose antecedent is the conjunction A and B and whose consequent is A.

Diagram description: Step 1 states the single assumption that is the conjunction of A and B, labeled one for discharge as a premise. Step 2 applies the conjunction elimination rule to 1 and concludes formula A. Step 3 applies the conditional introduction rule to 2 and concludes if A and B, then A. The final conclusion is if A and B, then A.

Source: proving-things.tex, line 42

1. Premise: No explicit premise is printed for this inference rule.
2. inference rule: $(\lnot A \lor B) \to (A \to B)$
   How to say this

   Read as: if either not A or B, then if A, then B

   Means: A conditional from the disjunction not A or B to the conditional from A to B.

Diagram description: Step 1 has no printed premise. Step 2 applies the inference rule to 1 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

Source: proving-things.tex, line 59

1. Premise: $[\lnot A \lor B]^1$
   How to say this

   Read as: the single assumption that is the disjunction of not A with B, labeled one for discharge

   Means: An occurrence of the disjunctive assumption not A or B marked with discharge label one.

2. Subderivation conclusion: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

3. conditional introduction rule: $(\lnot A \lor B) \to (A \to B)$
   How to say this

   Read as: if either not A or B, then if A, then B

   Means: A conditional from the disjunction not A or B to the conditional from A to B.

Diagram description: Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes if A, then B. Step 3 applies the conditional introduction rule to 2 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

Source: proving-things.tex, line 71

1. Premise: $[\lnot A \lor B]^1$
   How to say this

   Read as: the single assumption that is the disjunction of not A with B, labeled one for discharge

   Means: An occurrence of the disjunctive assumption not A or B marked with discharge label one.

2. Premise: $[\lnot A]^2$
   How to say this

   Read as: assumption not A, labeled two for discharge

   Means: An occurrence of assumption not A marked with discharge label two.

3. Subderivation conclusion: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

4. Premise: $[B]^2$
   How to say this

   Read as: assumption B, labeled two for discharge

   Means: An occurrence of assumption B marked with discharge label two.

5. Subderivation conclusion: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

6. disjunction elimination rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

7. conditional introduction rule: $(\lnot A \lor B) \to (A \to B)$
   How to say this

   Read as: if either not A or B, then if A, then B

   Means: A conditional from the disjunction not A or B to the conditional from A to B.

Diagram description: Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumption not A, labeled two for discharge as a premise. Step 3 applies the subderivation to 2 and concludes if A, then B. Step 4 states assumption B, labeled two for discharge as a premise. Step 5 applies the subderivation to 4 and concludes if A, then B. Step 6 applies the disjunction elimination rule to 1, 3, 5 and concludes if A, then B. Step 7 applies the conditional introduction rule to 6 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

Source: proving-things.tex, line 86

1. Premise: $[\lnot A \lor B]^1$
   How to say this

   Read as: the single assumption that is the disjunction of not A with B, labeled one for discharge

   Means: An occurrence of the disjunctive assumption not A or B marked with discharge label one.

2. Premise: $[\lnot A]^2, [A]^3$
   How to say this

   Read as: assumptions not A labeled two, and A labeled three, for discharge

   Means: Two active assumptions: not A carries discharge label two, while A carries discharge label three.

3. Subderivation conclusion: $B$
   How to say this

   Read as: formula B

   Means: The metavariable B denotes an arbitrary formula.

4. conditional introduction rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

5. Premise: $[B]^2, [A]^4$
   How to say this

   Read as: assumptions B labeled two, and A labeled four, for discharge

   Means: Two active assumptions: B carries discharge label two, while A carries discharge label four.

6. Subderivation conclusion: $B$
   How to say this

   Read as: formula B

   Means: The metavariable B denotes an arbitrary formula.

7. conditional introduction rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

8. disjunction elimination rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

9. conditional introduction rule: $(\lnot A \lor B) \to (A \to B)$
   How to say this

   Read as: if either not A or B, then if A, then B

   Means: A conditional from the disjunction not A or B to the conditional from A to B.

Diagram description: Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumptions not A labeled two, and A labeled three, for discharge as a premise. Step 3 applies the subderivation to 2 and concludes formula B. Step 4 applies the conditional introduction rule to 3 and concludes if A, then B. Step 5 states assumptions B labeled two, and A labeled four, for discharge as a premise. Step 6 applies the subderivation to 5 and concludes formula B. Step 7 applies the conditional introduction rule to 6 and concludes if A, then B. Step 8 applies the disjunction elimination rule to 1, 4, 7 and concludes if A, then B. Step 9 applies the conditional introduction rule to 8 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

Source: proving-things.tex, line 100

1. Premise: $[\lnot A]^2$
   How to say this

   Read as: assumption not A, labeled two for discharge

   Means: An occurrence of assumption not A marked with discharge label two.

2. Premise: $[A]^3$
   How to say this

   Read as: assumption A, labeled three for discharge

   Means: An occurrence of assumption A marked with discharge label three.

3. negation elimination rule: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

4. Subderivation conclusion: $B$
   How to say this

   Read as: formula B

   Means: The metavariable B denotes an arbitrary formula.

Diagram description: Step 1 states assumption not A, labeled two for discharge as a premise. Step 2 states assumption A, labeled three for discharge as a premise. Step 3 applies the negation elimination rule to 1, 2 and concludes a contradiction. Step 4 applies the subderivation to 3 and concludes formula B. The final conclusion is formula B.

Source: proving-things.tex, line 120

1. Premise: $[\lnot A \lor B]^1$
   How to say this

   Read as: the single assumption that is the disjunction of not A with B, labeled one for discharge

   Means: An occurrence of the disjunctive assumption not A or B marked with discharge label one.

2. Premise: $[\lnot A]^2$
   How to say this

   Read as: assumption not A, labeled two for discharge

   Means: An occurrence of assumption not A marked with discharge label two.

3. Premise: $[A]^3$
   How to say this

   Read as: assumption A, labeled three for discharge

   Means: An occurrence of assumption A marked with discharge label three.

4. falsehood introduction rule: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

5. falsehood elimination rule: $B$
   How to say this

   Read as: formula B

   Means: The metavariable B denotes an arbitrary formula.

6. conditional introduction rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

7. Premise: $[B]^2, [A]^4$
   How to say this

   Read as: assumptions B labeled two, and A labeled four, for discharge

   Means: Two active assumptions: B carries discharge label two, while A carries discharge label four.

8. Subderivation conclusion: $B$
   How to say this

   Read as: formula B

   Means: The metavariable B denotes an arbitrary formula.

9. conditional introduction rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

10. disjunction elimination rule: $A \to B$
    How to say this

    Read as: if A, then B

    Means: The conditional whose antecedent is A and whose consequent is B.

11. conditional introduction rule: $(\lnot A \lor B) \to (A \to B)$
    How to say this

    Read as: if either not A or B, then if A, then B

    Means: A conditional from the disjunction not A or B to the conditional from A to B.

Diagram description: Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumption not A, labeled two for discharge as a premise. Step 3 states assumption A, labeled three for discharge as a premise. Step 4 applies the falsehood introduction rule to 2, 3 and concludes a contradiction. Step 5 applies the falsehood elimination rule to 4 and concludes formula B. Step 6 applies the conditional introduction rule to 5 and concludes if A, then B. Step 7 states assumptions B labeled two, and A labeled four, for discharge as a premise. Step 8 applies the subderivation to 7 and concludes formula B. Step 9 applies the conditional introduction rule to 8 and concludes if A, then B. Step 10 applies the disjunction elimination rule to 1, 6, 9 and concludes if A, then B. Step 11 applies the conditional introduction rule to 10 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

Source: proving-things.tex, line 129

1. Premise: $[\lnot A \lor B]^1$
   How to say this

   Read as: the single assumption that is the disjunction of not A with B, labeled one for discharge

   Means: An occurrence of the disjunctive assumption not A or B marked with discharge label one.

2. Premise: $[\lnot A]^2$
   How to say this

   Read as: assumption not A, labeled two for discharge

   Means: An occurrence of assumption not A marked with discharge label two.

3. Premise: $[A]^3$
   How to say this

   Read as: assumption A, labeled three for discharge

   Means: An occurrence of assumption A marked with discharge label three.

4. negation elimination rule: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

5. falsehood elimination rule: $B$
   How to say this

   Read as: formula B

   Means: The metavariable B denotes an arbitrary formula.

6. conditional introduction rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

7. Premise: $[B]^2$
   How to say this

   Read as: assumption B, labeled two for discharge

   Means: An occurrence of assumption B marked with discharge label two.

8. conditional introduction rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

9. disjunction elimination rule: $A \to B$
   How to say this

   Read as: if A, then B

   Means: The conditional whose antecedent is A and whose consequent is B.

10. conditional introduction rule: $(\lnot A \lor B) \to (A \to B)$
    How to say this

    Read as: if either not A or B, then if A, then B

    Means: A conditional from the disjunction not A or B to the conditional from A to B.

Diagram description: Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumption not A, labeled two for discharge as a premise. Step 3 states assumption A, labeled three for discharge as a premise. Step 4 applies the negation elimination rule to 2, 3 and concludes a contradiction. Step 5 applies the falsehood elimination rule to 4 and concludes formula B. Step 6 applies the conditional introduction rule to 5 and concludes if A, then B. Step 7 states assumption B, labeled two for discharge as a premise. Step 8 applies the conditional introduction rule to 7 and concludes if A, then B. Step 9 applies the disjunction elimination rule to 1, 6, 8 and concludes if A, then B. Step 10 applies the conditional introduction rule to 9 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

Source: proving-things.tex, line 156

1. Premise: $[\lnot(A \lor \lnot A)]^1$
   How to say this

   Read as: assumption denying the whole disjunction A or not A, labeled one for discharge

   Means: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.

2. Subderivation conclusion: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

3. classical contradiction rule: $A \lor \lnot A$
   How to say this

   Read as: A or not A

   Means: The instance of excluded middle asserting the disjunction of A with its negation.

Diagram description: Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the classical contradiction rule to 2 and concludes A or not A. The final conclusion is A or not A.

Source: proving-things.tex, line 190

1. Premise: $[\lnot(A \lor \lnot A)]^1$
   How to say this

   Read as: assumption denying the whole disjunction A or not A, labeled one for discharge

   Means: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.

2. Subderivation conclusion: $\lnot A$
   How to say this

   Read as: not A

   Means: The negation of formula A.

3. Premise: $[\lnot(A \lor \lnot A)]^1$
   How to say this

   Read as: assumption denying the whole disjunction A or not A, labeled one for discharge

   Means: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.

4. Subderivation conclusion: $A$
   How to say this

   Read as: formula A

   Means: The metavariable A denotes an arbitrary formula.

5. negation elimination rule: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

6. classical contradiction rule: $A \lor \lnot A$
   How to say this

   Read as: A or not A

   Means: The instance of excluded middle asserting the disjunction of A with its negation.

Diagram description: Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes not A. Step 3 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 4 applies the subderivation to 3 and concludes formula A. Step 5 applies the negation elimination rule to 2, 4 and concludes a contradiction. Step 6 applies the classical contradiction rule to 5 and concludes A or not A. The final conclusion is A or not A.

Source: proving-things.tex, line 199

1. Premise: $[\lnot(A \lor \lnot A)]^1, [A]^2$
   How to say this

   Read as: two assumptions for discharge: the first denies the entire disjunction A or not A and is labeled one; the second is A and is labeled two

   Means: Two active assumptions: the negation of the complete disjunction A or not A carries label one, and A carries label two.

2. Subderivation conclusion: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

3. negation introduction rule: $\lnot A$
   How to say this

   Read as: not A

   Means: The negation of formula A.

4. Premise: $[\lnot(A \lor \lnot A)]^1$
   How to say this

   Read as: assumption denying the whole disjunction A or not A, labeled one for discharge

   Means: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.

5. Subderivation conclusion: $A$
   How to say this

   Read as: formula A

   Means: The metavariable A denotes an arbitrary formula.

6. negation elimination rule: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

7. classical contradiction rule: $A \lor \lnot A$
   How to say this

   Read as: A or not A

   Means: The instance of excluded middle asserting the disjunction of A with its negation.

Diagram description: Step 1 states two assumptions for discharge: the first denies the entire disjunction A or not A and is labeled one; the second is A and is labeled two as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the negation introduction rule to 2 and concludes not A. Step 4 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 5 applies the subderivation to 4 and concludes formula A. Step 6 applies the negation elimination rule to 3, 5 and concludes a contradiction. Step 7 applies the classical contradiction rule to 6 and concludes A or not A. The final conclusion is A or not A.

Source: proving-things.tex, line 211

1. Premise: $[\lnot(A \lor \lnot A)]^1$
   How to say this

   Read as: assumption denying the whole disjunction A or not A, labeled one for discharge

   Means: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.

2. Premise: $[A]^2$
   How to say this

   Read as: assumption A, labeled two for discharge

   Means: An occurrence of assumption A marked with discharge label two.

3. disjunction introduction rule: $A \lor \lnot A$
   How to say this

   Read as: A or not A

   Means: The instance of excluded middle asserting the disjunction of A with its negation.

4. negation elimination rule: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

5. negation introduction rule: $\lnot A$
   How to say this

   Read as: not A

   Means: The negation of formula A.

6. Premise: $[\lnot(A \lor \lnot A)]^1$
   How to say this

   Read as: assumption denying the whole disjunction A or not A, labeled one for discharge

   Means: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.

7. Subderivation conclusion: $A$
   How to say this

   Read as: formula A

   Means: The metavariable A denotes an arbitrary formula.

8. negation elimination rule: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

9. classical contradiction rule: $A \lor \lnot A$
   How to say this

   Read as: A or not A

   Means: The instance of excluded middle asserting the disjunction of A with its negation.

Diagram description: Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 states assumption A, labeled two for discharge as a premise. Step 3 applies the disjunction introduction rule to 2 and concludes A or not A. Step 4 applies the negation elimination rule to 1, 3 and concludes a contradiction. Step 5 applies the negation introduction rule to 4 and concludes not A. Step 6 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 7 applies the subderivation to 6 and concludes formula A. Step 8 applies the negation elimination rule to 5, 7 and concludes a contradiction. Step 9 applies the classical contradiction rule to 8 and concludes A or not A. The final conclusion is A or not A.

Source: proving-things.tex, line 226

1. Premise: $[\lnot(A \lor \lnot A)]^1$
   How to say this

   Read as: assumption denying the whole disjunction A or not A, labeled one for discharge

   Means: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.

2. Premise: $[A]^2$
   How to say this

   Read as: assumption A, labeled two for discharge

   Means: An occurrence of assumption A marked with discharge label two.

3. disjunction introduction rule: $A \lor \lnot A$
   How to say this

   Read as: A or not A

   Means: The instance of excluded middle asserting the disjunction of A with its negation.

4. negation elimination rule: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

5. negation introduction rule: $\lnot A$
   How to say this

   Read as: not A

   Means: The negation of formula A.

6. Premise: $[\lnot(A \lor \lnot A)]^1$
   How to say this

   Read as: assumption denying the whole disjunction A or not A, labeled one for discharge

   Means: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.

7. Premise: $[\lnot A]^3$
   How to say this

   Read as: assumption not A, labeled three for discharge

   Means: An occurrence of assumption not A marked with discharge label three.

8. disjunction introduction rule: $A \lor \lnot A$
   How to say this

   Read as: A or not A

   Means: The instance of excluded middle asserting the disjunction of A with its negation.

9. negation elimination rule: $\bot$
   How to say this

   Read as: a contradiction

   Means: The falsum symbol, meaning contradiction.

10. classical contradiction rule: $A$
    How to say this

    Read as: formula A

    Means: The metavariable A denotes an arbitrary formula.

11. negation elimination rule: $\bot$
    How to say this

    Read as: a contradiction

    Means: The falsum symbol, meaning contradiction.

12. classical contradiction rule: $A \lor \lnot A$
    How to say this

    Read as: A or not A

    Means: The instance of excluded middle asserting the disjunction of A with its negation.

Diagram description: Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 states assumption A, labeled two for discharge as a premise. Step 3 applies the disjunction introduction rule to 2 and concludes A or not A. Step 4 applies the negation elimination rule to 1, 3 and concludes a contradiction. Step 5 applies the negation introduction rule to 4 and concludes not A. Step 6 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 7 states assumption not A, labeled three for discharge as a premise. Step 8 applies the disjunction introduction rule to 7 and concludes A or not A. Step 9 applies the negation elimination rule to 6, 8 and concludes a contradiction. Step 10 applies the classical contradiction rule to 9 and concludes formula A. Step 11 applies the negation elimination rule to 5, 10 and concludes a contradiction. Step 12 applies the classical contradiction rule to 11 and concludes A or not A. The final conclusion is A or not A.

Source: proving-things.tex, line 243