Can we ever use implication with an existential quantifier?

I am doing a class on logic and I was given the following question: Is this predicate a valid formalization of "some dogs are sleepy"?

The statement in question is

$\exists d \in Dogs: is\,a \,dog(d) \implies sleepy(d)$

now I know that the rule of thumb is that we should use the conjunction. My understanding of the question was that $is\,a\,dog(d)$ is a tautology based on the previous predicate bounding $d$ to $Dogs$. This would result in the following predicate:

$\exists d \in Dogs: True \implies sleepy(d)$

then this would be equivalent to:

$\exists d \in Dogs: sleepy(d)$

giving interpreting the resulting predicates gives the meaning: "some dogs are sleepy". Can modus ponens be used in predicate to infer that two predicates are equivalent, thus giving them the same meaning?

• It's a good idea to avoid using an existential quantifier on an implication statement. Consider that for any set $S$ and logical proposition $P$ we can prove, using ordinary set theory that $\exists x: [x\in S \implies P]$. This is a set-theoretic variation of the Drinkers' Paradox. See dcproof.com/DrinkersParadox.html – Dan Christensen Feb 22 '17 at 19:44
• @DanChristensen: the drinkers' paradox is entertaining and instructive, but it doesn't imply that existentially quantified implications are bad in any sense. Of course, the OP's "some dogs are sleepy" is not an existentially quantified implication. – Rob Arthan Feb 22 '17 at 23:34
• @RobArthan In writing mathematical proofs, alarm bells should go off if you are tempted to write anything of the form $\exists x:[x\in S \implies P]$. The implication should in all likelihood be a conjunction as in Mauro's example. That has been my experience having written maybe tens of thousands of lines of machine-verified formal proof over the years. Note that a universal quantifier on either an implication or conjunction would not present a problem. – Dan Christensen Feb 23 '17 at 3:28
• @DanChristensen: "It's a good idea to avoid blah blah blah" is not the same as "blah blah blah is often written by mistake for something else". Yes, if you write an existentially quantified implication you should check that it means what you really meant to say, but you shouldn't just say existentially quantified implications are a bad idea. – Rob Arthan Feb 23 '17 at 6:27
• @RobArthan I will be sure to revisit these opinions if I ever study constructive or intuitionistic logic. Thanks. – Dan Christensen Feb 24 '17 at 22:51

No, the correct formalization is:

$\exists d (Dog(d) \land Sleepy(d))$.

You can abbreviate it as :

$(\exists d \in Dogs) (Sleepy(d))$.

Why your proposal does not work ?

Because if we change "universe" and we move to that of $Men$, we have that

$\exists d (Dog(d) \land Sleepy(d))$

is false: no memeber of the universe is a dog and thus $Dog(x) \land Sleepy(x)$ is false for every value, while:

$\exists d (Dog(d) \to Sleepy(d))$

will be true, because $Dog(x) \to Sleepy(x)$ is vacuously true.

"Two predicate [logic formula]s are equivalent"

when they have always the same truth values (i.e. either both true or both false) where "always" means: in every possible interpretation.

• Thanks for you answer. I understand the vacuous truth brought by the implication. Every other universe will be true. Can we say that it is valid only for the specific universe $Dogs$? Also, to prove equivalence in predicate logic, do we need to prove that the result is always the same for every universe or can it be used on specific universes? – Justin Léger Feb 22 '17 at 20:01
• @JustinLéger - equivalence means $\vDash \varphi \leftrightarrow \psi$, i.e. true in every "universe". – Mauro ALLEGRANZA Feb 22 '17 at 20:04
• @MauroALLENGRANZA thanks for the clarification! – Justin Léger Feb 22 '17 at 20:06
• @MauroALLEGRANZA It seems to me that the OP's proposal does work if you assume $d\in Dogs \equiv isAdog(d)$. – Dan Christensen Feb 24 '17 at 22:34
• @DanChristensen - correct... But you cannot "assume" in the sense "it is implicit". You have to state a "definitional" axiom : $\forall d ( d \in Dogs \leftrightarrow isAdog(d))$. Math logic is formal: you cannot use "intuition". :-) – Mauro ALLEGRANZA Feb 25 '17 at 9:39

The notation you're using, $$\exists d \in Dogs: isAdog(d) \implies sleepy(d)$$ can be viewed as "syntactic sugar" for the expression $$\exists d ((d \in Dogs) \land (isAdog(d) \implies sleepy(d))).\tag1$$

Moreover, the name $isAdog$ seems superfluous, since apparently $isAdog(d) \equiv (d \in Dogs)$, and $(d \in Dogs)$ is just about as easy to write as $isAdog(d).$ So Predicate $1$ is equivalent to $$\exists d ((d \in Dogs) \land ((d \in Dogs) \implies sleepy(d))). \tag2$$

And then I think you are correct: $(d \in Dogs) \land ((d \in Dogs) \implies sleepy(d))$ can be replaced by $(d \in Dogs) \land sleepy(d)$ (or vice versa), so the Predicate $2$ is completely equivalent to $$\exists d ((d \in Dogs) \land sleepy(d)). \tag3$$

But why would you translate "some dogs are sleepy" into Predicate $1$ or Predicate $2,$ or even a disguised form of one of these predicates using the $\exists d\in Dogs$ notation, when you can instead write Predicate $3$?

If we really want to express "some dogs are sleepy" using an (slightly) excessively complex predicate with an implication, we could write

$$\exists d (\lnot((d \in Dogs) \implies \lnot sleepy(d))),$$

using the fact that $A \land B$ is equivalent to $\lnot(A\implies\lnot B).$

• How did you remove the implication from predicate 2 to predicate 3? – Justin Léger Feb 22 '17 at 20:13
• @JustinLéger How would you go about showing that $A \land (A\implies B)$ is equivalent to $A\land B$? That way. – David K Feb 22 '17 at 20:28

Is this predicate a valid formalization of "some dogs are sleepy"?

The statement in question is

$\exists d \in Dogs: isAdog(d) \implies sleepy(d)$

Assuming you meant $d\in Dogs \equiv isAdog(d)$, equivalent to your original statement would be:

$\exists d:[isAdog(d) \land [isAdog(d) \implies sleepy(d)]]$

Equivalent, too, would be:

$\exists d: [isAdog(d) \land sleepy(d)]$

(Proof left as an exercise.)

So, there is nothing wrong with your original statement, but I think you will agree this is a much more straightforward formalizing "some dogs are sleepy."

...now I know that the rule of thumb is that we should use the conjunction.

There is a good reason for that, especially in set theory (see my comments), but you actually have an existential quantifier on a conjunction.

My understanding of the question was that $isAdog(d)$ is a tautology based on the previous predicate bounding $d$ to $Dogs$. This would result in the following predicate:

$\exists d \in Dogs: True \implies sleepy(d)$

I am not familiar with this usage of "True."

...then this would be equivalent to:

$\exists d \in Dogs: sleepy(d)$

This, too, is equivalent to the original statement.

• "True" is just a sentence that is always true - you can think of it as a 0-ary predicate symbol (there are only two of these "true" $\top$ and "false" $\perp$). Meanwhile, I'm a bit confused: why do you respond to "we should use the conjunction" with "you actually have an existential quantifier on a conjunction" - isn't that what the OP wrote? – Noah Schweber Feb 24 '17 at 21:21
• @NoahSchweber The heading states, "Can we ever use implication with an existential quantifier?" He seemed to think that his original statement was an example of that. It isn't. – Dan Christensen Feb 24 '17 at 21:27
• That's not what I meant - I think you meant to write "you actually have an existential quantifier on an implication" (or "disjunction" since $a\implies b$ is $b\vee\neg a$). – Noah Schweber Feb 24 '17 at 21:28
• @NoahSchweber No, the original statement is equivalent to: $\exists d:[d \in Dogs \land[ isAdog(d) \implies sleepy(d)]]$. – Dan Christensen Feb 24 '17 at 21:58
• My point is that you seem to have written something like: "You think you want to use a conjunction, but you should use a conjunction." I'm just confused by the double-use of conjunction there; can you clarify what exactly you're correcting? – Noah Schweber Feb 24 '17 at 23:48