自由变元和约束变元

指变元在公式中的出现而言。一个(个体)变元x在公式A中的一个出现是约束的，如果x的这一出现是在量词x或x中或在量词x或x的辖域中；否则称为自由的。在一公式中约束出现的变元称为约束变元，自由出现的变元称为自由变元。在一公式A中量词x(x)的辖域是指紧接x(x)的右方的A的子公式。在有的数理逻辑书中，根据公式的形成规则，同一变元在一公式中可以同时自由出现又约束出现；有的书中则规定不能同时既自由出现又约束出现。例如：在公式

xF(x，y)→xyF(x，y)

中，x的所有出现都是约束的，y的第一个出现是自由的，第二和第三个出现是约束的；x的辖域是它的紧接右方的F(x，y)，x的辖域是yF(x，y)，y的辖域是它右方的F(x，y)。

称一项t对公式A(x)中的x而言是自由的，如果x在A(x)中的自由出现都不在A(x)的形如yB的子公式中，其中y是在t中出现的变元。

在高阶逻辑中，变元(包括高阶变元)的自由出现和约束出现，如上类似地定义。