Talk:Skolem normal form

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: Start Class Low Priority  Field: Foundations, logic, and set theory
Please update this rating as the article progresses, or if the rating is inaccurate. Please also add comments to suggest improvements to the article.

Contents

[edit] Definition of SNF

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.

[edit] Equisatisfiable

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)

[edit] Lay person's explanation please!

I am grateful for the degree of expertise and precision reflected in this article, but it badly needs a simple, lay person's explanation in addition to the precise mathematical definition. It should give the reader some idea of why it exists, what it's used for, what problem it addresses, so the read can get some intuitive sense of what it is all about. Can anyone help add this please? Thanks. -- DBooth 17:20, 29 January 2007 (UTC)

I don't understand the "uses of ..." part. Anyway, Skolemization is used in the process of converting any FOPL formula to clausal normal form, which is required in order to use resolution by refutation (a process that can be automated) to prove a provable theorem. I don't want to touch the article since I don't understand all of it, but perhaps something should be added about this, or at least a link to the clausal normal form page. Tapir (talk) 20:13, 5 May 2008 (UTC)

[edit] more wikilinks please

I get the basic idea behind this, but get lost a bit of the ways in: for example when the article states \exists M \exists \mu ~.~ ( M,\mu \models \Phi), I have a gut feeling for what this means, but would like to have the symbol \models explained/linked/defined. I don't see that the topic of this article is so complex that the reader must be assumed to know model theory. (especially since skolemization is used in AI circles, it could use a more layman's approach) linas 01:00, 20 June 2007 (UTC)

\models is a basic notion of derivability and should be part of every introductory course to logic. And thus can be assumed as background knowledge for a reader of this page.

[edit] "Skolemification"

Is the process really called "Skolemification"? That word gets 0 hits at books.google.com, groups.google.com, and amazingly even at google.com. As does "skolemify". —Preceding unsigned comment added by 66.194.141.170 (talk) 21:44, 20 May 2008 (UTC)

  • It's "skolemization". Neither "Skolemification" nor "skolemify" occur in the article. Tizio 12:33, 26 May 2008 (UTC)