• 合式公式等于命题，当且仅当 所有变元用个体常项赋值 或用 量词约束 。

定义

• 约束变元 ：若变元 出现在使用变元的量词的辖域之内。
• 自由变元 ：若变元 不为约束变元。

示例

类比

1
2internal class Program
3{
4int count = 0;
5void increaseCount(int x)
6{
7count += x;
8}
9}
10

(★) 例题#1 - 判断下列个体变量为自由变元还是约束变元

约束变元改名规则

• 将量词中的变元以及该量词辖域中此变元的所有约束出现都用新的个体变元替换。
• 新的变元名称有别于辖域中其他的变元。

自由变元的代入规则

• 对于每个自由出现，都用新的个体变元替换。
• 新的变元不允许在原公式中以任何约束形式出现，也可用个体常量代入。

闭式

• 设是 任意一个公式，若 中无自由出现的个体变元，则称 为封闭的合式公式，即闭式。
• 闭式是一个命题。

类比

1
2using static System.Console;
3
4internal class Program
5{
6static int increaseCount(int count, int x)
7{
8return count += x;
9}
10
11private static void Main()
12{
13int count = 0;
14WriteLine(count); // 0
15count = increaseCount(count, 1);
16WriteLine(count); // 1
17}
18}
19