First Order Logic Formula with quantifiers, needs some help

Question

Are these FOL formulae transformations correct?

Every doctor of Central Hospital has a badge

$\forall x \forall y$ $[Doctor(x) \land WorksIn(x,Central Hospital) \Rightarrow$ HasBadge(x,y)]

I think it is not. We need an $\exists y$ instead of $\forall y$ because is right that if x is a doctor and he works for Central he has a badge but the badge must be unique! Can't be true for every badge of the universe right?

Second:

Every baby with a mother has a parent

$\forall x \forall y \exists z [Baby(x) \land Mother(x,y) \Rightarrow Parent(x,z)]$

Same, i think that we would use the $\exists y$ since only one mother is a mother of a creature and it's not true that every element of the Domain is mother of x.

Many thanks

Answer 1

First one:

$$\forall x [\operatorname{Doctor}(x) \land \operatorname{WorksIn}(x,\text{CentralHospital}) \implies \exists y \operatorname{HasBadge}(x,y)]$$

Second one:

$$\forall x [\operatorname{Baby}(x) \land \exists y \operatorname{Mother}(x,y) \implies \exists z \operatorname{Parent}(x,z)]$$

Answer 2

Every doctor of Central Hospital has a badge

$\forall x \forall y~[\text{Doctor}(x) \land \text{WorksIn}(x,\text{[Central Hospital]}) \Rightarrow \text{HasBadge}(x,y)]$

I think it is not. We need an $\exists y$ instead of $\forall y$ because is right that if x is a doctor and he works for Central he has a badge but the badge must be unique! Can't be true for every badge of the universe right?

Correct. But more, you have to assert that $y$ is a badge.

$$\forall x~\exists y~((\operatorname{isDoctor}(x)\wedge \operatorname{WorksIn}(x,C))\to (\operatorname{isBadge}(y)\wedge \operatorname{Has}(x,y)))$$

Or you could merge the predicates. Either is acceptable, but consistency is best practice.

$$\forall x~\exists y~(\operatorname{isDoctorOf}(x,C)\to \operatorname{isBadgeOf}(y,x))$$

Every baby with a mother has a parent

$\forall x \forall y \exists z [Baby(x) \land Mother(x,y) \Rightarrow Parent(x,z)]$

Same, i think that we would use the $\exists y$ since only one mother is a mother of a creature and it's not true that every element of the Domain is mother of x.

No, you wish to affirm: "For any (x,y): if x is a baby and y is the mother of x, then x has a parent."

$$\forall x~\forall y~\exists z~[(\operatorname{isBaby}(x) \land \operatorname{isMotherOf}(y,x))\to \operatorname{isParentOf}(z,x)]$$

This Prenex form is equivalent to: "for every baby, the existence of a mother implies the existence of a parent." $$\forall x~[\operatorname{isBaby}(x)\to((\exists y~\operatorname{isMotherOf}(y,x))\to (\exists z~\operatorname{isParentOf}(z,x)))]$$

Answer 3

You're right that for the second one you should use a $\exists y$ rather than a $\forall y$.

The second is more tricky! The best thing to do is exactly what Kenny did, which is to introduce the quantifiers at the time they are referred to, instead of trying to put them all out at the front. So, as Kenny did:

$$\forall x [\operatorname{Baby}(x) \land \exists y \operatorname{Mother}(x,y) \implies \exists z \operatorname{Parent}(x,z)]$$

If you insist on taking the quantifiers out to the front, you need to be very careful, because the rules for these (called the Prenex Laws) are:

Prenex Laws

Where $x$ is not a free variable in $Q$:

$ \forall x \ P(x) \land Q \Leftrightarrow \forall x (P(x) \land Q)$

$ \forall x \ P(x) \land Q \Leftrightarrow \exists x (P(x) \land Q)$

$ \forall x \ P(x) \lor Q \Leftrightarrow \forall x (P(x) \lor Q)$

$\exists x \ P(x) \lor Q \Leftrightarrow \exists x (P(x) \lor Q)$

$\forall x \ Q \rightarrow P(x) \Leftrightarrow \forall x (Q\rightarrow P(x))$

$\exists x \ Q \rightarrow P(x) \Leftrightarrow \exists x (Q\rightarrow P(x))$

$\exists x \ P(x) \rightarrow Q \Leftrightarrow \forall x (P(x) \rightarrow Q)$

$\forall x \ P(x) \rightarrow Q \Leftrightarrow \exists x (P(x) \rightarrow Q)$

Notice in particular the last two equivalences, which show that if you take out a quantifier that is in the antecedent of an implication, then the quantifier changes into the other quantifier! So, if we apply these rules to Kenny's sentence, we get:

$$\forall x [\operatorname{Baby}(x) \land \exists y \operatorname{Mother}(x,y) \implies \exists z \operatorname{Parent}(x,z)] \Leftrightarrow$$

$$\forall x \forall y[\operatorname{Baby}(x) \land \operatorname{Mother}(x,y) \implies \exists z \operatorname{Parent}(x,z)] \Leftrightarrow$$

$$\forall x \forall y \exists z [\operatorname{Baby}(x) \land \operatorname{Mother}(x,y) \implies \operatorname{Parent}(x,z)] $$

...so you actually had it right the first place, and you should not change the $\forall y$ into a $\exists y$. But again, for readability sake, leaving the quantifiers on the inside makes it often more easier to translate in the first place.