Expressing a geometric axiom in logic

62 Views Asked by At

This question is motivated by one of my previous questions, Basic geometry in logic. For convenience, I'll copy all the required content out in this question.

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$. Express $\mathrm{~A} 1$ as an $L_{i n c}$-sentence.

(A1) Any two distinct points are incident with exactly one line;

The official solution is given,

$\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)$.

Now, I was confused about how/why the meaning of 'distinct points' is expressed in the above sentence. When I attempted this exercise again, my solution looked like:

$\mathrm{A} 1:\forall v_{1}, v_{2}, \left(\left(P\left(v_{1}\right) \wedge P\left(v_{2}\right) \land (\lnot (v_1 = v_2))\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) \land (\lnot (v_4 = v_3)) \rightarrow \lnot(I(v_1,v_4) \land I(v_2,v_4)))\right) \right.\right.\right.\right.\right.$

Here, I thought the $(\lnot (v_1 = v_2))$ was needed to express 'any two distinct points'. Why is the official solution correct without this? Also, is my attempted solution correct?

1

There are 1 best solutions below

0
On BEST ANSWER

You are right, the official formulation is missing that important aspect of points being distinct. Your formulation expresses that well.