Using semantic tableaux to prove a situation can occur

Question

I am having a wedding and want to prevent fights at the wedding. suppose the following:

1. John will attend if mark or Aston attends.
2. Aston attends if Mark does not Attend
3. If Aston attends, john will not.

use semantic tableaux to prove that if Mark and John but not Aston attends, there will be no fights at the wedding.

So I have broken up the problem into variables:
J = John attends
M = Mark attends
A = Aston attends

So I have to satisfy the following situations $M \to J, A \to J, \lnot M \to A, A \to \lnot J$

My attempt was:

prove { $M \to J, A \to j, \lnot M \to A, A \to \lnot J$} $\vDash (M \land J \land \lnot A)$

to prove this we show:

$(M \to J) \land (A \to J) \land (\lnot M \to A) \land (A \to \lnot J) \vDash \lnot (M \land J \land \lnot A)$ is unsatisfiable

However my prove turned out to be satisfiable. So now I am wondering that the initial setup of my solution is wrong. Is my setup correct according to the problem or am I making false assumptions?

Answer 1

I think you may be confused, you need to show that $(M \land J \land \lnot A)$ is satisfiable (which you said you did). Remember, you prove the negation is unsatisfiable only if you are checking to see if the original formula is valid or not. In this case you are not looking for validity, just that the above claim is satisfiable.

Also you do not want to use $(M \land J \land \lnot A)$ for you tableaux proof. Instead use $((M \lor A) \to J) \land (\lnot M \to A) \land (A \to \lnot J)$. Hope this helps