![]() | This ![]() It is of interest to the following WikiProjects: | ||||||||||
|
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:
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)
"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.
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)
I am a physicist who stumbled across this page and had never until now encountered something in Wikipedia which I really couldn't "get" just by reading it over. So my request is simple: Please use the amazing intelligence you all appear to possess to keep us from pushing our planet out of the (current, recent) metastable equilibrium that is favorable to our kind of life? You can go on with mathematics afterward, but much of current human activity is an existential threat to the future of mathematics... at least in our species and its relatives. If you can't figure out a way, I'm not sure anyone else can, or will, in time. Thanks for "listening." AquatiCat ( talk) 23:10, 20 March 2021 (UTC)
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)
Here's a stab at a lay person's explanation: "Skolemization is a mathematical technique used to simplify the automated theorem proving process." But that doesn't give a definition, it just describes its utility. It's really difficult to give a lay person's explanation of such a precise and technical thing. —Preceding unsigned comment added by 144.26.117.1 ( talk) 20:54, 16 December 2009 (UTC)
I get the basic idea behind this, but get lost a bit of the ways in: for example when the article states , I have a gut feeling for what this means, but would like to have the symbol 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)
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)
The Axiom of Choice is used to guarantee the existence of a Skolem function. Is it really necessary? I am new to the subject but suspicious because the Axiom of Choice seems to bust the borders of simple logical replacement algorithms since its validity is commonly due to the assumption of something as complicated as sets.
If it is needed, we should explicitly note that we need the Axiom of Choice to guarantee equisatisfiability. Otherwise, we should not use the axiom. Mathelerner ( talk) 21:32, 1 October 2022 (UTC)
![]() | This ![]() It is of interest to the following WikiProjects: | ||||||||||
|
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:
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)
"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.
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)
I am a physicist who stumbled across this page and had never until now encountered something in Wikipedia which I really couldn't "get" just by reading it over. So my request is simple: Please use the amazing intelligence you all appear to possess to keep us from pushing our planet out of the (current, recent) metastable equilibrium that is favorable to our kind of life? You can go on with mathematics afterward, but much of current human activity is an existential threat to the future of mathematics... at least in our species and its relatives. If you can't figure out a way, I'm not sure anyone else can, or will, in time. Thanks for "listening." AquatiCat ( talk) 23:10, 20 March 2021 (UTC)
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)
Here's a stab at a lay person's explanation: "Skolemization is a mathematical technique used to simplify the automated theorem proving process." But that doesn't give a definition, it just describes its utility. It's really difficult to give a lay person's explanation of such a precise and technical thing. —Preceding unsigned comment added by 144.26.117.1 ( talk) 20:54, 16 December 2009 (UTC)
I get the basic idea behind this, but get lost a bit of the ways in: for example when the article states , I have a gut feeling for what this means, but would like to have the symbol 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)
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)
The Axiom of Choice is used to guarantee the existence of a Skolem function. Is it really necessary? I am new to the subject but suspicious because the Axiom of Choice seems to bust the borders of simple logical replacement algorithms since its validity is commonly due to the assumption of something as complicated as sets.
If it is needed, we should explicitly note that we need the Axiom of Choice to guarantee equisatisfiability. Otherwise, we should not use the axiom. Mathelerner ( talk) 21:32, 1 October 2022 (UTC)