1 Basics of Variables in Logical Expressions

1.1 Variables and their roles in formulas

In first-order logic, variables act as placeholders for objects in a domain. An expression containing variables can be interpreted in different ways depending on what values are assigned to those placeholders. Variables may appear in predicates (to indicate which object(s) the predicate applies to) and in terms (to build arguments of predicates or functions).

Variables do not, by themselves, determine a formula’s truth. Truth generally depends on both the chosen interpretation of symbols (predicates, functions, relations) and the specific assignment of values to variables that remain unspecified within the expression.

1.2 Atomic formulas and variable occurrence

Atomic formulas are the simplest statement forms, typically of the form \(P(t_1,\dots,t_n)\), where \(P\) is a predicate symbol and each \(t_i\) is a term that may contain variables. Variable occurrence refers to whether a variable appears textually or, more precisely, syntactically within the term structure of an atomic formula.

For many purposes, one distinguishes variables that occur in an atomic formula from those that are introduced later and constrained by quantifiers. This syntactic bookkeeping becomes crucial when determining which variables are free.

1.3 Free vs. bound distinction

A variable is bound if it is within the scope of a quantifier that declares it. A variable is free if it occurs in the expression but is not declared by any quantifier that covers that occurrence.

The distinction is not semantic only; it is determined by the syntax—specifically by the placement of quantifiers relative to variable occurrences. As a result, two formulas can have the same “surface meaning” under some readings yet differ in which variables are free, and that difference affects interpretation, substitution, and proof rules.

2 Quantifiers and Binding

2.1 Universal quantification (∀)

Universal quantification \(\forall x\,\varphi\) asserts that \(\varphi\) holds for every value of \(x\) in the domain. The variable \(x\) becomes bound within \(\varphi\). Any occurrence of \(x\) inside the scope of the quantifier is treated as ranging over the domain rather than as a parameter awaiting an external assignment.

Consequently, \(\forall x\,\varphi\) typically has fewer free variables than \(\varphi\) itself, because \(x\) no longer depends on an external choice.

2.2 Existential quantification (∃)

Existential quantification \(\exists x\,\varphi\) asserts that there exists at least one value of \(x\) for which \(\varphi\) is true. As with universals, \(x\) is bound in \(\varphi\) by the quantifier.

The same structural principle applies: within \(\exists x\,\varphi\), occurrences of \(x\) are not free with respect to the outer formula. Instead, the truth of the whole expression depends on whether some value can make the inner formula true.

2.3 Binding scope: where a quantifier applies

The scope of a quantifier is the part of the formula in which the bound variable’s occurrences are governed by the quantifier. Formally, scope is determined by how quantifiers are nested and by parentheses or the syntactic rules that determine grouping.

Only occurrences of a variable inside the relevant scope are bound by that quantifier; occurrences outside are unaffected and remain free (unless captured by another quantifier). Correct reasoning about free variables therefore requires tracking both quantifier nesting and scope boundaries.

3 Identifying Free Variables

3.1 Free variable occurrence in syntax

To identify free variables, one can apply a syntactic rule: start from the full formula and mark variables, then remove those occurrences that fall under a quantifier binding the same variable name within its scope. The remaining occurrences correspond to free variables.

This process is often described recursively on the structure of the formula: for compound formulas, free variables are computed from the free variables of the parts, with special subtraction in the case of a quantifier binding a variable.

3.2 Free variables in compound formulas (∧, ∨, ¬, →)

Compound logical connectives combine formulas without introducing new bindings. For negation, \(\neg\varphi\), the free variables are exactly the free variables of \(\varphi\). For conjunction \(\varphi\wedge\psi\) and disjunction \(\varphi\vee\psi\), free variables are the union of free variables from \(\varphi\) and \(\psi\). For implication \(\varphi\rightarrow\psi\), free variables similarly come from both sides.

This reflects a key point: connectives affect truth conditions but do not alter which variables are bound. Only quantifiers modify the free/bound status.

3.3 Example walkthroughs for common patterns

Consider \(P(x)\). There is no quantifier binding \(x\), so \(x\) is free.

Next, \(\forall x\,P(x)\) binds every occurrence of \(x\) inside the quantified scope, leaving no free occurrence of \(x\); if no other variables appear, the result is a closed formula (a sentence).

For a pattern like \(\exists y\,Q(y,z)\), the variable \(y\) is bound, while \(z\) is untouched and remains free. Thus the whole formula depends on \(z\) but not on \(y\).

These patterns generalize: any variable not introduced by an enclosing quantifier that covers its occurrence stays free.

4 Substitution and Capturing

4.1 Substitution for free variables

Substitution replaces free occurrences of a variable with a term. If \(\varphi\) contains free occurrences of \(x\), one can form \(\varphi[t/x]\), meaning “replace those occurrences of \(x\) with \(t\).” The intended effect is that the resulting formula expresses the same underlying predicate behavior but with the parameter \(x\) fixed to the term \(t\).

A crucial requirement is that the substitution should not alter occurrences of \(x\) that are bound by quantifiers in \(\varphi\). Bound variables are not meant to be replaced by the substitution, because their values are governed internally by their quantifiers.

4.2 Variable renaming (α-conversion)

α-conversion (alpha-conversion) is the practice of renaming bound variables consistently within a formula. For example, \(\forall x\,\varphi\) can be replaced by \(\forall y\,\varphi[y/x]\) provided the renaming avoids conflict with free variables and preserves binding structure.

This is not merely aesthetic: α-conversion can be used to prepare formulas for substitution by ensuring that no name collisions occur between bound variables and variables occurring in the substituted term.

4.3 Avoiding variable capture in substitutions

Variable capture occurs when a substitution introduces a variable that becomes accidentally bound by an existing quantifier. Suppose a substitution term contains a variable \(y\), and the target formula already has a quantifier \(\forall y\) whose scope includes the position where the substitution is inserted. Then occurrences of \(y\) inside the inserted term may become bound, changing the intended meaning.

Standard substitution definitions therefore include conditions—often enforced through renaming—that ensure the substituted term does not cause unintended binding of its internal variables.

4.4 Substitution correctness conditions

A substitution is considered correct when it respects binding structure and avoids capture. Typical correctness conditions include:

  • Only free occurrences of the target variable are replaced.
  • Any variable that appears in the replacing term is treated carefully relative to quantifiers already present in the formula.
  • If there is risk of capture, an appropriate α-conversion step is performed first.

In practice, logical systems formalize these requirements so that substitution behaves predictably and preserves logical equivalences where expected.

5 Semantics: Interpretation Dependence

5.1 Valuations/assignments and evaluating formulas

To evaluate first-order formulas, one uses an interpretation (domain plus meanings for predicate and function symbols) together with a variable assignment (also called a valuation), which maps each variable to an element of the domain.

Given an assignment \(s\), a formula \(\varphi\) can be evaluated as true or false under that assignment. Different assignments may yield different truth values if the formula contains free variables. If the formula is closed (no free variables), its truth value is independent of any external assignment.

5.2 What it means for a formula to “depend on” free variables

A formula “depends on” a free variable when changing the assignment of that variable can change the truth value of the formula. More formally, if two assignments agree on all free variables of \(\varphi\), then \(\varphi\) has the same truth value under both assignments.

Conversely, if a variable is not free in \(\varphi\), its assigned value does not affect evaluation, because either it is bound internally (so its value is handled by quantification) or it does not occur in the formula at all.

5.3 From formulas to predicates with parameters

Semantically, a formula with free variables can be viewed as a predicate with parameters. For instance, \(P(x)\) can be seen as defining a property of the parameter \(x\). Likewise, a formula with free variables \(x\) and \(z\) defines a relation between those parameters: the truth of the formula becomes a function of their chosen values.

This perspective connects syntactic free variables to semantic families of statements—one for each possible assignment to the free variables.

6 Free Variables in Proof Systems

6.1 Rules that mention free variables

Many proof systems use explicit restrictions involving free variables. For example, rules for introducing quantifiers commonly require that a variable be “arbitrary” (often meaning it is not constrained by assumptions) before universal generalization is allowed, and similarly that existential instantiation uses a witness consistent with the rule.

Free variables therefore play a role not only in model semantics but also in the admissibility of inference steps.

6.2 Generalization vs. specialization (conceptual relation to binding)

Specialization replaces a quantified variable by a particular term, producing an instance; generalization does the reverse by introducing a quantifier. While both are logically connected, their interaction with free variables is delicate: generalization requires conditions ensuring that the variable being quantified does not inadvertently depend on special assumptions.

Conceptually, specialization reduces quantificational generality to a concrete claim, while generalization lifts a claim back to a quantified statement. Proper handling of free variables ensures the lift is justified.

6.3 Common proof pitfalls involving unintended dependence

A frequent error is attempting to generalize a statement containing a variable that is not truly arbitrary from the standpoint of the proof context. If that variable appears in a way that depends on earlier assumptions, then universal generalization may fail.

Another pitfall involves substitution in proofs, where careless replacement can create variable capture or change which occurrences are bound, leading to an incorrect line that is syntactically well-formed but semantically unintended.

Robust proof practice typically includes:

  • checking which variables are free at each step,
  • respecting side conditions on inference rules,
  • using α-conversion when necessary to maintain clean binding structure.

7.1 Closed formulas (sentences) and quantifier closure

A closed formula (or sentence) has no free variables. Such formulas have a definite truth value under an interpretation without reference to external assignments. Quantifiers “close” formulas by binding variables, thereby eliminating dependence on those variables from outside the expression.

In many treatments, free variables serve as the interface between syntax and parameterized semantics, whereas closed formulas represent fully specified statements.

7.2 Free variable sets and notation conventions

It is common to denote the set of free variables of a formula \(\varphi\) as \(\mathrm{FV}(\varphi)\). This set supports concise statements like “\(\varphi\) depends only on variables in \(\mathrm{FV}(\varphi)\).”

Notation also appears in substitution conventions such as \(\varphi[t/x]\) and in side conditions for rules, where comparisons like \(x\notin \mathrm{FV}(\Gamma)\) (with \(\Gamma\) a set of assumptions) express “arbitrariness” requirements.

7.3 Connection to lambda calculus (high-level intuition)

At a high level, lambda calculus uses free variables and bound variables in a way that parallels first-order binding: lambda abstraction binds variables in its body, and free variables represent parameters not provided by the abstraction. This shared structure helps build intuition for binding and substitution, even though the logics and term constructors differ.

In both settings, capture-avoidance and correct scoping are central for maintaining meaning during substitution.

7.4 Parameterized statements vs. quantified statements

A quantified statement, such as \(\forall x\,\varphi\), expresses a claim uniform across all values of \(x\). A parameterized statement, such as \(\varphi\) with free \(x\), expresses how truth varies with the chosen value of \(x\).

Free variables thus correspond to parameters supplied externally (via assignments, witness choices, or context), while quantifiers correspond to internal ranging within the logic itself.

8 Examples and Mini Case Studies

8.1 Simple examples: P(x), ∀x P(x), ∃y Q(y, z)

  • \(P(x)\): \(x\) is free, so the truth of the formula may vary with the chosen value of \(x\).
  • \(\forall x\,P(x)\): \(x\) is bound, leaving no free variables from \(x\); the formula is closed if no other variables appear.
  • \(\exists y\,Q(y,z)\): \(y\) is bound by the existential quantifier, while \(z\) remains free.

These examples illustrate the mechanism by which quantifiers remove variables from the “external dependence” footprint.

8.2 Nested quantifiers and multiple free variables

Consider \(\forall x\,\exists y\,R(x,y,u)\). Here \(x\) and \(y\) are bound by their respective quantifiers. The variable \(u\) is not quantified anywhere, so it remains free.

Now compare \(\exists u\,\forall x\,\exists y\,R(x,y,u)\). In this second formula, \(u\) becomes bound by the outer existential quantifier, so if no other free variables exist, the entire expression becomes closed.

Nested quantifiers therefore act like layers of binding that progressively determine which symbols function as parameters.

8.3 Rewriting formulas to clarify free variables

Sometimes formulas are rewritten to make dependencies explicit. For instance, if one has \(\forall x\,P(x)\wedge Q(z)\), the free variable set is \(\{z\}\), because the quantifier binds all occurrences of \(x\). A clearer presentation might separate the quantified component and the parameter component to emphasize that the truth of the whole conjunction depends on \(z\) but is uniform with respect to \(x\).

Similarly, before performing substitution, one may use α-conversion to rename bound variables to avoid clashes with the variables occurring in the term being substituted. This can turn a potentially ambiguous operation into a straightforward one by ensuring capture cannot occur.