# First Order Logic Inference , Proof of sentence

I need to find a proof for my goal , given some assumptions. The assumptions and the goal were translated from english sentences.

My assumptions(KB)

John ,Mary,Helen,George are the only members of club1:

-Member(Club1,John) ∧ Member(Club1,Mary) ∧ -Member(Club1,Helen) ∧ Member(Club1,George)


John is Mary's husband.

-Married(John,Mary)


George is Helen's brother.

-Siblings(Goerge,Helen)


The husband or the wife of each person is also a part of the same club

- (∀x)(∀y)(∀s)(Married(x,y) & Member(s,x) → Member(s,y))


My Goal(Φ)

Helen is not married.

- (∀x)(¬(Married(x,Helen)).


With common logic we can prove that helen (being ethical and not incest) , is not married. But the above assumptions , can't prove my goal with propotitional logic. I need to add my own assumptions , so that I can prove my goal. What assumptions should I add to my KB to prove φ.

I tried the following ones , but they are not enough:

(∀x)(∀y)(Siblings(x,y) -> -Married(x,y)).
(∀x)(∀y)(∀z)( Married(x,y) -> -Married(x,z) & -Married(y,z)).


The above assumptions , tells that if two atoms are siblings then they can't be marry each other and if they can't marry more than one person. I am using prover9 , to also prove my goal , but I can't find what else does it need , to prove it.

EDIT 1 So , far , what I have done enter image description here

• Another rule is missing: not member if different of Helen, ... – pasaba por aqui Jan 12 '17 at 20:24
• @MauroALLEGRANZA The OP tried to say that one cannot marry more than one person with the last sentence but didn't do a very good job ... – Bram28 Jan 12 '17 at 20:32

You also need:

$\forall x (Member(Club1,x) \rightarrow (x = John \lor x = Mary \lor x = Helen \lor x = George))$

Since these four are the only members of the club, i.e. there are no others!

Also, let's make sure they are all different people:

$John \not = Mary$

$John \not = Helen$

$John \not = George$

$Mary \not= Helen$

$Mary \not = George$

$Helen \not = George$

Also, I think the puzzle assumes no gay marriage, so:

$\forall x \forall y ((Male(x) \land Married(x,y) \rightarrow Female(y))$

$\forall x \forall y ((Female(x) \land Married(x,y) \rightarrow Male(y))$

And so you'll also want to add:

$Male(John)$

$Female(Mary)$

$Female(Helen)$

$Male(George)$

$\forall x (Male(x) \leftrightarrow \neg Female(x))$

Finally, your last sentence where you try to say that someone cannot be married to more than one person isn't correct; it should be:

$\forall x \forall y \forall z (Married(x,y) \color{red}{ \land z \not = y}) \rightarrow \neg Married(x,z))$

and to use that, you'll probably also need:

$\forall x \forall y (Married(x,y) \rightarrow Married(y,x))$

• Still can't find a solultion... :/ – Social Programmer Jan 12 '17 at 21:09
• Oh! You should add that they are all different people, since in logic, just because you have different constant symbols does not mean they denote different objects. I'll add that to my post. – Bram28 Jan 12 '17 at 21:38
• Still no answer , should I post a picture of what i have done so far ? – Social Programmer Jan 12 '17 at 22:05
• @SocialProgrammer yeah, go ahead and show what you have. – Bram28 Jan 12 '17 at 22:15
• here you go brother – Social Programmer Jan 12 '17 at 22:23

Finally , the answer : enter image description here

and the proof: enter image description here

• @Bram28 Answer is up ! – Social Programmer Jan 12 '17 at 23:03
• Looks good! looks like the prover is using some kind of resolution. – Bram28 Jan 12 '17 at 23:26
• Yeah. Anyways , thanks a lot bram. Can i add you as a friend ? – Social Programmer Jan 12 '17 at 23:31
• I don't think this site has a friends feature, but if you ever have another problem you know how to reach me! – Bram28 Jan 12 '17 at 23:36
• Ok , I am new here , goodnight sir – Social Programmer Jan 12 '17 at 23:38