Axiomatic WikiWWikiDDefinitionsQuantifier logical axiom schemas
Definition·D101
Instantiating a universal at a substitutable term, and pulling a universal out past an antecedent it does not mention.
For a language
(using the notation for formulas and terms), a formula
is a quantifier axiom
there exist
and
such that, taking either a term
with
for the first schema, or a formula
with
for the second,
is one of:
In words
A formula is a quantifier axiom exactly when it has one of two shapes: a universal quantification implies the result of substituting a term, free for the bound variable, into its body, or a universal quantification of an implication implies the implication with the universal pulled across to just the consequent, provided the bound variable is not free in the antecedent.
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
Both schemas need a side condition to stay sound: dropping "
" from the first would let a substituted term's own variable be captured (see D099's notes for the exact failure), and dropping "
" from the second would let a quantifier over
soak up a
that was never meant to be bound - e.g. taking
itself would derive nonsense. Together with D100 and D102, these are the quantifier-handling half of the full logical axiom set a deduction system will be built from.