Editing First-order logic (section)

===Free and bound variables===
{{Main|Free variables and bound variables}}

In a formula, a variable may occur ''free'' or ''bound'' (or both). One formalization of this notion is due to Quine, first the concept of a variable occurrence is defined, then whether a variable occurrence is free or bound, then whether a variable symbol overall is free or bound. In order to distinguish different occurrences of the identical symbol ''x'', each occurrence of a variable symbol ''x'' in a formula &phi; is identified with the initial substring of &phi; up to the point at which said instance of the symbol ''x'' appears.<ref name="Quine81">[[Willard Van Orman Quine|W. V. O. Quine]], [https://www.google.com/books/edition/_/6_syEAAAQBAJ?hl=en&gbpv=1&pg=PP1 ''Mathematical Logic''] (1981). [[Harvard University Press]], 0-674-55451-5.</ref><sup>p.297</sup> Then, an occurrence of ''x'' is said to be bound if that occurrence of ''x'' lies within the scope of at least one of either <math>\exists x</math> or <math>\forall x</math>. Finally, ''x'' is bound in &phi; if all occurrences of ''x'' in &phi; are bound.<ref name="Quine81" /><sup>pp.142--143</sup>

Intuitively, a variable symbol is free in a formula if at no point is it quantified:<ref name="Quine81" /><sup>pp.142--143</sup> in {{math|∀''y'' ''P''(''x'', ''y'')}}, the sole occurrence of variable ''x'' is free while that of ''y'' is bound. The free and bound variable occurrences in a formula are defined inductively as follows.
; Atomic formulas : If ''φ'' is an atomic formula, then ''x'' occurs free in ''φ'' if and only if ''x'' occurs in ''φ''. Moreover, there are no bound variables in any atomic formula.
; Negation : ''x'' occurs free in ¬''φ'' if and only if ''x'' occurs free in ''φ''. ''x'' occurs bound in ¬''φ'' if and only if ''x'' occurs bound in ''φ''
; Binary connectives : ''x'' occurs free in (''φ'' → ''ψ'') if and only if ''x'' occurs free in either ''φ'' or ''ψ''. ''x'' occurs bound in (''φ'' → ''ψ'') if and only if ''x'' occurs bound in either ''φ'' or ''ψ''. The same rule applies to any other binary connective in place of →.
; Quantifiers : ''x'' occurs free in {{math|∀''y'' ''φ''}}, if and only if x occurs free in ''φ'' and ''x'' is a different symbol from ''y''. Also, ''x'' occurs bound in {{math|∀''y'' ''φ''}}, if and only if ''x'' is ''y'' or ''x'' occurs bound in ''φ''. The same rule holds with {{math|∃}} in place of {{math|∀}}.

For example, in {{math|∀''x'' ∀''y'' (''P''(''x'') → ''Q''(''x'',''f''(''x''),''z''))}}, ''x'' and ''y'' occur only bound,<ref>''y'' occurs bound by rule 4, although it doesn't appear in any atomic subformula</ref>  ''z'' occurs only free, and ''w'' is neither because it does not occur in the formula.

Free and bound variables of a formula need not be disjoint sets: in the formula {{math|''P''(''x'') → ∀''x'' ''Q''(''x'')}}, the first occurrence of ''x'', as argument of ''P'', is free while the second one, as argument of ''Q'', is bound.

A formula in first-order logic with no free variable occurrences is called a ''first-order [[sentence (mathematical logic)|sentence]]''. These are the formulas that will have well-defined [[truth value]]s under an interpretation. For example, whether a formula such as Phil(''x'') is true must depend on what ''x'' represents. But the sentence {{math|∃''x'' Phil(''x'')}} will be either true or false in a given interpretation.