Talk:Skolem normal form

From Wikipedia, the free encyclopedia

You have new messages (last change).

The page that the word "equisatisfiable" links to, does not even mention the word "equisatisfiable", let alone define it. greenrd 02:45, 2 May 2006 (UTC)

Question with regards to definition of SNF: Elliot Mendelson, in Introduction to Mathematical Logic, (as well as my logic professor) defines SNF as a prenex normal form where every existential quantifier precedes every universal quantifier. If there are different conventions on how to describe SNF, does that merit a mention in the article?

Skolemization makes use of this equivalence:

\forall x_1 \dots \forall x_n \exists y R(x_1,\dots,x_n,y)

\Leftrightarrow

\exists f \forall x_1 \dots \forall x_n R(x_1,\dots,x_n,f(x_1,\dots,x_n))

I suppose, then, the Skolemization is simply finding f in the latter. In any case, the equivalence should be mentioned. —Ashley Y 10:42, 2005 May 17 (UTC)

That's irrelevant. Any first order formula of the form ∀ xPx or ∃ xPx is true only if there exist a property P such that for any/some x in the domain, Px holds. But who cares? We're talking first order here and its equivalence with some higher order formula is unimportant. The significance of Skolemization is to prove theorems such as Herbrand's sharpened Haupsatz which establishes an important relationship between first order validity and propositional truth functional validity. Nortexoid 00:52, 18 May 2005 (UTC)
I disagree. Skolemization is finding a particular function. The latter formula simply asserts that such a function exists. —Ashley Y 02:41, 2005 May 18 (UTC)
What could that possibly mean? The function is defined such that is has the value of quantified variable whose place it took. There is no "finding" involved and it needn't be asserted that the function 'exists' (again, whatever that means). Nortexoid 04:34, 18 May 2005 (UTC)
It's really very simple. There's an equivalence:
\forall x \exists y R(x,y) \Leftrightarrow \exists f \forall x R(x,f(x))
Skolemization consists of nothing more than specifying the function asserted to exist in the RHS formula. Note that this is true regardless of the "order" of the formula, for instance, x and y might themselves be functions. —Ashley Y 07:51, 2005 May 18 (UTC)
Who said it wasn't simple? There is no reason to introduce higher order machinery. It's irrelevant and confusing. Nortexoid 09:47, 18 May 2005 (UTC)

"Which makes the formula ... true". Only if f is defined. Otherwise f must be existentially quantified. That means, there has to be a way to define f (to meet the requirement of only universal quantifiers), not just to note that suchs a function exists. The above definition of SNF by Medelson solves this issue.


"that if a formula in the form ... is satisfied in some model, then for each x_1,\dots,x_n there must be some point y in the model which makes ... true". That's stating the obvious. Anyone who understand the meaning of that statement, realises that it's redundant.

Retrieved from "http://en.wikipedia.org../../../s/k/o/Talk%7ESkolem_normal_form_e9db.html"