There are two things I would like to prove.
- DLO – Dense linear order is complete, that means that when $\psi$ is a sentence of the language $\{<\}$ then $DLO\vDash\psi$ or $DLO\vDash\neg\psi$
- When $S$ is recurisvely enumerable and a complete set of axioms then $M:=\{\phi: S\vDash\phi\}$ is recursiv (i.e decidable=computable)
For 1. I do not have an idea. For 2. I use the fact that $M$ is recursively enumerable. Then I would like to argue (using the Church-Turing thesis) that in the case of complete theories the complement of $M$ is also recursively enumerable. Then I want to use the theorem that a set is recurisv if and only if the set and its complement are recursively enumerable.
Best Answer
DLO is not complete: The intervals $[0,1]$, $(0,1)$, $[0,1)$, and $(0,1]$ are all models of this theory and are not elementarily equivalent. On the other hand, these $4$ theories are the only possibilities:
It is a well-known theorem of Cantor that all countable models of DLO without end-points are isomorphic. This is typically proved using the back-and-forth technique. With this, it follows that if to DLO you add the sentence that says that there are no end-points, then you get a complete theory (using Lowenheim-Skolem, for example. One can think of this as a particular case of the fact that if $T$ is a countable theory that is $\kappa$-categorical for some infinite $\kappa$, and $T$ has no finite models, then $T$ is complete).
You can similarly see that the other three extensions of DLO (adding both endpoints, or only one) are complete. For example, any countable model of DLO+ "There are endpoints" looks like $\bullet+\mathbb Q+\bullet$, so any two countable models are isomorphic.
As for question 2, you have an algorithm for enumerating $S$. Using it, you can easily enumerate all consequences of $S$. The point is that if $\phi$ is provable from $S$, then for some $n$, $\phi$ is provable from the first $n$ axioms of $S$ with a proof that uses at most $n$ steps. Since $S$ is complete, eventually either $\phi$ or $\lnot\phi$ will appear listed this way. So you have a way of deciding whether $\phi$ is provable from $S$ or not (just wait until one of $\phi,\lnot\phi$ appears in your list of consequences). I agree this is a highly inefficient algorithm in practice.