Skip to content
Axiomatic Wiki

HFoundation

14articles

The logical axioms of identity that sit beneath ZFC: the ground floor everything else is built on.

F01The logical frameworkClassical first-order logic with equality: the language everything here is written in.
Every article on this wiki is a statement in the formal language built from these symbols, together with variables and parentheses. The connectives and quantifiers are fixed by rules of inference, identity by four axioms, and membership by the ZFC axioms.
F02Implication If A then B: any proof of A can be turned into a proof of B.
Elimination is modus ponens: from and , conclude . Introduction discharges an assumption: if has been derived from the assumption , conclude and drop the assumption.
F03Falsum The absurd proposition: it has no proof, and from it anything follows.
Equivalently, as a statement of implication: for every proposition .
F04Negation Not A is an abbreviation: A implies falsum.
Defined from implication and falsum: to refute is to show that leads to absurdity.
F05Conjunction A and B: prove both to assert it, recover each from it.
To prove a conjunction, prove both conjuncts; from a conjunction, extract either conjunct.
F06Disjunction A or B, inclusively: it follows from either, and is used by cases.
Either disjunct proves the disjunction. Elimination is proof by cases, stated with implication: if each disjunct leads to , then follows from the disjunction.
F07Biconditional A if and only if B: implication in both directions.
Defined from implication and conjunction.
F08Excluded middleEvery proposition is true or false: the classical assumption.
Built from disjunction and negation. This is the one axiom separating classical logic from intuitionistic logic.
F09Universal quantifier For all x: instantiate at any term, prove at an arbitrary one.
Elimination instantiates: what holds of everything holds of any particular term . Introduction generalizes: if was derived using no assumption about , conclude .
F10Existential quantifier There is an x: prove it with a witness, use it via an arbitrary one.
Introduction: any witness satisfying proves the existential. Elimination, stated with the universal quantifier and implication: if follows from for arbitrary , then follows from bare existence.
F11Reflexivity of identityEverything is equal to itself.
Stated with the universal quantifier: everything, without exception, is equal to itself.
F12Symmetry of identityEquality can be read in either direction.
Built from the universal quantifier and implication.
F13Transitivity of identityChains of equalities compose.
Built from the universal quantifier, conjunction, and implication.
F14Substitutivity of identityEqual objects are interchangeable in any property (Leibniz).
Built from the universal quantifier and implication. Formally a schema: one instance for every formula .