1
$\begingroup$

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!

Improve this question
$\endgroup$
  • $\begingroup$ 1c) start from the unievrsal closure of the formula you want "skolemize". $\endgroup$ – Mauro ALLEGRANZA Jan 26 '17 at 12:15
  • $\begingroup$ Oh right... so we just add universal quantifiers for every free variable. And the in order to achieve conjunctive normal form from SNF we just remove those universal quantifiers and we don't have anymore free variables? So to make it more simple: in order to achieve CNF we can just ignore the free variables? $\endgroup$ – Dimitur Epitropov Jan 26 '17 at 12:51
1
$\begingroup$

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]$.

Improve this answer
$\endgroup$
  • $\begingroup$ Thanks a lot, that solved me a lot of headaches. Two things made the difference in order to wrap my head around: 1) That we can just rename the bounded x 2)" 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$ :" So if s(x)=b and p(x)[s] holds but q(x)[s] doesn't hold, but there is such $a$ for which q(x) holds the whole formula is still satisfied by $s$ in $\mathfrak A$. right? :) $\endgroup$ – Dimitur Epitropov Jan 26 '17 at 12:44
  • $\begingroup$ 1) the "renaming" trick is not formally necessary: in the formal specs we have only to verify that $c$ exists and $s'=s(x|c)$ will works. But for readibility, avoiding multiple use of variables (taking into account that FOL language has an infinite supply of them : $x_0,x_1,\ldots$) may help. $\endgroup$ – Mauro ALLEGRANZA Jan 26 '17 at 12:51
  • $\begingroup$ 2) yes; with free vars, a formula can be satisfied by $s$ and not satisfied by a different $s'$. In my example with $\mathbb N$, $s(x)=0$ satisfy it while $s'(x)=1$ will not. In general, we say that $\varphi$ is satisfiable in $\mathfrak A$ if there is at least one $s$ such that $\mathfrak A \vDash \varphi [s]$. $\endgroup$ – Mauro ALLEGRANZA Jan 26 '17 at 12:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.