First Order Logic Inference. Proof of sentence.

Question

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

My Assumptions (Knowledge Base)

• John, Mary, Helen, George are the only members of Club1
  $\mathtt{Member(Club1,John) ∧ Member(Club1,Mary) ∧ -Member(Club1,Helen) ∧ Member(Club1,George)}$
  
  

• John is Mary's husband
  $\mathtt{Married(John,Mary)}$
  
  

• George is Helen's brother
  $\mathtt{Siblings(Goerge,Helen)}$
  
  

• The husband or the wife of each person is also a part of the same club
  $\mathtt{(∀x)(∀y)(∀s)(Married(x,y) \& Member(s,x) → Member(s,y))}$
  
  

My Goal (Φ)
Helen is not married
$\mathtt{(∀x)(¬(Married(x,Helen))}$

---

With common logic we can prove that Helen is not married. But the above assumptions can't prove my goal with propositional logic. I need to add my own assumptions, so that I can prove my goal.
What assumptions should I add to my Knowledge Base to prove φ ?

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

$\mathtt{(∀x)(∀y)(Siblings(x,y) \to -Married(x,y))}$
$\mathtt{(∀x)(∀y)(∀z)( Married(x,y) \to -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 prove my goal, but I can't find what else does it need to prove it.

Here is what I have done.

Answer 1

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))$

Answer 2

Finally , the answer :

and the proof: