Is the following predicate logic formula a contradiction?

Question

I have this predicate logic formula:

$(\forall x)(\forall y)(\forall z)((p(x,y)\land p(y,z))\rightarrow p(x,z))\land(\forall x)\neg p(x,x)\land\neg((\forall x)(\forall y)(p(x,y)\vee (x=y)\vee p(y,x))$

You can notice that the first formula of a conjunction is an axiom for transitivity, the second one is an axiom for ireflexivity and the third one is a negation of a formula for linearity. I want to find out wheter the formula for linearity is a logical consequence of those two axioms.

Therefore I wonder - Is this formula a contradiction? I am not able to do a semantic tree for this formula to find it out.

Answer 1

The formula is satisfiable.

Consider an interpretation $\mathscr I$ with domain $\mathscr D = \{ a,b,c \}$ and interpret the binary predicate symbol $p(x,y)$ with the relation $p^{\mathscr I} = \{ (a,b), (a,c) \}$.

Answer 2

One relation satisfying your formula is: $x$ is a proper divisor of $y$.

Clearly that relation is transitive and irreflexive (the latter is what “proper“ means here), but not linear (e.g. of two different primes, none is a proper divisor of the other).