I have a problem in understanding quantification for set-builder notation (comprehensions) and equational definitions. For example, $odd$ natural numbers can expressed as:
$\{ x \in \Bbb N \mid \exists k \in \Bbb N, x = 2k+1 \}$ (1) set builder,correction suggested by John Hughes
$\exists k \in \mathbb{N} : x = 2k + 1 $ (2) definition
as a comprehension and a definition.
With respect to comprehensions, in the absence of an explicit quantifier, are the variables before $|$ considered free in comprehensions?
With respect to equational definition, I am unsure of $Odd$ as a predicate, where $x$ is on the left of the equation.
$\text {Odd}(x) \text { iff } \exists k \in \mathbb N \ (x=2k+1)$
Are the variables in arguments of such predicates, and even functions, considered free?
(2) is the definition of the predicate $\text {Odd}(x)$ :
In (2) the variable $k$ is bound, while the variable $x$ is free.
This corresponds to the fact that we are defining a unary predicate (a "property") that will hold of all and only those numbers $n$ that satisfy the corresponding formula.
(1), slightly corrected : $\{ x \mid \exists k ∈ \mathbb N \ (x=2k+1) \}$, is the definition of the set $\text {Odd}$ of odd numbers.
In (1) we are using the set-builder notation, whose syntax is $\{ x \mid \varphi(x) \}$, where $\varphi(x)$ is a formula with variable $x$ occurring free.
In our case the formula is again $\exists k ∈ \mathbb N \ (x=2k+1)$, where $k$ is bound.
The set-builder notation acst itself as a quantifier, binding the variable $x$. This corresponds to the fact that the notation does not define a property, but use a (formula expressing a) property to define a set : the set of all and only those $x$ that satisfy the formula.
There is a simple link between the two expressions :