I'm trying to solve the following exercise, which just seems to express a geometric system in terms of symbols. (I edited the exercise slightly)
Let $\mathcal{L}_{\text {inc }}$ be a first order language that consists of only relation symbols $\{P, L, I\}$ where $P$ and $L$ are unary relation symbols and $I$ is a binary relation symbol. An incidence structure $\mathfrak{A}$ is an $\mathcal{L}_{\text {inc }}$ -structure where the elements of $P^{\mathfrak{A}}$ are interpreted as points, elements of $L^{\mathfrak{A}}$ are interpreted as lines and $I^{\mathfrak{A}} \subseteq P^{\mathfrak{A}} \times L^{\mathfrak{A}}$ is the incidents relation. When $(p, l) \in I^{\mathfrak{A}}$ then we say point $p$ is incident with line $l$. Consider the following set of axioms:
(A0) $P^{2}$ and $L^{\mathfrak{A}}$ partitions the domain of $\mathfrak{A}$ i.e. every element of the domain is either a point or a line but not both;
(A1) Any two distinct points are incident with exactly one line;
Express $\mathrm{A} 0, \mathrm{~A} 1$ as $L_{i n c}$ -sentences.
Here is my solution:
$\mathrm{A} 0:\forall v(((P(v) \vee L(v)) \wedge (\lnot(P(v) \land L(v)))) .$
$\mathrm{A} 1:\forall v_{1}, v_{2}\left(\left(P\left(v_{1}\right) \wedge P\left(v_{2}\right)\right) \land \left(\exists v_{3}\left(L\left(v_{3}\right) \wedge I\left(v_{1}, v_{3}\right) \wedge I\left(v_{2}, v_{3}\right) \wedge\left(\left(\forall v_{4}\left(L\left(v_{4}\right) \wedge I\left(v_{1}, v_{4}\right) \wedge I\left(v_{2}, v_{4}\right)\right) \rightarrow\right.\right.\right.\right.\right.$ $\left.\left.\left.v_{3} \doteq v_{4}\right)\right)\right)$
The official solution is:
$\mathrm{A} 0:(\forall v(P(v) \vee L(v))) \wedge \forall v((P(v) \rightarrow \neg L(v)) \wedge(L(v) \rightarrow \neg P(v))) .$
$\mathrm{A} 1:\forall v_{1}, v_{2}\left(\left(P\left(v_{1}\right) \wedge P\left(v_{2}\right)\right) \rightarrow\left(\exists v_{3}\left(L\left(v_{3}\right) \wedge I\left(v_{1}, v_{3}\right) \wedge I\left(v_{2}, v_{3}\right) \wedge\left(\left(\forall v_{4}\left(L\left(v_{4}\right) \wedge I\left(v_{1}, v_{4}\right) \wedge I\left(v_{2}, v_{4}\right)\right) \rightarrow\right.\right.\right.\right.\right.$ $\left.\left.\left.v_{3} \doteq v_{4}\right)\right)\right)$
The question is, is my solution correct? I think A0 is correct, but I'm concerned about A1, especially because I used $\land$ instead of $\rightarrow$. If my solution is wrong, can you help me understand why? Thanks.
A0 looks good: it translates to "any v is either a point or a line and isn't both a point and a line"
A1 will not be true if $v_1$ or $v_2$ is a line.