1

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.

Tentative Models

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

Community
  • 1
Patrick Browne
  • 521
  • 2
  • 10

1 Answers1

2

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

user21820
  • 57,693
  • 9
  • 98
  • 256
  • Thank for your answer. I had not thought of a track with more than 2 cities. – Patrick Browne Dec 19 '19 at 15:24
  • 1
    @PatrickBrowne: Indeed that's why I said the problem was unclear, so it's not really your fault for not thinking of that possibility. I didn't either until I read (3). Feel free to ask to clarify any point, and then if you are satisfied with my answer you can accept it. =) – user21820 Dec 19 '19 at 15:31
  • Following your suggestions, I have updated my attempt. Any feedback would be welcome. – Patrick Browne Dec 22 '19 at 12:21
  • 1
    @PatrickBrowne: (1) to (3) are correct, and it's interesting how you had expressed uniqueness of objects that satisfy a property P, because it's not either of the two usual ways of doing it: (a) exists an object satisfying P such that every other object satisfying P is equal to it; (b) exists an object satisfying P, and every pair of objects satisfying P are equal. But your attempt for (4) is incorrect, and I think it's partly because of your non-systematic expressing of uniqueness. You might want to try that one again. =) – user21820 Dec 22 '19 at 16:32
  • I have made another attempt at part 4. – Patrick Browne Dec 28 '19 at 20:33
  • 1
    @PatrickBrowne: If I didn't make a mistake it's correct now based on the most grammatical interpretation of the English sentence. Yes you are right that there is an ambiguity in the English. Yours is the one that agrees most closely with the grammar, because of the comma. If the other interpretation was desired, it should have been phrased as "there is exactly one track U such that C lies on U and no city on T lies on U". – user21820 Dec 29 '19 at 11:53
  • 1
    Thanks for taking the time to look at my efforts. Your helpful answer and comments are much appreciated. – Patrick Browne Dec 29 '19 at 18:52