自由变元（Free Variable）是数学逻辑和形式语言中的一个基本概念。在逻辑表达式中，自由变元是指那些在表达式中没有绑定（即没有被特定的量词如全称量词“?”或存在量词“?”所约束）的变量。
以下是一些关于自由变元的要点：
1. 绑定与未绑定：如果一个变量在某个表达式中被量词所绑定，那么它就不是自由变元；反之，如果变量没有被量词绑定，那么它是自由变元。
2. 量词的作用：全称量词“?x”表示“对于所有的x”，它绑定了变量x，使得x不再是自由变元。存在量词“?x”表示“存在一个x”，同样地，它也绑定了变量x。
3. 自由变元的实例：在表达式“x > 0”中，变量x是自由变元，因为它没有被任何量词所绑定。
4. 自由变元的重要性：自由变元是逻辑表达式的核心组成部分，它们决定了表达式的真值。例如，在表达式“对于所有的x，x > 0”中，如果x被赋值为0，则整个表达式的真值为假。
5. 自由变元与约束变元：与自由变元相对的是约束变元，后者在表达式中被量词所绑定。
理解自由变元对于逻辑学、数学和计算机科学等领域都非常重要，因为它们直接关系到表达式的含义和真值。
