Propositional logic concerns concepts such as truth, falsity, conjunction, disjunction, implication, biconditionals, and negation. This page serves as an index for proof modules and interfaces in this area.

##
Intuitionistic logic

Intuitionistic logic is a subsystem of classical logic which is sometimes used in its own right, and which here provides the proofs for many of the propositional logic theorems.

##
Classical logic

By adding the law of the excluded middle to intuitionistic logic, we get classical logic.

There are a variety of theorems which are fairly direct consequences of the above theorems but which exist to simplify proofs which use them.