Solving this coq exercise

Question

I'm learning COQ and I'm stuck on one of the book exercises. The book doesn't give me a solution so I don't know what to do. I've done the first one though. I have to translate these statements to predicate logic:

   h0 : Everybody knows somebody
   h1 : Nobody doesn't know anybody. 
   h2 : Everybody knows somebody 
   h3 : A footballer is known by everybody.
   h4 : Footballers only know footballers. 
   h5 : There is somebody who only knows one person.

Code:

Section Stadium.

Variable Fans : Set.
Variable Knows : Fans -> Fans -> Prop.
Variable Footballer : Fans -> Prop.

Hypothesis h0 : forall x: Fans, exists y: Fans, Knows x y.


End Stadium

.

Can you please help? Thank you so much!

Answer 1

I assume these definitions were provided to you, so "everybody" is represented by the members of Fans.

What are you stuck with?

For instance, h1 says that "nobody does not know anybody". What this boils down to is the fact that "it is not the case that someone does not know anyone". Now you have two ways to proceed:

1. You encode "someone does not know anybody" manually, and just negate it.

2. (or) You reuse h0, noticing that its negation is "someone does not know anybody".

---

To talk about footballers, you just verify that a variable x : Fans satisfy Footballer x ->. For instance, h3 would start like:

forall x, Footballer x -> (* here, you encode "everybody knows x" *)

---

Maybe h5 is a little bit harder. One way to encode "only one person" is to says that he knows one person p0, and that if he knows another person p1, then p1 = p0.

---

Without further details on what you find difficult, it is hard to provide you an helpful answer that is not the solution.