Represent the following sentences in first order logic.

discrete mathematicsfirst-order-logiclogicpredicate-logicpropositional-calculus

Q) Represent the following sentences in first order logic is this the right?

1) John is intelligent than all other student in his class.

FOL: ∀X∶Student(X)→Intelligent(john,X)

2) Neiher Alex nor John is unhappy.

FOL: ¬(happy(alex) ∨ happy(john))

3) Some dogs are domestic pets. (which one is correct)

FOL: i) ∃X∶Dog(X)→DomesticPets(X) (or)

ii) ∃X∶(Dogs(X) ∧ DomesticPets(X))

4) Some turtles are faster than rabbits.

FOL: ∃X∶Turtle(X) ∧ Rabbit(Y)→faster(X,Y)

Best Answer

Some dogs are domestic pets. Should be the second one $$ ∃X∶\text{Dogs(X)} ∧ \text{DomesticPets(X)}$$ To see why it's not the first one, apply distributive law of $\exists$ over $\to$ we have \begin{align} &∃X∶\text{Dog(X)}→\text{DomesticPets(X)}\\ \equiv&\forall X:\text{Dog(X)}→\exists X:\text{DomesticPets(X)} \end{align} It basicly means if everything are dog, then something is a DomesticPet, clearly isn't what we want to say.
Some turtles are faster than rabbits. Same mistake: \begin{align} &∃X∶\text{Turtle(X)} ∧ \text{Rabbit(Y)}→\text{faster(X,Y)}\\ \equiv&\forall X∶\text{Turtle(X)} ∧ \text{Rabbit(Y)}→\exists X:\text{faster(X,Y)} \end{align} That is if everything are Tutle and $Y$ is Rabbit, then $\dots$ just make no sense. Instead we write $$\exists X:\text{Turtle(X)} ∧ \forall Y:\text{Rabbit(Y)}\to\text{faster(X,Y)}$$ This is some Turtle faster than all the rabbits.

Related Solutions

[Math] How to represent the following sentences in first-order logic

Let me address the first three sentences (since they form a maximal coherent collection of sentences).

We have a use for the following five predicates:

$\mathsf{Student}(x)$: $x$ is a student;
$\mathsf{French}(y), \mathsf{Greek}(y)$: $y$ is the course in French, resp. Greek;
$\mathsf{Take}(x,y)$: $x$ (student) takes $y$ (course);
$\mathsf{Pass}(x,y)$: $x$ (student) passes $y$ (course);
$\mathsf{TakeInSpring2001}(x,y)$: $x$ (student) takes $y$ (course) in Spring 2001.

Now we can formulate the sentences as follows:

a) $\exists x\exists y: \mathsf{Student}(x) \land \mathsf{French}(y) \land \mathsf{TakeInSpring2001}(x,y)$

b) $\forall x\forall y: (\mathsf{Student}(x) \land \mathsf{French}(y) \land \mathsf{Take}(x,y)) \implies \mathsf{Pass}(x,y)$

c) $\exists x\exists y\forall z: \mathsf{Student}(x) \land \mathsf{Greek}(y) \land \mathsf{TakeInSpring2001}(x,y) \land ((\mathsf{Student}(z) \land \mathsf{TakeInSpring2001}(z,y))\implies x = z)$

The other five shouldn't be hard once one understands the above three. A different approach would be to use more specific predicates (e.g. $\mathsf{FrenchInSpring2001}(x)$ as suggested in the comments), but that would defeat the "consistent vocabulary" requirement of the question IMO.

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 represent the following sentences in first-order logic

Translating from First Order Logic to Order-Sorted Logic

Related Question