Foundation·F02
Implication
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.
Part of the logical framework beneath ZFC (classical first-order logic with equality): taken as given rather than proven, it belongs to the language the set-theoretic axioms are stated in.
Remarks
Implication is primitive: it is not defined from other symbols, and its meaning is exhausted by the two rules (see the logical framework). Semantically
is false only when
is true and
is false; a false
makes the implication vacuously true, which is what lets universally quantified statements pass harmlessly over irrelevant cases. In Hilbert-style systems the introduction rule reappears as the deduction theorem. In Lean, implication is the primitive function arrow: a proof of
literally is a function turning proofs of
into proofs of
, so there is no definition to link to.
Used by
Propose an edit2 published revisions