)
)Top-level context. Axioms and definitions for propositional calculus.
We take implication and negation as primitive. The biconditional must also be taken primitive (it cannot be used to define itself).
| Sym | Comment |
| Logical negation. |
| () | Logical implication. |
| () |
| Name | Comment |
| ax-mp | Rule of Modus Ponens. |
| ax1 | Axiom Simp. |
| ax2 | Axiom Frege. |
| ax3 | Axiom Transp. |
| df-bi |
| Name | Sym | Comment |
| df-an | ( ) | |
| df-or | ( ) |