# Metamath Proof Explorer

Propositional calculus deals with general truths about well-formed formulas (wffs) regardless of how they are constructed. The simplest propositional truth is , which can be read "if something is true, then it is true" - rather trivial and obvious, but nonetheless it must be proved from the axioms (see Theorem id).

Our system of propositional calculus consists of three basic axioms and another axiom that defines the modus-ponens inference rule. It is attributed to Jan Lukasiewicz (pronounced woo-kah-SHAY-vitch) and was popularized by Alonzo Church, who called it system P2. (Thanks to Ted Ulrich for this information.) These axioms are ax-1, ax-2, ax-3, and (for modus ponens) ax-mp. Some closely followed texts include [Margaris] for the axioms and [WhiteheadRussell] for the theorems.

The propositional calculus used here is the classical system widely used by mathematicians. In particular, this logic system accepts the "law of the excluded middle" as proven in exmid, which says that a logical statement is either true or not true. This is an essential distinction of classical logic and is not a theorem of intuitionistic logic.

All 194 axioms, definitions, and theorems for propositional calculus in Principia Mathematica (specifically *1.2 through *5.75) are axioms or formally proven. See the Bibliographic Cross-References at mmbiblio.html for a complete cross-reference from sources used to its formalization in the Metamath Proof Explorer.

1. Recursively define primitive wffs for propositional calculus
2. The axioms of propositional calculus
3. Logical implication
4. Logical negation
5. Logical equivalence
6. Logical conjunction
7. Logical disjunction
8. Mixed connectives
9. The conditional operator for propositions
10. The weak deduction theorem for propositional calculus
11. Abbreviated conjunction and disjunction of three wff's
12. Logical "nand" (Sheffer stroke)
13. Logical "xor"
14. Logical "nor"
15. True and false constants
16. Truth tables