Axiomatic WikiWWikiDDefinitionsPropositional logical axiom schemas
Definition·D100
Three schemas for implication and negation, sufficient by themselves for propositional completeness, plus one biconditional schema pinning each of the other three connectives to its -> / not unfolding.
For a language
, a formula
is a propositional axiom
there exist
and, for the quantifier schema,
, such that, writing formulas with the notation of D109,
is one of:
In words
A formula is a propositional axiom exactly when it is an instance of one of seven schemas: the first formula implies that the second formula implies the first, if the first formula implies that the second implies the third, then the first formula implying the second implies that the first implies the third, if the negation of the second formula implies the negation of the first, then the first implies the second (contraposition), a conjunction of two formulas holds exactly when it is not the case that the first implies the negation of the second, a disjunction of two formulas holds exactly when the negation of the first implies the second, a biconditional between two formulas holds exactly when it is not the case that the forward implication implies the negation of the backward implication, and an existential over a variable holds exactly when it is not the case that the negation of the formula holds for every value of that variable.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 · A09 (computed from the citation graph, not asserted).
Remarks
Each schema is now written using the notation of D109 instead of spelled out via the raw construction directly: since
are already known to lie in
, a display such as
still names a genuine formula of
built from the logical symbols of the alphabet by concatenation, not an informal claim about
. The first three are the classical Łukasiewicz-style axioms for
alone - already complete for propositional logic once combined with modus ponens and the deduction theorem, a fact this wiki will not reprove from scratch. The remaining four pin
to their intended meaning purely in terms of
(and, for
,
): since satisfaction already gives all seven connectives independent, native truth clauses, these axioms are exactly what is needed for soundness to go through - without them,
would be syntactically inert, provable of nothing. Quantifier and equality axioms are separate; the full set of logical axioms is their union with this one.