I am trying to express the following axiomatic system (theory) in the language of typed first order logic (FOL).
There are at least two cities. For any two distinct cities, there is exactly one track connecting them. No train track connect all cities. Given any track T and any city C not on T, there is exactly one track on which C lies, but none of the cities on T are on this track.
Below is my attempt. I used the predicate $track(x,y)$ which is true when there is a track from $x$ to $y$ :
1. There are at least two cities.
$\exists x,y:City (x \neq y)$
2. For any two distinct cities, there is exactly one track connecting them (using left and right uniqueness)
$\forall x,z,w:City ((x \neq w) \land (x \neq z) \land ((track(x,z) \land track(x,w)) \Rightarrow (w = z)) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \land ((track(z,x) \land track(w,x)) \Rightarrow ( w = z))) $
3. No track connects all cities.
$\neg \exists x:City (\forall y:City \bullet track(x,y))$ (Not sure about this!)
4. Given any track T and any city C not on T, there is exactly one track on which C lies, but none of the cities on T are on this track.(using unique existential)
$\forall x,y,c:City ((track(x,y) \land(c \neq x) \land (c \neq y )) \Rightarrow (\exists k, \forall j:City (track(c,k) \land (k \neq x) \land (k \neq y)) \Rightarrow(j = k)))$
EDIT: new attempt at formalisation
Taking into account the suggested solution the tentative models of this theory consist of one or more distinct tracks (or connections) as in Model 1 or possibly more than one city per track Model 2. I will have to reconsider my solution from scratch.
Here is a new formalisation following suggestions from user21820
1 There are at least two cities.
$\exists x,y:City : (x \neq y)$
2 For any two distinct cities, there is exactly one track connecting them.
$\forall c1:City, \forall c2:City : (c1 \neq c2) \Rightarrow (\exists t1:Track, \forall t2:Track : (CityOnTrack(c1,t1) \land CityOnTrack(c2,t1)) \Leftrightarrow (t1 = t2)))$
3 No track connects all cities.
$\forall t:Track, \exists c:City : \neg(CityOnTrack(c,t)))$
4 Given any track T and any city C not on T, there is exactly one track on which C lies, but none of the cities on T are on this track,
\begin{align*} \forall c:City ,\forall t:Track : &(\neg CityOnTrack(c,t) \Rightarrow \\ &((\exists t2:Track : CityOnTrack(c,t2) \land \\ &(\forall c2:City :(CityOnTrack(c2,t) \Rightarrow \neg CityOnTrack(c2,t2))) \land \\ &(\forall t3:Track,\forall t4:Track, (CityOnTrack(c,t3) \land CityOnTrack(c,t4))))\Rightarrow (t3=t4))). \end{align*} For 4 I am not sure if the FOL for "none of the cities on T are on this track" is correct or is in the correct position. Also, as suggested by user21820, I have used the third of the four definitions of unique existential from Wikipedia.
Question
Is this new formalisation correct?
The original problem is from A TeXas Style Introduction to Proof (page 124).
The problem as stated was very unclear, to the point that you misinterpreted what you were required to express. From (3) I guess that a track is not merely a city-to-city connection, but rather a whole long 'line' with some cities on it, possibly more than $2$. So you need to have two types, one for cities and one for tracks. And you would need a predicate to express "city C is on track T". Here are English renderings suitable for translation to FOL:
(1) Fine in the new interpretation.
(2) For every cities X,Y, if they are different then there is a unique track T such that X,Y are both on T.
(3) There is no track T such that every city X is on T.
(4) I'll leave this one to you.
(By the way, colon is an acceptable standard symbol for the typing of quantified objects, but I do not think the big black dot is a standard convention.)