First Order Logic: Skolemization and Free Variables? Bound/Free Variable assignment.

Question

I have a couple of questions about the role of the free variables.

The first one is more specific:

1) So a formula to be in a Skolem Normal Form it has to be:

a) In Prenex Normal Form

b) Not to have any ∃ quantifiers.

c) Not to have any free variables

Okay, I know how to achieve a) and b), but I couldn't find information anywhere on how to achieve c)?

2) I am trying to grasp my mind around the idea of the difference between free variables and bound variables. I know the difference mechanically, I know the rules, I understand how to work with them, but I still cannot completely understand the difference in terms of intuition. I will share some questions that will help me understand:

a) If we have the formula: p(x)&∃q(x). The first occurrence of x is free, the second is bound.

• What is different between the two sub formulas in terms of x? My idea is that:
  • In both sub formulas if there is no x in the Domain to satisfy the
    formula it is false.
  • If there is at least one x to satisfy both sub formulas: then P(x) is feasible (I am not sure if that is the correct term) and q(x) is true.
  • If both subformulas are satisfied for all x then both are true.

Is that the difference? That if there is at least one x (but not all) that satisfies the formula if we have existence quantifier then the formula is true but if we don't have - it is feasible?

b) What happens when we make a Variable assignment?

• Does the bounded x get an assignment?
• Do both x's get assignment?

Thank you in advance!

Answer 1

What is the difference between free variables and bound variables.

Consider : $p(x) \land ∃xq(x)$ [typo corrected].

The first thing to note is that the quantified variable can be renamed without changing the "meaning" : $p(x) \land ∃yq(y)$.

Now, the issue regarding the difference between the two sub formulas in terms of $x$ has been removed.

As you say, in order to evaluate the truth-value of the formula in a domain $\mathfrak A$ you have to consider an assignment function : $s : \text {Var} \to \mathfrak A$.

Assume that there is $a \in \mathfrak A$ such that $q(a)$ holds. What about the satisfiability of the formula ? It depends on $s$ : if $s(x)=b$ and $p(x)$ holds for $b$, than the complete formula is satisfied by $s$ in $\mathfrak A$ :

$\mathfrak A \vDash (p(x) \land ∃yq(y))[s]$.

Now, consider the part $∃yq(y)$: we have that it is satified in $\mathfrak A$ by $s$ if there is an object $c \in \mathfrak A$ and an assignment $s'=s(y|c)$ which is exactly like $s$ except for one thing: at the variable $y$ it assignes the value $c$, such that $q(y)$ holds for $d$.

In conclusion, for $b, c \in \mathfrak A$: if $s(x)=b$ and $s'=s(y|c)$ and $p(x)$ holds for $b$ and $q(y)$ holds for $c$, we have that :

$\mathfrak A \vDash (p(x) \land ∃yq(y))[s]$,

i.e. the formula $p(x) \land ∃yq(y)$ is satisfied by $s$ in $\mathfrak A$.

---

The formal specification seems convoluted, but it is very easy to manufacture an example.

Consider the domain $\mathbb N$ of natural numbers and consider $(x = 0)$ as $p(x)$ and $(y > 0)$ as $q(y)$.

Consider the function $s$ such that : $s(x)=0$ and check whether :

$\mathbb N \vDash ((x = 0) \land ∃y(y > 0))[s]$.