Free Variable

SE212

An occurrence of a variable is free if it does not fall within the scope of a quantifier for that variable.

An occurrance of a variable is bound if it falls within the scope of a quantifier for that variable.

A wff is closed if it contains no free variables.

We define $P[t/x]$ to be the formula obtained by replacing in $P$ every free occurrence of variable $x$ with $t$.

• The original expression $P$ CAN have the variable $t$, but there shouldn’t be a Variable Capture (see note for example)

CS241E

A free variable is one that is not bound in a given expression.

Consider this example of an Anonymous Function in Anonymous Function in Scala,

increase = { x => x + increment }

We say that increment is a free variable in this expression because it is not bound (Scala will say increment is not defined)

in contrast, the variable x can be used in the expression x + increment because it is bound when it is introduced as the parameter to the anonymous function in { x => ... }