自由变量和约束变量
维基百科,自由的 encyclopedia
在数学和其他涉及形式语言的学科中,包括数理逻辑和计算机科学,自由变量是在表达式中用于表示一个位置或一些位置的符号,某些明确的代换(英语:Substitution_(logic))可以在其中发生,或某些运算(比如总和或量化)可以在其上发生。这个概念有关于占位符(它是以后会被文字串(英语:String literal)所替换),或表示未指定符号的通配符,但更加深入和复杂。
变量x成为约束变量,比如
- 对于所有 x,(x + 1)2 = x2 + 2x + 1。
或
- 存在x,使得 x2 = 2。
在任何这种命题中,是否使用x或其他什么字母在逻辑上不重要。但是,在复合命题的其他地方再次使用同一个字母可能导致冲突。就是说,自由变量变成了约束的,并在支持公式的格式化的进一步工作中在某种意义上“退休”了。