Showing that the theory DTO is consistent Toward the end of Kunen's Models of Set Theory section in his most recent Set Theory text, after talking about relativization, he begins to mention the idea of relative consistency proofs. I've been looking at the following exercise in this section.

Give a purely finitistic proof that the theory $DTO$ of dense total orders without first or last elements is consistent. Here, $\mathcal{L} = \{ < \}$.

There is a hint for the exercise: Give a purely finitistic definition of the notion $\mathbb{Q} \models \varphi[s]$, and then prove that $\mathbb{Q} \models \varphi$ whenever $\varphi$ is a sentence that is provable from $DTO$.  
Not working with consistency proofs before, nor seeing the theory $DTO$ anywhere in the previous sections of the text, I'm not entirely sure what to do. Also, what does he mean by "purely finitistic?" How would I go about giving a purely finitistic definition of $\mathbb{Q} \models \varphi[s]$? I would greatly appreciate it if anyone would be able to help me with this one. 
 A: We first define $\mathbb Q\models'\varphi[\sigma]$ by induction on the complexity of $\varphi$, for all $\sigma=(s_0,\ldots,s_n)$ such that $s_1\leq\ldots\leq s_n$; suitably rearranging the variables, as follows:
For atomic formulas let $\models'$ be the usual definition of satisfaction. The inductive step definitions for $\neg$ and $\wedge$ are the natural ones. 
The tricky thing is for the existencial formulas, so if $\varphi(\bar x)=\exists z\psi(z,\bar x)$, you define $\mathbb Q\models'\varphi[\sigma]$ iff $\mathbb Q\models'\psi[s_1-1,\sigma]$ or $\mathbb Q\models'\psi[\sigma,s_n+1]$ or $\mathbb Q\models'\psi[s_1,\ldots,s_i\frac{s_i+s_{i+1}}{2},s_{i+1},\ldots,s_n]$ for some $i<n$ or $\mathbb Q\models'\psi(s_i,\sigma)$ for some $i\leq n$; as $\models'$ has been defined for $\psi$.
From this you can now define $\mathbb Q\models'\varphi[\sigma]$, regardless of the order of $\sigma$.
Now, the key part of the exercise is to show that $\models'$ coincides with $\models$; the proof is not in a finitistic fashion, i.e., for all formulas $\varphi$ and all $\sigma$: $$\mathbb Q\models\varphi[\sigma]\text{ if and only if }\mathbb Q\models'\varphi[\sigma],$$
which you prove by induction on the complexity of $\varphi$:
If $\varphi$ is atomic, there is nothing to prove by our definition of $\models'$, and the inductive steps for $\neg$ and $\wedge$ are trivial. 
Now let us prove the case $\varphi(\bar x)=\exists z\psi(z,\bar x)$. 
The $(\Leftarrow)$ direction is clear by the inductive hypothesis. 
Now suppose $\mathbb Q\models\varphi[\sigma]$, then there is some $a\in\mathbb Q$ with $\mathbb Q\models\psi[a,\sigma]$. There exists some $b\in\{s_1-1,s_n+1\}\cup\{\frac{s_i+s_{i+1}}{2}:i<n\}\cup\{s_0,\ldots,s_n\},$ such that $b$ is ordered with respect to $s_0,\ldots,s_n$ as $a$ is to $s_0,\ldots,s_n$, then pick an isomorphism $f:(\mathbb Q,<)\longrightarrow(\mathbb Q,<)$ fixing all $s_0,\ldots,s_n$ and $f(a)=b$, then $\mathbb Q\models\psi[b,\sigma]$, thus by the inductive hypothesis $\mathbb Q\models'\psi[b,\sigma]$, and hence $\mathbb Q\models'\varphi[\sigma]$.

Now, the problem is to do this for an arbitrary $DLO$, $(A,<)$, without using choice. This can indeed be done using choice the same way as it was done for $(\mathbb Q,<)$, using instead of $s_1-1,\frac{s_i+s_{i+1}}{2},s_n+1; i<n$ some $a_0,a'_i,a_n\in A$ such that $a_0<s_0$, $s_i<a'_i<s_{i+1}$ and $s_n<a_n$, which exist as $(A,<)$ is a model of $DLO$. But I don't see whether there is a point of doing this with choice if the author asks for a finitistic proof.
A: DTO would refer to "dense linear orders without endpoints" as described in Wikipedia.  The axioms would be as follows:


*

*$( \forall x ) ( \neg x < x )$;

*$(\forall x ) ( \forall y ) ( \forall z ) ( ( x < y \wedge y < z ) \rightarrow x < z )$;

*$( \forall x ) ( \forall y ) ( x < y \vee x = y \vee y < x )$;

*$( \forall x ) ( \forall y ) ( x < y \rightarrow ( \exists z ) ( x < z \wedge z < y ) )$;

*$( \forall x ) ( \exists y ) ( y < x )$;

*$( \forall x ) ( \exists y ) ( x < y )$; 


I think that here "purely finitistic" refers to only ever making finitely many checks to see if a formula is true.
With this interpretation the basic idea is that given any formula $\varphi ( x , y , z )$ and rationals $a < b$, then for all $s,t$ which share the same relationship with both $a$ and $b$ we have that $\mathbb{Q} \models \varphi [ s,a,b ]$ iff $\mathbb{Q} \models [t,a,b]$: the model $\mathbb{Q}$ "cannot distinguish rationals within an interval".  So to check whether $\mathbb{Q} \models \exists x \psi$ it suffices to only check representatives in the intervals.
So let us finitistically define $\mathbb{Q} \models \varphi [ s_1 , \ldots , s_n ]$ for all $\varphi$.


*

*if $\varphi \equiv x = y$, then $\mathbb{Q} \models \varphi [ s , t ]$ iff $s = t$;

*if $\varphi \equiv x < y$, then $\mathbb{Q} \models \varphi [ s , t ]$ iff $s < t$;

*if $\varphi \equiv \neg \psi$, then $\mathbb{Q} \models \varphi [s_1 , \ldots , s_n ]$ iff $\mathbb{Q} \not\models \psi [ s_1 , \ldots , s_n ]$;

*if $\varphi \equiv \psi \wedge \theta$ then $\mathbb{Q} \models \varphi [ s_1 , \ldots , s_n ]$ iff $\mathbb{Q} \models \psi [ s_1 , \ldots , s_n ]$ and $\mathbb{Q} \models \theta [ s_1 , \ldots , s_n ]$;

*if $\varphi \equiv \exists x \psi$, then given $s_1 , \ldots , s_n \in \mathbb{Q}$ rearrange them as $s_1^\prime \leq \cdots \leq s_n^\prime$, then $\mathbb{Q} \models \varphi [ s_1 , \ldots , s_n ]$ iff at least one of the following holds:


*

*$\mathbb{Q} \models \psi [ s_1^\prime - 1 , s_1 , \ldots , s_n ]$;

*$\mathbb{Q} \models \psi [ s_1^\prime , s_1 , \ldots , s_n ]$;

*$\mathbb{Q} \models \psi [ \frac{s_1^\prime + s_2^\prime}{2} , s_1 , \ldots , s_n ]$;

*$\mathbb{Q} \models \psi [ s_2^\prime , s_1 , \ldots , s_n ]$;

*$\vdots$

*$\mathbb{Q} \models \psi [ \frac{s_{n-1}^\prime + s_n^\prime}{2} , s_1 , \ldots , s_n ]$;

*$\mathbb{Q} \models \psi [ s_n^\prime , s_1 , \ldots , s_n ]$;

*$\mathbb{Q} \models \psi [ s_n^\prime + 1 , s_1 , \ldots , s_n ]$;


(If $\varphi \equiv \exists x \psi$ where $\psi$ has no variables other than $x$  free, then $\mathbb{Q} \models \varphi$ iff $\mathbb{Q} \models \psi [ 0 ]$.)

Let us show that this works with the following axiom of DTO: $$( \forall x ) ( \forall y ) ( x < y \rightarrow ( \exists z ) ( x < z \wedge z < y ) )$$ which is logically equivalent to $$ \neg ( \exists x ) ( \exists y ) ( x < y \wedge \neg ( \exists z ) ( x < z \wedge z < y ) ) ).$$


*

*$\mathbb{Q} \models \neg ( \exists x ) ( \exists y ) ( x < y \wedge \neg ( \exists z ) ( x < z \wedge z < y ) ) )$ iff

*$\mathbb{Q} \not\models ( \exists x ) ( \exists y ) ( x < y \wedge \neg ( \exists z ) ( x < z \wedge z < y ) ) )$ iff

*$\mathbb{Q} \not\models ( \exists y ) ( 0 < y \wedge \neg ( \exists z ) ( 0 < z \wedge z < y ) ) )$ iff

*each of the following are true

*

*$\mathbb{Q} \not\models ( 0 < -1 \wedge \neg ( \exists z ) ( 0 < z \wedge z < -1 ) ) )$;

*$\mathbb{Q} \not\models ( 0 < 0 \wedge \neg ( \exists z ) ( 0 < z \wedge z < 0 ) ) )$;

*$\mathbb{Q} \not\models ( 0 < 1 \wedge \neg ( \exists z ) ( 0 < z \wedge z < 1 ) ) )$;



Look at these three separately:


*

*$\mathbb{Q} \not\models ( 0 < -1 \wedge \neg ( \exists z ) ( 0 < z \wedge z < -1 ) ) )$ iff $\mathbb{Q} \not\models 0 < -1 $ or $\mathbb{Q} \not\models \neg ( \exists z ) ( 0 < z \wedge z < -1 ) ) )$, which is true since $\mathbb{Q} \not\models 0 < -1$.

*$\mathbb{Q} \not\models ( 0 < 0 \wedge \neg ( \exists z ) ( 0 < z \wedge z < 0 ) ) )$ iff $\mathbb{Q} \not\models 0 < 0 $ or $\mathbb{Q} \not\models \neg ( \exists z ) ( 0 < z \wedge z < 0 ) ) )$, which is true since $\mathbb{Q} \not\models 0 < 0$.

*$\mathbb{Q} \not\models ( 0 < 1 \wedge \neg ( \exists z ) ( 0 < z \wedge z < 1 ) ) )$ iff either $\mathbb{Q} \not\models 0 < 1$ or $\mathbb{Q} \not\models \neg ( \exists z ) ( 0 < z \wedge z < 1 )$ iff (since $\mathbb{Q} \models 0 < 1$) $\mathbb{Q} \not\models \neg ( \exists z ) ( 0 < z \wedge z < 1 )$ iff $\mathbb{Q} \models ( \exists z ) ( 0 < z \wedge z < 1 )$ iff at least one of the following is true


*

*$\mathbb{Q} \models 0 < -1 \wedge -1 < 1$;

*$\mathbb{Q} \models 0 < 0 \wedge 0 < 1$;

*$\mathbb{Q} \models 0 < \frac 12 \wedge \frac 12 < 1$;

*$\mathbb{Q} \models 0 < 1 \wedge 1 < 1$;

*$\mathbb{Q} \models 0 < 2 \wedge 2 < 1$;


and the third one is clearly true.
