### 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