Definition·D100
Propositional logical axiom schemas
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
is one of:
In words
A formula is a propositional axiom exactly when it is an instance of one of seven shapes: p implies (q implies p), a shape distributing an implication over an implication, contraposition, a conjunction holds exactly when it is not the case that the first implies the negation of the second, a disjunction holds exactly when the negation of the first implies the second, a biconditional holds exactly when it is not the case that one direction implies the negation of the other, and an existential holds exactly when it is not the case that the variable is universally negated.
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
Writing every schema in raw prefix notation keeps this a genuine formula of
rather than an informal shorthand: the first display is literally
, spelled out via the logical symbol for -> and concatenation for juxtaposition, and so on for the rest. 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.