Classical

Base

classical interpretations
model relation
validity of formulas

Tautologies

contradiction (i.e. if ¬f and f hold every formula holds)
law of excluded middle
removal of double negation

Eval

alternative definition of the model relation based on an eval function mapping interpretations and formulas to booleans
equivalence proof of both model relation