Propositional
Propositional logic instantiates Popper’s Basis III: a formula’s atoms and connectives fix a truth table, and Basis III’s abstract deducibility becomes semantic entailment between formulas. Under this instance, conjunction, disjunction, and negation satisfy Popper’s own characterizing properties for a conjunction, a disjunction, and a classical negation.
| Module | Definitions | Abbreviations | Lemmas | Theorems | Examples | Difficulty |
|---|---|---|---|---|---|---|
| Formula | 4 | 1 | 0 | 0 | 0 | moderate |
| FunctionalCompleteness | 9 | 1 | 7 | 2 | 0 | optional |
| Hilbert | 4 | 0 | 12 | 1 | 0 | optional |
| Popper | 4 | 0 | 0 | 7 | 0 | hard |
| Completeness | 1 | 0 | 3 | 2 | 0 | hard |