Proof Result:

### Logical Language and Proofs

#### Formulas

The standard propositional logical symbols can be used. Specifically, the allowed symbols and their representations are

• ¬ is `--` (negation)
• ∧ is `/\` (conjunction/and)
• ∨ is `\/` (disjunction/or)
• → is `->` (implication)

#### Justification

Each line of a proof consists of a formula written with variables and the symbols above and a justification. The justification is separated by `:` and consists of numbers, referencing the lines that justify the current formula. The possible justifications are

• `PR` premise, no justification needed.
• `AS` assumption, no justification needed. Used in conditional and indirect derivations.
• `MP` modus ponens, justified by two previous lines. Relative to the following, one of the listed lines should contain φ → ψ and the other φ.
φ → ψ, φ ⊢ ψ
• `MT` modus tollens, justified by two previous lines. Relative to the following, one of the listed lines should contain φ → ψ and the other ¬ ψ.
φ → ψ, ¬ ψ ⊢ ψ
• `DNE` double negation elimination, justified by one previous line. Relative to the following, the listed line should contain ¬(¬ φ).
¬(¬ φ) ⊢ φ
• `DNI` double negation introduction, justified by one previous line. Relative to the following, the list line should contain φ.
φ ⊢ ¬(¬ φ)
• `ADJ` adjunction, justified by two previous lines. Relative to the following, one of the listed lines should contain φ and the other ψ.
φ, ψ ⊢ φ ∧ ψ
• `S` simplification, justified by one previous line. Relative to the following, the listed line should contain φ ∧ ψ.
φ ∧ ψ ⊢ φ
• `ADD` addition, justified by one previous line. Relative to the following, the listed line should contain φ.
φ ⊢ φ ∨ ψ
• `MTP` modus tollendo ponens (also called disjunctive syllogism), justified by two previous lines. Relative to the following, one of the other listed lines should contain φ ∨ ψ and the other ¬ φ.
φ ∨ ψ, ¬ φ ⊢ ψ

#### Writing Proofs

Proofs are started with a show line, which consists of `show` followed by the formula to be proved. The following lines are formulas with justifications, until the QED line.

#### Proof Techniques

There are three styles of proofs that are allowed: direct derivations, conditional derivations, and indirect derivations. They are identified by their QED lines.
• Direct derivations prove any formula and have no assumptions. They begin with a show line and proceed directly from the show line to the QED line, which is `:DD` followed by the line number on which the formula specified in the show line was achieved.

• Conditional derivations prove formulas of the form φ → ψ and have one assumption, namely φ. They begin with assuming φ and proceed to achieve ψ. They conclude with the QED line, which is `:CD` followed by the line number on which ψ was achieved.

• Indirect derivations prove formulas of the from ¬ φ and have one assumption, namely φ. They begin with assuming φ and proceeds to achieve a contradiction, which is having ψ and ¬ ψ on separate lines for any formula ψ. They conclude with the QED line, which is `:ID` followed by the line numbers on which ψ and ¬ ψ were achieved.

Note that proofs can be nested using show and QED lines as usual.

#### Examples of Proofs

Law of Excluded Middle: `T |- (p \/ --p)`

``` 1. show: (p \/ --p) 2. show: ----(p \/ --p) 3. --(p \/ --p) :AS 4. show: --p 5. p :AS 6. p \/ --p :ADD 5 7. :ID 3 6 8. p \/ --p :ADD 4 9. :ID 3 8 10. p \/ --p :DNE 2 11. :DD 10 ```

One version of DeMorgan's Law: `--(P /\ Q) |- --P \/ --Q`

``` 1. show: --P \/ --Q 2. --(P /\ Q) :PR 3. show: ----(--P \/ --Q) 4. --(--P \/ --Q) :AS 5. show: ----P 6. --P :AS 7. --P \/ --Q :ADD 6 8. :ID 4 7 9. P :DNE 5 10. show: ----Q 11. --Q :AS 12. --P \/ --Q :ADD 11 13. :ID 4 12 14. Q :DNE 10 15. P /\ Q :ADJ 9 14 16. :ID 2 15 17. --P \/ --Q :DNE 3 18. :DD 17 ```