在数学和其他涉及形式语言的学科中，包括数理逻辑和计算机科学，自由变量是在表达式中用于表示一个位置或一些位置的符号，某些明确的代换可以在其中发生，或某些运算（比如总和或量化）可以在其上发生。这个概念有关于占位符（它是以后会被文字串所替换），或表示未指定符号的通配符，但更加深入和复杂。
变量x成为约束变量，比如[1]
'对于所有x，(x+ 1)=x+ 2x+ 1'。
'存在x使得x= 2'。
在任何这种命题中，是否使用x或其他什么字母在逻辑上不重要。但是，在复合命题的其他地方再次使用同一个字母可能导致冲突。就是说，自由变量变成了约束的，并在支持公式的格式化的进一步工作中在某种意义上退休了。
在陈述自由变量和约束变量（或虚变量）的严格定义之前，我们会给出一些例子，使这两个概念比定义看起来更加清楚：
在表达式
中y是自由变量而x是约束变量（或虚变量）；因此这个表达式的值依赖于y的值。
在表达式
中x是自由变量而y是约束变量；因此这个表达式的值依赖于x的值。
在表达式
中y是自由变量而x是约束变量；因此这个表达式的值依赖于y的值。
在表达式
中x是自由变量而h是约束变量；因此这个表达式的值依赖于x的值。
在表达式
中z是自由变量而x和y是约束变量；因此这个表达式的真值依赖于z的值。
下列的
都是变量约束算子，它们都约束变量x。
变量约束机制出现在数学、逻辑和计算机科学中的不同情况中，但是在所有情形下它们是其中的表达式和变量的纯粹语法性质。本节中我们用叶子节点是变量、函数常量或谓词常量，而节点是逻辑运算符的树，识别表达式来总结语法。变量约束的运算符是几乎出现在所有形式语言中的逻辑运算符。没有它们的语言实际上要么是非常缺乏表达能力，要么非常难于使用。约束的运算符 Q 接受两个参数：变量v和表达式P，把 Q 应用于它的参数时就会生成新表达式 Q(v,P) 。约束运算符的意义由这个语言的语义提供而不是我们现在关心的。[2]
变量约束有关于三个事情：变量v，这个变量在表达式中的位置a，和形成 Q(v,P) 的节点n。注意: 我们定义在表达式中位置为在这个语法树中的叶子节点。变量约束在这个位置在节点n之下的时候发生。
举个数学的例子，考虑定义了一个函数的表达式
这里的 t 是一个表达式。t 可以包含某些、所有的、或者不包含x1, ...,xn的任意一个，并可以包含其他变量。在这种情况下我们称函数的定义约束了这些变量x1, ...,xn。