Suppose that, in first-order logic, I need to consider an ordered structure (such as time instants or ordered field). I begin with a binary predicate $≺$ to express the order:
$x ≺ y: x$ strictly precedes $y$.
And I impose the axioms of the total linear order:
$\forall x\neg(x ≺ x)$
$\forall x\forall y(x ≺ y \rightarrow \neg(y ≺ x)) $
$\forall x \forall y \forall z(x ≺ y ˄ y < z \rightarrow x ≺ z)$
$ \forall x \forall y(x = y ˅ x ≺ y ˅ y ≺ x)$
Now, I read that intervals can be defined as ordered couples, in such a way that intuitively $⟨x, y⟩$ is the interval that begins in x and ends in y. But I don't understand how to do this formally. What options there are to define the ordered couples in the object language?
My idea is that I need to introduce an unary predicate I for intervals and two unary function symbols b and e to express respectively the beginning and end-point of the intervals. So:
$I(x): x$ is an interval
$b(x):$ the beginning point of $x$
$e(x):$ the ending point of $x$
and say:
$\forall x\forall y(x ≺ y \rightarrow \exists z(I(z) ˄ b(z) = x ˄ e(z) = y))$
Is this enough? Or I need to introduce sets in the domain of discourse to say that $⟨x, y⟩$ is by definition equal to $\{\{x\}, \{x, y\}\}$? I'm confusing...
Thanks
Some of your choice as to how to formalize this will depend on how you are going to use this, and what you are trying to prove about it. But, why not use a 2-place function symbol $int(x,y)$ that takes $x$ and $y$ and 'returns' an interval $<x,y>$?
Or, maybe use a 3-place predicate $Int(x,y,z)$ that says that $z$ is the interval $<x,y>$. So then you could do:
$$\forall x \forall y \forall z (Int(x,y,z) \rightarrow x < y)$$
to ensure that for an interval $<x,y>$ you indeed have $x<y$