[Math] First Order Logic Question – “All cats either love or hate dogs.”

first-order-logiclogicnotation

Given the following set of predicates:

$$\{cat(x), dog(x), love(x, y), hate(x, y)\}$$

How would you transform the following English statement into First Order Logic…

Statement: "All cats either love or hate dogs."

I came up with two possible ways to represent the statement, I am leaning towards the first, but I can also see the second being correct. Can someone give me some reasoning why one would be more correct than the other?

$$ \forall x \forall y (cat(x) \implies dog(y) \land [love(x, y) \lor hate(x, y)]) $$

$$ \forall x \forall y (cat(x) \land dog(y) \implies [love(x,y) \lor hate(x,y)])$$

Best Answer

Neither of your suggestions captures the meaning I get from the original sentence.

However, the second one is the most wrong. It will be true as soon as there exists anything that is not a dog. Namely, no matter what $x$ is, you can choose the non-dog to be $y$, and then ${\rm cat}(x)\land{\rm dog}(y)$ will be false, which automatically makes the entire implication true.

The first one is better, but what it says is that every cat either loves or hates some dog. I would understand the sentence in the problem as saying that every cat belongs to one of two types: those that hate all dogs, and those that love all dogs. And that's not what your suggestion expresses.

Related Solutions

[Math] How to translate the following sentences into first order logic

Edit: The question was updated; this answer refers to the original posting.

You haven't specified the meanings of Howl, Have, etc. I have made the most charitable assumptions, but if I'm wrong you may need to make some changes (for instance, if "Howl" doesn't have "at night" baked in).

This is probably fine.
Your two options are logically equivalent, and they're logically equivalent to how I would translate it, but my personal preference would be for something like $\forall x\left((\exists y(\ldots))\to\ldots\right)$. Even though it's equivalent, the phrasing "has any cats" makes me think of an embedded $\exists y$.
Your answers are odd because the sentence says "have" but you don't use the $\mathrm{Have}(x,y)$ construction.
This is close, but your FOL form is false in a world with no cats at all, even though "Peter has either a cat or a dog" could still be true if he has a dog.
This is probably fine.

Translating from First Order Logic to Order-Sorted Logic

I don't know about the OSA system specifically. However, here's a proof that I wrote up in Coq using types. Most of the length of this is just the setup, then the actual proof becomes very short.

Parameters Horse Dog Greyhound Rabbit Animal : Type.
Parameter Horse_inc_Animal : Horse -> Animal.
Parameter Dog_inc_Animal : Dog -> Animal.
Parameter Greyhound_inc_Dog : Greyhound -> Dog.  (* 3a *)
Parameter Rabbit_inc_Animal : Rabbit -> Animal.

Coercion Horse_inc_Animal : Horse >-> Animal.
Coercion Dog_inc_Animal : Dog >-> Animal.
Coercion Greyhound_inc_Dog : Greyhound >-> Dog.
Coercion Rabbit_inc_Animal : Rabbit >-> Animal.

Parameter Faster : Animal -> Animal -> Prop.

Axiom stmt_1a : forall (x : Horse) (y : Dog),
  Faster x y.
Axiom stmt_2a : exists y : Greyhound,
  forall z : Rabbit, Faster y z.
Axiom stmt_4a : forall x y z : Animal,
  Faster x y -> Faster y z -> Faster x z.

Parameter Harry : Horse. (* 5a *)
Parameter Ralph : Rabbit. (* 6a *)

(* Main result... *)
Goal Faster Harry Ralph.
Proof.

(* existential elimination on (2a) *)
destruct stmt_2a as [g].

(* specialization of (4a), and also implicitly applies ->E (modus ponens)
   a couple of times *)
apply stmt_4a with (y := g).

(* Subgoal: Faster Harry g,
   proved by specializing (1a) *)
+ apply stmt_1a.

(* Subgoal: Faster g Ralph,
   proved by specializing the statement
   H : forall z : Rabbit, faster g z
   gotten from the existential elimination *)
+ apply H.
Qed.

Again, I don't know how much this would help in constructing a proof in your particular system - I'm just posting in the hopes that it might be close enough to be of some help. (Do keep in mind that Coq is often oriented towards top-down programming of a proof, as in this case, whereas Fitch-style systems are often closer to bottom-up serializations of the same proof term.)

Best Answer

Related Solutions

[Math] How to translate the following sentences into first order logic

Translating from First Order Logic to Order-Sorted Logic

Related Question