Axiomatic WikiWWikiDDefinitionsFree variables of a formula
Definition·D093
Every variable occurring in an atomic formula's terms is free; a negation or connective just unions its parts; a quantifier strips its own bound variable out.
For a language
, the set of variables occurring free in a formula
, written
, is characterized by (using the notation of D109): for
and
:
for
and
with
:
for
:
for
and
:
for
and
:
In words
An equality of two terms is free in exactly the variables occurring in either term, a relation applied to a tuple of terms is free in whatever occurs in any of them, and a negation has the same free variables as the formula it negates. Each of the four binary connectives joining two formulas is free in the union of what each side is free in: conjunction, disjunction, the conditional, and the biconditional. Likewise, each quantifier is free in whatever its body is free in, except its own bound variable, which it strips out: the universal quantifier and the existential quantifier.
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
Existence and uniqueness of
, for every formula, is T38. Unlike satisfaction, all four binary connectives share the same combination rule (the union of each side's free variables) and both quantifiers strip the same single bound variable from the same body, since which connective or quantifier it is does not affect which variables are free - only *how they are combined into a formula* was ever connective-specific, and free-variable occurrence does not see truth values at all. A formula
with
is a sentence: its truth under an assignment cannot depend on that assignment, since nothing in it is free to vary.