Is there a first-order sentence characterizing total orders with an order-automorphism with no fixed points?

Question

I'm interested in Boolean rings since they model classical logic well. If you take an infinite Boolean ring whose induced order is total and cut off the top and bottom elements, then you get the kind of total order described below.

I'm interested in total orders without endpoints equipped with an involution, i.e. the theory $T$ constructed as follows where $a < b$ is an abbreviation for $a \le b \land a \neq b$:

1. $\forall a \exists b \mathop. b \lt a$
2. $\forall a \exists b \mathop. a \lt b$
3. $\forall a \forall b \mathop. a \le b \land b \le a \to a = b$
4. $\forall a \forall b \forall c \mathop. a \le b \land b \le c \to a \le c$
5. $\forall a \forall b \mathop. a \le b \lor b \le a$
6. $a^{**} = a$
7. $(a \le b) \leftrightarrow (b^* \le a^*)$.

Some of these orders, like $(\mathbb{R}, \le)$ have order-automorphisms with no fixed points, e.g. $x \mapsto x + 1$.

Other orders, like the order associated with $\mathbb{R} + \{0, 1, 2\} + \mathbb{R}$, where $a + b$ means $a$ and then $b$ appear to have no such order-automorphisms. (Update: I originally wrote $\mathbb{R} \cdot 0 \cdot \mathbb{R}$, but updated it to be a correct example of an order whose automorphisms all have fixed points and to use standard notation based on comments in the answer by Noah Schweber.)

We can express the existence of such an autoomorphism in existential second-order logic (or, equivalently, by extending the language from $\{\le, *\}$ to $\{\le, f, *\}$) as follows:

$$ \exists f : D \to D \mathop. (\forall a \forall b \mathop. f(a) \le f(b) \leftrightarrow a \le b) \land (\forall a \mathop. f(a) \neq a) $$

However, I'm not sure whether we can express this property via a first-order sentence or not.

My question is twofold:

1. Is there a first-order sentence that picks out precisely the orders with an involution with no fixed points?
2. If there is no such sentence, is there a convenient way to show that no such sentence exists?

Answer 1

First, let me just answer the version of the question for linear orders (that is, without an involution specified). In fact, in my first read I missed that there were involutions involved at all, since you're only asking for order-isomorphisms!

By a back-and-forth argument, any two countable dense linear orders without endpoints ("DLOWEs" for short) are isomorphic. Now by downward Lowenheim-Skolem, this means that any two DLOWEs of arbitrary cardinality are elementarily equivalent: if $\mathfrak{A},\mathfrak{B}$ are DLOWEs then by dLS we get countable DLOWEs $\mathfrak{A}'\equiv\mathfrak{A}$ and $\mathfrak{B}'\equiv\mathfrak{B}$, but then $$\mathfrak{A}\equiv\mathfrak{A}'\cong\mathfrak{B}'\equiv\mathfrak{B}$$ finishes us off.

Since some DLOWEs do admit fixed-point-free automorphisms while others don't, this gives a negative answer to your question for linear orders.

What about linear orders with an involution? Well, the same basic idea will still apply, but it takes more work. You can show (via dLS + b-and-f, as above) that the theory $T$ of dense linear orders without endpoints with an involution which has a fixed point is complete, and the obvious countable model of this theory ($\mathbb{Q}$ with the involution $x\mapsto -x$) does admit fixed-point-free order order-automorphisms (e.g. $x\mapsto x+1$). So we just need to find a model of $T$ with no fixed-point-free order-automorphism. You claim an example of such in your post, but it doesn't work: $\mathbb{R}+{\bf 1}+\mathbb{R}\cong\mathbb{R}$.

Here's one way to do this. Let $\eta_1$ be an "$\aleph_1$-analogue" of the rationals; basically, $\eta_1$ is a linear order without endpoints which is isomorphic to its reverse and in which given any pair of countable sets $A,B$ with every element of $A$ below every element of $B$, there are $\aleph_1$-many points greater than every element of $A$ but less than every element of $B$. For now let's take it for granted that such an $\eta_1$ exists; they're not hard to build (do it in stages!) but it's not trivial.

Now consider the linear order $$(\eta_1\cdot \omega)+{\bf 1}+(\eta_1\cdot\omega^*).$$ Less snappily but more intuitively this is $$\eta_1+\eta_1+\eta_1+...{\bf 1}...+\eta_1+\eta_1+\eta_1,$$ and the key observation is that we're controlling cofinality of points. This has an obvious involution, but no fixed-point-free order-automorphisms since there is precisely one element which is "approachable by an $\omega$-sequence" (this is the cofinality feature suggested a sentence prior).