Chapter 20-22 - PL proofs - syntax
if
a…¬a
then
⊥ (falsum)
if
a… ⊥
then
¬a
the introduction and elimination rules for negation can be viewed as an intro/elim rule for ⊥
solving exercises:
- look at the conclusion
- its main connective’s introduction rule
e.g.:
¬P
in the exam there are usually two exercises, one easy and one difficult