Talk:Prenex normal form

Is the first formula correct ?

Yes. Either Q or not Q. If Q, then anything implies Q, so in particular, the LHS is true, and ∃xP(x) implies Q, so LHS=RHS. If not Q, then both sides reduce to "P never holds" (i.e. there is no x such that P(x)), so again they must be equal. greenrd 01:42, 2 May 2006 (UTC)

Article Title

I am curious as to whether or not the "normal" used in this articles title is misplaced. The form the article details converting terms to doesn't seem to correspond to what would normally be considered a normal form (by the current process formulas can correspond to several prenex "normal" form terms). Is this not just prenex form, with prenex conjuntive/disjunctive normal forms being special cases? --Luke.mccrohon (talk) 14:43, 23 January 2008 (UTC)

Question

Does someone know where the name comes from?

In the example, after the implication, the page says that one formula can have more than one prenex forms. Now, if the formula we had started with had an exists z rho, instead of forall z rho, at the head, then following the different rewriting orders, we would get two prenex formulae which mean different things:

1) forall x . exists z . (phi or psi) implies rho

2) exists z . forall x . (phi or psi) implies rho

The first one allows us to use a different z for each x, while the second one requests the same z to be used for all x, right? So, can we indeed rewrite the formula in whatever order or do we need to start from the head? —Preceding unsigned comment added by 138.40.94.198 (talk) 13:58, 18 March 2009 (UTC)

Hmm, went in and changed the example, only to realise that it was (almost) correct - I've now detailed all the steps so that it's clear how the two forms are derived. My question was really about a case where the rho refers to x, so there z is bound by x. Then the exists z cannot move before the forall x.
An example with such a case would be nice: forall x ( Lovable(x) implies exists z (Loves(z,x) ) becomes forall x exists z ( Lovable(x) implies Loves(z, x) ), meaning that there's some z for each x, possibly different, but does not become exists z forall x ( Lovable(x) implies Loves(z, x) ), since the latter means that all Lovable x are loved by the same z (at least one).
Now, the question is - which is the rule which says that the first derivation is correct while the second is not?

Here is the sequence of three formulas you had:

forall x ( Lovable(x) implies exists z (Loves(z,x) )

forall x ( exists z ( Lovable(x) implies Loves(z, x) ))

exists z forall x ( Lovable(x) implies Loves(z, x) )

The problem with the last one is that you have moved the exists over the forall. The reason you cannot use the rules in the article to achieve this is that the top formula is not of the form $(\phi \to \exists z\rho )$, it is of the form $\forall x(\phi \to \exists z\rho )$ and there is no direct rule for a formula of the latter form that moves the exists to the front. It is sometimes possible to interchange the order of forall and exists quantifiers, such as if you start with $(\forall x\phi (x))\land (\exists y\psi (y))$. In that case both $\exists y\forall x(\phi (x)\land \psi (y))$ and $\forall x\exists y(\phi (x)\land \psi (y))$ equivalent formulas in prenex form. — Carl (CBM · talk) 01:01, 22 March 2009 (UTC)

first schemata

I don't understand the first schemata given as an example here. Isn't the quantifier on the far left in both forms? Are the parentheses important here? -- Creidieki 15:35, 21 November 2006 (UTC)

No, it isn't "on the far left" in both forms, and yes, parentheses are important here. --greenrd 03:12, 27 November 2006 (UTC)

Expansion of content

This page has scope for expansion in the following areas:

• A proof of the assertion that all formulas are logically equiv to some formula in PNF.
• A demonstration of how a formula can be 'converted' into PNF.

reetep 12:32, 1 December 2006 (UTC)

The work here outstrips the time available to do it. Even if you don't think it will be perfect, making a first set of edits yourself will probably draw others here to polish them up. CMummert 13:54, 1 December 2006 (UTC)

What do you mean when you say that the work required outstrips the time available? Wikipedia is a work in progress with no project deadlines. reetep 12:29, 4 December 2006 (UTC)

I mean that other people (like me) have also noticed that this article needs improvement, but such a large number of articles need improvement, relative to the amount of time per week that is spent editing them, that it may be a long time before articles like this get attention. So if you have some experience with this topic, and would like to see the article expanded, you can't do any harm by starting the improvements yourself. CMummert 13:17, 4 December 2006 (UTC)

The article is surprisingly silent on the issue of the equivalence connective. Although equivalence can first be translated into implications and conjunctions and then using the given rewrite rules, one usually wants to retain a similarity to the original formula when applying PNF rewrite rules. Is there are corresponding rule for equivalence? What are "typical" ways to deal with this issue? If it is to simply rewrite into implications and conjunction first, then this should probably be stated. The same could be said for implication, i.e. we could rewrite P -> Q into -P or Q and then apply the conversion rules for disjunction, whereupon we would NOT get back the implication symbol after the rewrite (as opposed to giving explicit rules as was done for implication).

Rules that do not hold in intuitionistic logic

Maybe we could add the list of the rules for converting a formula to prenex form that do fail in intuitionistic logic. I think that they are:

(1) $\forall x(\phi \lor \psi )$ implies $(\forall x\phi )\lor \psi$,

(2) $\forall x(\phi \lor \psi )$ implies $\phi \lor (\forall x\psi )$,

(3) $(\forall x\phi )\rightarrow \psi$ implies $\exists x(\phi \rightarrow \psi )$,

(4) $\phi \rightarrow (\exists x\psi )$ implies $\exists x(\phi \rightarrow \psi )$,

(5) $\lnot \forall x\phi$ implies $\exists x\lnot \phi$,

(x does not appear as a free variable of $\,\psi$ in (1) and (3); x does not appear as a free variable of $\,\phi$ in (2) and (4)). Jayme 10:41, 30 June 2007 (UTC)

First Example Not Correct?

We are told in the first section that:

"Every formula is equivalent in classical logic to a formula in prenex normal form. For example, if $\phi (y)$, $\psi (z)$, and $\rho (x)$ are quantifier-free formulas with the free variables shown then

$\forall x\exists y\exists z(\phi (y)\lor (\psi (z)\rightarrow \rho (x)))$

is in prenex normal form with matrix $\phi (y)\lor (\psi (z)\rightarrow \rho (x))$, while

$\forall x((\exists y\phi (y))\lor ((\exists z\psi (z))\rightarrow \rho (x)))$

is logically equivalent but not in prenex normal form."

Notice the second, non prenex'd expression

$\forall x((\exists y\phi (y))\lor ((\exists z\psi (z))\rightarrow \rho (x)))$

There is an existential quantifier in the implication. Accordingly, this would prenex to

$\forall x((\exists y\phi (y))\lor \forall z((\psi (z))\rightarrow \rho (x)))$

which further reduces to

$\forall x\forall z((\exists y\phi (y))\lor ((\psi (z))\rightarrow \rho (x)))$

and finally

$\forall x\forall z\exists y((\phi (y))\lor ((\psi (z))\rightarrow \rho (x)))$

Unfortunately, we are told that the second, non prenex'd expression is equivalent to the first, which is

$\forall x\exists y\exists z(\phi (y)\lor (\psi (z)\rightarrow \rho (x)))$

Which is not equivalent to the final prenex'd version of the second expression that I gave above.

Thus I believe either the first expression should be amended to

$\forall x\forall z\exists y((\phi (y))\lor ((\psi (z))\rightarrow \rho (x)))$

Or the second should be amended to

$\forall x((\exists y\phi (y))\lor ((\forall z\psi (z))\rightarrow \rho (x)))$

Let me know what you think. æntity 02:35, 8 March 2011 (UTC) — Preceding unsigned comment added by Aentity (talk • contribs)

Assumption of non-empty domain?

This isn't my specialty, but it seems to me that much of the discussion assumes at the outset that all variables have a non-empty domain. For instance, in the intuitionistic logic section, to say that

$(\exists x\phi )\rightarrow \exists y\psi$

is even classically equivalent to

$\exists y(\exists x\phi \rightarrow \psi )$

presupposes that it is known a priori that there exists a $y$ at all. Perhaps this is a common convention, but as someone with a stronger background in CS than logic, I was confused by this point. Luke Maurer (talk) 03:34, 7 October 2013 (UTC)

Good point. The axiom that the domain is inhabited is required for $\forall x(\phi \land \psi )\to (\forall x\phi )\land \psi$ and $(\exists x\phi )\lor \psi \to \exists x(\phi \lor \psi )$. I tried to find a logic textbook (an authoritative source) which mentions this explicitly, but to no avail. --Beroal (talk) 20:48, 29 October 2014 (UTC)

Inline citations are lacking

Seems strange to me that an article can make "B-class" when it has only one inline citation! So I'm going to add at least one more, viz., to Hinman's definition of PNF in the reference already given. But much more can be done to improve the article with inline citations. yoyo (talk) 16:20, 2 August 2018 (UTC)