Definition·D093
Free variables of a formula
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:
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, a negation has the same free variables as the formula it negates, a connective joining two formulas is free in the union of what each side is free in, and a quantifier is free in whatever its body is free in, except its own bound variable, which it strips out.
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, the four binary connectives share one clause and both quantifiers share one clause, 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.