I have a language $L=\{P\}$ with equation, where $P$ is binary predicate symbol. Language's formulas are:
$\varphi \equiv \forall x \forall y (\neg P(x,x) \land (P(x,y) \to P(y,x)))$,
$\psi \equiv \forall x \exists y \exists z(y\ne z \land P(x, y) \land P(x,z) \land \forall v (P(x,v) \to (v=y \lor v =z )))$
and for every $n \in N^+$
$\xi_n \equiv \exists x_1 \exists x_2 ... \exists x_n (\bigwedge \limits _{i=1}^{n-1}P(x_i, x_{i+1}) \land \bigwedge \limits _{i=1 }^{n}\bigwedge \limits _{j=i+1}^{n} x_i \ne x_j)$
I'm trying to prove that theory $T=\{\varphi,\psi\} \cup \{\xi_n | n \in N^+\}$ is complete and is not contradictory.
But still with no success. Could somebody suggest me some flow of proof?
This theory axiomatizes the class of graph of degree $2$ such that for all positive integers $n$ there exists a path of length $n$. Needless to say, such a graph has to be infinite to satisfy the last condition.
To prove that the theory is not contradictory, it suffices to come up with a model. An example of a model is the infinite path on $\mathbb Z$ where $P$ is the successor predicate.
The theory is not complete, however. Consider the structure $(\mathbb Z, s)$ of the integers with successor and add three new points $a,b,c$ that form a triangle for the predicate $P$, and are disjoint from the rest of the structure. This is again a 2-regular graph that satisfies all the $\xi_n$, thus it is a new model that is not elementarily equivalent to the former one.