How to decide whether a logical formula is satisfiable

Question

I'm trying to solve one logical problem. I have Language L={P} with equality (there can be '='). And we have 4 formulas an theories of this language.

We have to decide, for each formula, whether it is satisfiable.

These are formulas: $$ A: \exists{x,y,z}; \hspace{1cm} (x \ne y) \land(x \ne z) \land (y \ne z)\\ B: \forall{x,y}; \hspace{1cm} P(x,y)\\ C: \forall{x},\exists{y}; \hspace{1cm} P(x,y)\\ D: \exists{y},\forall{x}; \hspace{1cm} P(x,y) $$

and theories:

$$ T_1: \{A,B\}\\ T_2: \{A,C,\neg{D}\}\\ T_3: \{A,\neg{C},D\}\\ $$

I've probably solved T1 and T2 but I can't solve T3.

So:

T1: The formula A forces that there must be at least 3 atoms in universum. So I've chosen this universum: $\{1,2,3\}$ and the Predicate $P(x,y): (x=y) \lor (x \ne y)$

T2: The same thing: universum: $\{1,2,3\}$ and the $P(x,y): x \equiv 0 \hspace{2mm}(\bmod y)$

T3: $\neg{C}: \nexists{x},\exists{y}; P(x,y): \exists{x},\forall{y}; \neg P(x,y)$

Now I'm lost. I can't find any model but I can't decide and prove that this Theory is not satisfiable.

Could you help me?

Answer 1

Suppose both $\neg C$ and $D$, where: $$\begin{align} \neg C &\iff \exists x\, \forall y \,\neg P(x,y) \\ D &\iff \exists y\, \forall x\, P(x,y). \end{align}$$ By $\neg C$, there's some $x_0$ such that $$\forall y \,\neg P(x_0,y).\tag{1} $$ By $D$, there's some $y_0$ such that $$\forall x\, P(x,y_0).\tag{2} $$ Instantiating (1), we have $\neg P(x_0, y_0)$; instantiating (2), $P(x_0, y_0)$: contradiction.

So T3 is inconsistent.