I have to prove that the set of the following formulas is satisfiable
$$ \forall x \forall y(p(x,y) \&p(y,x)) \implies x=y \\ \neg\forall x (p(x,x)) \\ \forall x \exists y \exists z(p(x,y) \&p(z,x)) \\ \neg \forall x \forall y(\neg p(x,y) \lor \neg p(y,x)) $$
What I have so far is the following:
$\mathscr A =<A,\sigma,I>$ where $\mathscr A$ is a structure, A is the domain of discourse, $\sigma$ is the signature and I is the interpretation function.
I've drawn a graph from which I've the following tuples for the predicate p:
$\{(a,d), (b,a),(c,a),(c,b),(c,c),(d,c),(d,b),(d,d)\}$ where a,b,c,d are constant symbols.
My question is how can I best describe my solution rigorously and formally? How does the interpretation function I is defined for the following structure?
Thanks in advance!
As Mauro says, $a,b,c,d$ are not constant symbols, but objects that are elements from your domain. And your set of tuples is $I(p)$ or $p^I$.
And yes, your interpretation is indeed a model of the set of sentences. Hence, the set of sentences is satisfiable.