1 Basic definitions

1.1 Variables in formal expressions

In formal systems such as logic, mathematics, and computer science, a variable is a placeholder symbol that can denote different objects (numbers, elements of a domain, terms, types, etc.) depending on interpretation. Variables appear inside expressions that are built from symbols like logical connectives (and, or, not), predicates, function symbols, and—crucially—quantifiers.

Variables may play different roles depending on whether they are constrained by a quantifier. This distinction leads to the central idea of free versus bound variables.

1.2 Free vs. bound variables

A variable is called free in a formula or expression when it is not bound by any quantifier. Informally, the formula remains dependent on that variable’s value, because nothing in the formula fixes it.

A bound variable is constrained by a quantifier such as “for all” or “there exists.” Binding turns the variable into a local placeholder whose specific name is not meant to affect the meaning.

1.2.1 Quantifiers and binding

Quantifiers introduce binding by attaching to a variable and covering a specific part of the formula (its scope). For example, in a formula of the form

  • “∀x P(x)” the variable \(x\) is bound in \(P(x)\);
  • “∃y Q(y, z)” binds \(y\) within \(Q(y, z)\) but leaves \(z\) unaffected if it is not otherwise quantified.

Binding is structural: it is determined by where the quantifier sits syntactically, not by the variable’s appearance “in meaning” or “in prose.”

1.2.2 Scope of a variable

The scope of a quantifier is the syntactic region of a formula over which the bound variable is considered bound. A variable can appear in multiple places; whether those occurrences are free or bound depends on whether they fall within the scope of the quantifier that binds the variable.

If an occurrence lies outside every quantifier that binds that variable, the occurrence is free. If it lies inside the scope of at least one such quantifier, it is bound.

1.3 Occurrences: free occurrences vs. bound occurrences

The classification is typically applied to occurrences of variables, not merely to the symbol as a whole. A formula can contain some occurrences of a variable that are free and others that are bound, depending on nested quantifiers and shadowing.

Accordingly:

  • a free occurrence is an appearance of the variable not governed by any applicable quantifier scope for that variable;
  • a bound occurrence is an appearance controlled by some quantifier scope for that variable.

This occurrence-based viewpoint is important when dealing with nested quantifiers, repeated variable names, and transformations like substitution.

2 Quantifiers and scope

2.1 How quantifiers create binding

Quantifiers create binding by associating a variable with a portion of a formula. The variable’s role changes from “unknown input” (free) to “locally quantified variable” (bound) within the quantifier’s scope.

Because quantifiers are syntactic constructs, their effect is determined by the parse tree of the formula: the region under the quantifier defines the scope.

2.1.1 Universal quantification (∀)

In universal quantification, the statement has the form “∀x φ,” meaning \(φ\) holds for every permissible value of \(x\). Within \(φ\), the occurrences of \(x\) are bound by this universal quantifier, since the quantifier supplies the value range conceptually.

Outside the scope of that quantifier, \(x\) would not be bound by it and could become free (or bound by another quantifier).

2.1.2 Existential quantification (∃)

Existential quantification, “∃x φ,” expresses that there exists at least one value of \(x\) for which \(φ\) is true. As with universal quantification, any occurrence of \(x\) inside \(φ\) becomes bound by the existential quantifier.

Thus, a formula with free \(x\) indicates an open parameter, while a formula with quantified \(x\) indicates the truth of the statement does not depend on a particular external choice of \(x\).

2.2 Determining the free variables of a formula

The set of free variables of a formula is the collection of variables that have at least one free occurrence. Computing it is a matter of recursively analyzing the formula’s structure:

  • when encountering a quantifier “Qx ψ,” variables free in ψ except \(x\) remain free;
  • variables that are bound by that quantifier cease to be counted as free within its scope;
  • variables unaffected by quantifiers contribute as free variables if they appear unbound.

This recursive “remove the bound variable’s contribution” procedure aligns with the semantics: free variables are precisely those that require an external assignment to evaluate the formula.

2.3 Scope rules and syntactic structure

Scope is governed by the grammar used to build formulas. Many logical notations omit explicit parentheses, so the intended grouping matters. For instance, depending on convention,

  • “∀x P(x) ∧ Q(x)” might be parsed as either “(∀x P(x)) ∧ Q(x)” or “∀x (P(x) ∧ Q(x))”; these lead to different sets of free variables.

Formal treatments therefore rely on precise syntax, such as parenthesized expressions or explicit binding constructs, to unambiguously specify which occurrences fall under which quantifiers.

3 Free variables in formula interpretation

3.1 Open formulas and parameters

A formula with at least one free variable is often called an open formula. Such a formula does not, by itself, determine a single truth value; rather, it describes a relationship that depends on the chosen values of its free variables.

The free variables function like parameters: supplying concrete values (an “assignment”) yields an evaluable statement.

3.2 Truth under an assignment

Semantics typically evaluates an open formula relative to a mapping (an assignment) from variables to elements of a domain (or to specific terms, depending on the setting).

Given an open formula \(\phi(x_1,\dots,x_n)\), an assignment that maps each \(x_i\) to a particular domain element produces a determinate truth value for \(\phi\). Different assignments can produce different outcomes, reflecting the fact that the truth of \(\phi\) is parameter-dependent.

When the formula is closed (has no free variables), evaluation does not require external assignments; the formula is treated as a sentence whose truth is absolute within a model.

3.3 Meaning of expressions with free variables

In interpretation, a free-variable formula represents a family of statements—one for each possible instantiation of its free variables. This perspective explains why transformations that preserve free variables’ structure (or that handle them correctly) are essential in formal reasoning.

For example, an expression involving free variables may be viewed as defining a predicate over those variables: “for any choice of values, the formula yields whether the described property holds.”

4 Substitution and renaming

4.1 Substitution for free variables

Substitution replaces variables with terms. When substituting for free variables, the intent is typically to instantiate the open formula while preserving binding structure.

A common form is: given a formula \(\phi\) with free variable \(x\), and a term \(t\), one forms \(\phi[t/x]\) by replacing free occurrences of \(x\) with \(t\). Bound occurrences of \(x\) are not replaced, because they are locally controlled by quantifiers.

This restriction prevents substitution from unintentionally changing the meaning of quantification.

4.2 Alpha-conversion (renaming bound variables)

Alpha-conversion is the systematic renaming of bound variables within their scopes. Since bound variables behave like placeholders, changing their names does not alter the formula’s meaning, as long as the renaming is consistent and does not interfere with other bindings.

For instance, “∀x P(x)” and “∀y P(y)” are considered equivalent by alpha-conversion. Such renaming is often used as a preprocessing step before substitution.

4.2.1 Renaming for clarity and normalization

Renaming can also improve readability and supports algorithmic manipulation in proof systems and theorem provers. Many systems adopt conventions to maintain standard forms of variable naming to reduce ambiguity.

4.3 Capture-avoiding substitution

Variable capture occurs when a substitution introduces a variable into a context where it becomes bound by an existing quantifier, unintentionally changing the meaning.

Capture-avoiding substitution ensures that when substituting a term for a free variable, the operation does not “get caught” by quantifiers. The standard method is:

  1. perform alpha-conversion to rename bound variables that could conflict;
  2. then apply substitution for the intended free variable.

This guarantees that the replaced free variables remain free in the resulting formula (except where the original semantics genuinely binds them).

4.4 Common pitfalls and examples

A frequent error is treating substitution as purely textual. In logical syntax, the distinction between bound and free occurrences is essential.

Typical pitfalls include:

  • substituting under a quantifier when only free occurrences should change;
  • ignoring scope and assuming that renaming is unnecessary;
  • accidentally introducing a variable that is already quantified elsewhere, leading to capture.

Careful handling of binding and scope rules prevents these mistakes.

5 Worked examples

5.1 Free variables in simple predicates

Consider the predicate \(R(x,y)\). Both \(x\) and \(y\) are free if no quantifiers bind them. The formula is open and its truth depends on the chosen pair of domain elements.

If the formula is “∀x R(x,y),” then \(x\) becomes bound by the universal quantifier, while \(y\) remains free. The result is a statement about all \(x\) values with \(y\) acting as an external parameter.

5.2 Nested quantifiers and scope

Now examine “∀x ∃y (S(x,y) ∧ T(y,z)).”

  • \(x\) is bound by the outer universal quantifier.
  • \(y\) is bound by the inner existential quantifier.
  • \(z\) is not quantified anywhere, so \(z\) is free.

The formula expresses existence and universality relationships internally, while leaving \(z\) as an outside input.

A more subtle case is reusing variable names in nested scopes. For instance, “∀x (P(x) ∧ ∃x Q(x))” uses the same symbol \(x\) twice. The inner quantifier binds its own \(x\) within its scope; alpha-conversion can be used to clarify this by renaming one of them to a different variable.

5.3 Free variables across compound statements

Free-variable structure is preserved through connectives like conjunction and disjunction. For example, if \(\phi(x)\) and \(\psi(y)\) are open formulas, then “\(\phi(x) ∧ \psi(y)\)” has free variables consisting of the union of free variables from \(\phi\) and \(\psi\), minus any variables that become bound by quantifiers introduced around the compound.

If a quantifier encloses a compound formula, it can remove a variable from the free-variable set across the entire enclosed region. This behavior is a direct consequence of scope: quantifiers affect all occurrences inside their grammatical reach.

6 Free variables in common logical systems

6.1 First-order logic

In first-order logic, free variables occur in atomic formulas built from predicate symbols applied to terms. Terms may include variables and function symbols. Quantifiers bind variables within formulas, producing closed sentences when no free variables remain.

The standard semantic clause evaluates formulas with free variables relative to assignments. In this setting, the distinction between free and bound variables is foundational for:

  • defining satisfiability of open versus closed formulas,
  • formulating rules of inference that are sound with respect to substitution and quantifier introduction.

6.2 Predicate logic syntax conventions

Predicate logic presentations often include conventions that simplify tracking of scope:

  • quantifiers are written with explicit variable lists (e.g., ∀x or ∃y),
  • parentheses clarify binding,
  • “free variable” is usually defined syntactically and then tied to the semantics.

Some notations also allow shorthand for multiple quantifiers, such as ∀x∀y φ. These are syntactic sugar for nested quantifiers, which means the same scope analysis applies.

6.3 Relationship to terms and functions

Free variables can occur not only in predicate argument positions but also inside terms if the language allows function symbols. For example, in “P(f(x)),” the occurrence of \(x\) within the term \(f(x)\) is free if not quantified elsewhere.

When substitutions are performed, both variable occurrences inside terms and variables occurring directly as term arguments must be handled consistently. Capture-avoidance still applies if substitutions interact with quantifiers that bind variables appearing inside substituted terms.

7 Practical uses

7.1 Constraints and parameterization in specifications

Free variables naturally model parameters in formal specifications and program contracts. A requirement written with free variables can be interpreted as a template: after selecting values for those parameters, the specification becomes a concrete assertion.

This style is common in settings like type systems, static analysis, and formal verification, where one reasons about a family of program behaviors parametrized by inputs or intermediate values.

7.2 Role in proof systems and inference rules

Many proof rules manipulate formulas by introducing or eliminating quantifiers. The correct treatment of free variables is essential to maintain soundness:

  • rules for quantifier introduction typically require that certain variables are not free in particular assumptions;
  • rules for quantifier elimination often rely on substitution instances of quantified variables.

Hence, tracking which variables are free (and where they appear) determines whether a given inference step is permitted.

7.3 Connection to unification and logic programming

In logic programming paradigms, such as those based on Horn clauses, free variables in goals correspond to unknowns to be determined. Unification computes substitutions that make two expressions compatible, effectively replacing variables with terms to satisfy constraints.

While logic programming typically operates with conventions about scope and variable renaming (to avoid accidental capture or clashes), the underlying mechanism aligns with substitution for variables and careful handling of binding contexts.

8.1 Bound variables

Bound variables are variables whose occurrences are constrained by a quantifier. Their values are not supplied externally; instead, the quantifier determines how to interpret them (universally or existentially) over a domain.

Bound-variable analysis is often the complement of free-variable analysis and is essential for understanding transformations and inference rules.

8.2 Bound variable capture

Bound variable capture occurs when a variable introduced or inserted by a transformation becomes bound unexpectedly due to an intervening quantifier. This changes the logical content of the formula.

Capture-avoidance techniques—typically using alpha-conversion followed by substitution—exist to prevent this problem.

8.3 Closed formulas (sentences)

A closed formula is one with no free variables. Because all variables are either bound by quantifiers or absent, the formula can be evaluated to a single truth value within a model without reference to external assignments.

Closed formulas are often called sentences in first-order logic contexts.

8.4 Closures and quantifier introduction

A closure of an open formula is formed by introducing quantifiers for its free variables, producing a closed formula. For example, from an open formula \(φ(x)\), one can form “∀x φ(x)” or “∃x φ(x),” each yielding a closed statement with a different logical reading.

Quantifier introduction is closely tied to reasoning tasks: it generalizes from parameter-dependent statements to fully quantified claims, provided the proof conditions regarding free variables are satisfied.