2

I have a problem to solve:

$\forall x[\neg P(x) \land \forall y \neg Q(x,y) \rightarrow \forall x \forall y R(x,y,z)]$

I see that two quantifiers are influencing on the exact same variable.That's why I'm to make a change of variables: x change to t and y to k

Then this is what I have :

$\forall x[ P(x) \lor \exists y Q(x,y) \lor \forall t \forall k R(t,k,z)]$

Then I am making a preformed normal form

$\forall x \exists y \forall t \forall k [P(x) \lor Q(x,y) \lor R(t,k,z)]$

And finally making skolemization

y=f(x)

$\forall x \forall t \forall k [P(x) \lor Q(x,f(x)) \lor R(t,k,z)]$

Is it a right answer? Because I still don't know what to make with free variable z. How can I automatically check the answer of such problems? I mean can MATLAB or Mathematica solve the skolemization problems like this?

Natalie Clarius
  • 10,530
Elvin
  • 220
  • 1
  • 9

1 Answers1

1

There are different procedures for forming the skolemization, but if you want to treat open formulas (= formulas with free variables), you'd normally start by forming the universal closure of the formula, that is, for each free variable, introduce a universal quantifier to the beginning of the formula:

$0.\ ∀x[¬P(x)∧∀y¬Q(x,y)→∀x∀yR(x,y,z)]$ (original formula)

$1.\ ∀z∀x[¬P(x)∧∀y¬Q(x,y)→∀x∀yR(x,y,z)]$ (universal closure)

$2.\ ∀z∀x[P(x)∨∃yQ(x,y)∨∀t∀kR(t,k,z)]$ (resolve variable conflicts)

...

This is sound because semantically, free variables are implicitly universally quantified: By the definition of validity, a formula is valid if it is true under all valuations; but if a formula with free variables fulfills that requirement, that amounts to just the same as universally quantifying over all the free variables. So just putting a $\forall$ in front of every free variable leaves you with essentially the same formula that is now closed. (After all, with skolemization we do just the same vice versa in the end, where we remove all the $\forall$ quantifiers in the prefix to yield an quantifier-less, open formula.)

A different procedure that allows to treat open formulas without requiring to form the universal closure at the very beginning eliminates universal quantifiers on the fly rather than at the very end, but the above mentioned procedure should be fine with the way you layed out the skolemization in your post.

What's missing in your skolemization is the final, most crucial step, namely the elimination of the quantifiers:

...

$4.\ ∀z∀x∀t∀k[P(x)∨Q(x,f(z,x))∨R(t,k,z)]$ (note that with the additional $\forall z$ in front of the $\exists y$, we now also need $z$ in $f(z,x)$)

$5.\ P(x)∨Q(x,f(z,x))∨R(t,k,z)$ (eliminate universal quantifiers -- this is your fully skolemized formula)

Natalie Clarius
  • 10,530
  • thanks a lot for your answer, but do you know if something like MATLAB could solve these problems automatically. I need it because I have to check myself – Elvin Aug 05 '19 at 18:23
  • why the function is f(x,z) but not the f(z,x)? – Elvin Aug 05 '19 at 19:14
  • 1
    You are of course right -- it should be $f(z,x)$, not $f(x,z)$. I fixed it; thanks for the hint. Re. your other question: I have never worked with Matlab and am not aware of any other tools either, sorry. – Natalie Clarius Aug 05 '19 at 19:16
  • should the result also be in a CNF form ? – Elvin Aug 15 '19 at 19:14
  • @Elvin That depends on what you need. By itself, skolemization doesn't include conversion into CNF. If you want to apply resolution or something, you have to turn the formula into CNF before or after skolemization. – Natalie Clarius Aug 15 '19 at 19:29
  • but the answer we have is in CNF form? – Elvin Aug 15 '19 at 19:39
  • That's because you already CNF'ed and PNF'ed your formula before the actual skolemization (which is just the elimination of quantifiers). – Natalie Clarius Aug 15 '19 at 21:31