STRONG COMPLETENESS OF A FIRST-ORDER TEMPORAL LOGIC FOR REAL TIME

Abstract

Propositional temporal logic over the real number time flow is finitely axiomatisable, but its first-order counterpart is not recursively axiomatisable. We study the logic that combines the propositional axiomatisation with the usual axioms for first-order logic with identity, and develop an alternative “admissible” semantics for it, showing that it is strongly complete for admissible models over the reals. By contrast there is no recursive axiomatisation of the first-order temporal logic of admissible models whose time flow is the integers, or any scattered linear ordering.

1. Introduction

A set of formulas is called recursively axiomatisable if it is the set of theorems of some deductive system that has a recursive set of axioms and a recursive set of proofs [3, sec. 7]. For instance, if the flow of time is modelled by the linearly ordered set $(\mathbb {R},<)$ of real numbers, then in the temporal language of Prior’s connectives $\mathbf {G}$ (‘always in the future’) and $\mathbf {H}$ (‘always in the past’), the resulting logic of valid propositional formulas is recursively axiomatisable. This was shown by Bull [2], using finitely many axioms and inference rules.

The situation of first-order temporal logic is quite different. Dana Scott proved in the 1960s that the Priorean logic of first-order temporal models over the reals is not recursively enumerable and so has no recursive axiomatisation. The proof applies when the time flow is any infinite Dedekind complete linear order, including the integers $\mathbb {Z}$ and the natural numbers $\omega $ .

It is natural to consider the recursively axiomatised logic $\mathrm {L}_{\mathbb {R}}$ obtained by combining Bull’s propositional axioms and rules with those of classical first-order logic with identity. But, by Scott’s result, this $\mathrm {L}_{\mathbb {R}}$ is not complete for validity in first-order temporal models over the reals, and the incompleteness cannot be overcome by adding any recursive set of further axioms to $\mathrm {L}_{\mathbb {R}}$ . What model-theoretic interpretation can $\mathrm {L}_{\mathbb {R}}$ have, if any? Is there some notion of validity over real time, different to the standard one, with respect to which $\mathrm {L}_{\mathbb {R}}$ is complete?

There have been a number of approaches to developing alternative semantics for quantified modal logics (see [1, sec. 9] and [6]). Here we give a positive answer to our question by adapting the ‘admissible’ semantics developed in [7, 8]. This is based on the idea that, while a proposition can be identified with the set of worlds, or moments of time, at which it is true, not all sets of worlds/times need correspond in this way to any proposition. We use models $\mathcal {M}$ whose components include a time flow T, a universe U of individuals, and a designated collection $\mathit {Prop}$ of subsets of T, called the admissible propositions of $\mathcal {M}$ , from which the interpretations of formulas are to be selected. In particular $\mathcal {M}$ assigns to each sentence $\varphi $ a truth set $|\varphi |^{\mathcal {M}}$ of all points in T at which $\varphi $ is true, and these truth sets are required to be admissible. $\mathit {Prop}$ is closed under the Boolean set operations that interpret the truth-functional connectives, and under further operations interpreting the temporal modalities. The partial ordering $\subseteq $ of set inclusion serves as an entailment relation between propositions. $\mathit {Prop}$ is also used to give an alternative interpretation of the quantifiers which takes into account the admissibility of propositions but still validates the classical axioms and rules for $\forall $ and $\exists $ .

In a standard model, a sentence $\forall x\varphi $ is treated as semantically equivalent to the conjunction of the sentences $\varphi (a/x)$ for all $a\in U$ . This makes the truth sets $|\forall x\varphi |^{\mathcal {M}}$ , $|\varphi (a/x)|^{\mathcal {M}}$ satisfy

$$ \begin{align*}|\forall x\varphi|^{\mathcal{M}}= \mathop{\textstyle\bigcap}_{}\{|\varphi(a/x)|^{\mathcal{M}}:a\in U\}. \end{align*} $$

An admissible model has instead that

where is an operation that produces the greatest lower bound of the $|\varphi (a/x)|^{\mathcal {M}}$ ’s in the partially ordered set $(\mathit {Prop},\subseteq )$ . This means that $|\forall x\varphi |^{\mathcal {M}}$ is an admissible proposition that entails all of the $|\varphi (a/x)|^{\mathcal {M}}$ ’s, and is the weakest such proposition to do so, i.e., it is entailed by any other admissible proposition that entails all of the $|\varphi (a/x)|^{\mathcal {M}}$ ’s. Our definition of “model” ensures that this greatest lower bound exists and is admissible whenever all of the $|\varphi (a/x)|^{\mathcal {M}}$ ’s are admissible. The existential quantifier is treated dually as

$$ \begin{align*}|\exists x\varphi|^{\mathcal{M}}= \mathop{\textstyle\bigsqcup}_{}\{|\varphi(a/x)|^{\mathcal{M}}:a\in U\}, \end{align*} $$

where the operation $\mathop {\textstyle \bigsqcup }$ produces least upper bounds in $\mathit {Prop}$ . The interpretation of $\forall $ and $\exists $ by greatest-lower and least-upper bounds has a long history that is briefly discussed in [7, sec. 1.4].

The next two sections set out the background theory of admissible semantics for first-order temporal logic. Then in Section 4 we prove that for a countable language, $\mathrm {L}_{\mathbb {R}}$ is strongly complete over the set of admissible models based on $\mathbb {R}$ . This is done by taking an $\mathrm {L}_{\mathbb {R}}$ -consistent set $\Delta $ of formulas and applying known results to obtain a standard model that satisfies $\Delta $ and is based on the rational number time flow $(\mathbb {Q},<)$ . This model is then extending to an admissible model based on $\mathbb {R}$ that still satisfies $\Delta $ .

The final section shows that this construction cannot be successfully carried out when the temporal order is discrete. We prove that the set of formulas valid in all admissible models over the integer time flow $\mathbb {Z}$ is not recursively axiomatisable, just as for the logic of standard models over $\mathbb {Z}$ . The non-axiomatisability argument extends to hold for any logic characterised by the admissible models over a time flow that is scattered, i.e., does not contain a copy of $\mathbb {Q}$ as a suborder.

2. Logics

We review the syntax of first-order temporal logic. Fix a denumerable set $\mathsf {Var}=\{x,y,z,\dots \}$ of individual variables and a signature ${\cal L}$ , consisting of various individual constants ${\mathsf c}$ , function symbols F and predicate symbols P. An ${\cal L}$ -term is any individual variable, any constant ${\mathsf c}$ from ${\cal L}$ , or inductively any expression $F\tau _1\cdots \tau _n$ where F is an n-ary function symbol from ${\cal L}$ , and $ \tau _1,\dots ,\tau _n$ are ${\cal L}$ -terms. A term is closed if it contains no variables.

An atomic ${\cal L}$ -formula is any expression $P\tau _1\cdots \tau _n$ or $\tau _1\approx \tau _2$ where P is an n-ary predicate symbol from ${\cal L}$ , and the $ \tau _i$ are ${\cal L}$ -terms. The set of ${\cal L}$ -formulas is generated from the atomic ones in the usual way, using the Boolean connectives $\land $ (conjunction) and $\neg $ (negation), the universal quantifiers $\forall x$ for each individual variable x, and the temporal modalities $\mathbf {G}$ (‘it will always be that’) and $\mathbf {H}$ (‘it has always been that’). Other Boolean connectives ( $\lor $ , $\to $ , $\leftrightarrow $ ) and the existential quantifiers $\exists x$ are introduced by standard definitions. $\mathbf {F}$ (‘at some future time’) and $\mathbf {P}$ (‘at some past time’) are defined as $\neg \mathbf {G}\neg $ and $\neg \mathbf {H}\neg $ respectively. The modality $\Box $ is introduced by defining $\Box \varphi $ to be the formula $\mathbf {H}\varphi \land \varphi \land \mathbf {G}\varphi $ . On a linear time flow $\Box $ is the universal modality expressing ‘at all times, past present and future’. $\lozenge \varphi $ abbreviates $\mathbf {P}\varphi \lor \varphi \lor \mathbf {F}\varphi $ (‘at some time’). The notation $\varphi (\tau /x)$ denotes the formula obtained by replacing all free occurrences of x in formula $\varphi $ by the term $\tau $ . Each formula or inference rule has a mirror image, obtained by replacing $\mathbf {G}$ by $\mathbf {H}$ and vice versa, hence also interchanging $\mathbf {F}$ and $\mathbf {P}$ .

We now list axioms and rules of inference that define the notion of a temporal logic that we will work with. The inference rules needed are

We adopt the following axioms about quantifiers.

$$ \begin{align*} \begin{array}{ll} \forall x\varphi\to \varphi(\tau/x), \qquad \text{where}\ \tau\ \text{is free for}\ x\ \text{in}\ \varphi. &\quad \quad {Universal\ Instantiation} \\ \forall x(\varphi\to \psi) \to (\forall x\varphi\to\forall x\psi). &\quad\quad {Universal\ Distribution} \\ \varphi\to\forall x\varphi, \qquad \text{where}\ x\ \text{is\ not\ free\ in}\ \varphi. &\quad\quad {Vacuous\ Quantification} \end{array} \end{align*} $$

For the identity symbol $\approx $ we need the following axioms, in which the notation $\varphi (\tau ' /\!/ \tau )$ denotes any formula obtained from $\varphi $ by replacing some, but not necessarily all, occurrences of $\tau $ by $\tau '$ .

$$ \begin{align*} \begin{array}{ll} \tau\approx\tau, &\quad\quad {Self\ Identity} \\ \tau\approx\tau'\to(\varphi\to\varphi(\tau'/\!/ \tau)), \quad \text{with}\ \varphi\ \text{atomic}. &\quad \quad{Substitution\ of\ Identicals} \\ \tau\approx\tau'\to \Box(\tau\approx\tau'). &\quad \quad{Rigid\ Identity} \end{array} \end{align*} $$

By a (temporal) logic over a signature ${\cal L}$ we will mean any set $\mathrm {L}$ of ${\cal L}$ -formulas that is closed under the above rules and includes all instances of truth-functional tautologies and the above axioms, as well as the following two schemes and their mirror images.

Members of $\mathrm {L}$ are called $\mathrm {L}$ -theorems. The last two schemes and their mirror images axiomatise the propositional logic K $_t$ due to E. J. Lemmon and known as the ‘minimal tense-logic’ [10, p. 176].

It is significant that the Barcan formulas

(1) $$ \begin{align} \forall x\mathbf{G}\varphi\to\mathbf{G}\forall x\varphi, \qquad \forall x\mathbf{H}\varphi\to\mathbf{H}\forall x\varphi \end{align} $$

are derivable as theorems of any logic as defined here. The derivation depends on Universal Instantiation as well as the scheme $\varphi \to \mathbf {G}\mathbf {P}\varphi $ and its mirror (see [10, p. 147] or [4, theorem 11.5]).

The logic $\mathrm {L}_{\mathbb {Q}}$ over ${\cal L}$ is defined to be the smallest logic that includes the following schemes and their mirror images (with the properties of the temporal order that they encapsulate listed on the right):

Thus the $\mathrm {L}_{\mathbb {Q}}$ -theorems over ${\cal L}$ are all ${\cal L}$ -formulas that are obtainable from the above axioms by applying the given rules. The last six propositional schemes together axiomatise the propositional temporal logic of $(\mathbb {Q},<)$ [2].

The logic $\mathrm {L}_{\mathbb {R}}$ can be defined by adding to $\mathrm {L}_{\mathbb {Q}}$ the axiom

(2) $$ \begin{align} \Box(\mathbf{G}\varphi\to\mathbf{P}\mathbf{G}\varphi)\to(\mathbf{G}\varphi\to\mathbf{H}\varphi). \qquad\qquad\qquad{Dedekind\ completeness} \end{align} $$

For a given logic $\mathrm {L}$ , a formula $\varphi $ is $\mathrm {L}$ -consistent if $\neg \varphi $ is not an $\mathrm {L}$ -theorem, and a set $\Delta $ of formulas is $\mathrm {L}$ -consistent if every finite subset of $\Delta $ has an $\mathrm {L}$ -consistent conjunction. An $\mathrm {L}$ -consistent set $\Delta $ of ${\cal L}$ -formulas is maximally $\mathrm {L}$ -consistent over ${\cal L}$ if there is no $\mathrm {L}$ -consistent set of ${\cal L}$ -formulas that properly extends it, or equivalently if it is negation complete in the sense that for any ${\cal L}$ -formula $\varphi $ , if $\varphi \notin \Delta $ then $\neg \varphi \in \Delta $ . A maximally $\mathrm {L}$ -consistent set contains all $\mathrm {L}$ -theorems.

Write $\Delta \vdash _{\mathrm {L}}\varphi $ to mean that there is a formula $\delta \to \varphi $ in $\mathrm {L}$ such that $\delta $ is the conjunction of finitely many members of $\Delta $ . $\Delta $ is $\forall $ -complete over ${\cal L}$ if for every ${\cal L}$ -formula $\varphi $ and variable x, if $\Delta \vdash _{\mathrm {L}}\varphi (\tau /x)$ for all closed ${\cal L}$ -terms $\tau $ , then $\Delta \vdash _{\mathrm {L}}\forall x\varphi $ . $\Delta $ is $\mathrm {L}$ -saturated over ${\cal L}$ if it is both maximally $\mathrm {L}$ -consistent and $\forall $ -complete over ${\cal L}$ . The following is a well-known result that goes back to [9].

Theorem 1. For any logic $\mathrm {L}$ over a countable signature ${\cal L}$ , if $\Delta $ is $\mathrm {L}$ -consistent over ${\cal L}$ , and ${\cal L}^+$ is a countable extension of ${\cal L}$ that includes infinitely many constants not in ${\cal L}$ , then $\Delta $ can be extended to an $\mathrm {L}$ -saturated set over ${\cal L}^+$ .

3. Admissible models

A time flow is a structure $(T,<)$ for which T is a set (thought of as a set of times/instants), and $<$ is a linear ordering on T, i.e., a transitive irreflexive relation that is linear in the sense that either $s<t$ or $t<s$ for all distinct $s,t\in T$ . The relation inverse to $<$ will be denoted $>$ . When T is a set of numbers, e.g., the reals $\mathbb {R}$ , rationals $\mathbb {Q}$ , integers $\mathbb {Z}$ or natural numbers $\omega $ , then $<$ will invariably have its usual numerical meaning.

A model structure is a system $\mathcal {S}=(T,<,\mathit {Prop},U)$ such that $(T,<)$ is a time flow; $\mathit {Prop}$ is a non-empty subset of the powerset $\wp T$ of T that is closed under the Boolean set operations and under the operations $[<]$ and $[>]$ , interpreting $\mathbf {G}$ and $\mathbf {H}$ , defined by

$$ \begin{align*} [<]X&=\{t\in T: \forall s\in T(t<s\text{ implies } s\in X)\}, \\ [>]X&=\{t\in T: \forall s\in T(t>s\text{ implies } s\in X)\}; \end{align*} $$

and U is a set, called the universe of $\mathcal {S}$ . A subset of T is called admissible if it belongs to $\mathit {Prop}$ . Members of $\mathit {Prop}$ may be referred to as the admissible propositions of $\mathcal {S}$ .

Operations and $\mathop {\textstyle \bigsqcup }$ on collections of subsets of T are defined by putting, for each ${\cal Z}\subseteq \wp T$ ,

We emphasise that and $\mathop {\textstyle \bigsqcup }{\cal Z}$ are defined for arbitrary ${\cal Z}\subseteq \wp T$ . They need not be admissible, even when all members of ${\cal Z}$ are admissible. If ${\cal Z}\subseteq \mathit {Prop}$ and is admissible, then is the greatest lower bound of ${\cal Z}$ in the partially ordered set $(\mathit {Prop},\subseteq )$ , and will not be equal to $\mathop {\textstyle \bigcap }{\cal Z}$ unless the latter is admissible, which it need not be. Dual statements hold about $ \mathop {\textstyle \bigsqcup } {\cal Z}$ and $\mathop {\textstyle \bigcup } {\cal Z}$ and least upper bounds [7, sec. 1.5].

Another perspective is that $\mathit {Prop}$ is a base for a topology on T for which is the interior of $ \mathop {\textstyle \bigcap } {\cal Z}$ , while $\mathop {\textstyle \bigsqcup } {\cal Z}$ is the closure of $\mathop {\textstyle \bigcup } {\cal Z}$ .

A premodel $\mathcal {M}=(\mathcal {S},|\mathord {-}|^{\mathcal {M}})$ for ${\cal L}$ based on $\mathcal {S}$ is given by an interpretation function $|\mathord {-}|^{\mathcal {M}}$ that assigns to each individual constant $\mathsf c\in {\cal L}$ an element $|\mathsf {c}|^{\mathcal {M}}$ of the universe $ U$ ; to each n-ary function symbol $F\in {\cal L}$ an n-ary function $|F|^{\mathcal {M}}:U^n\to U$ ; and to each n-ary predicate symbol $P\in {\cal L}$ a function $|P|^{\mathcal {M}}:U^n\to \wp T$ . Informally $|P|^{\mathcal {M}}(a_1,\dots ,a_n)$ represents the proposition that the predicate P holds of the n-tuple $(a_1,\dots ,a_n)$ . Equivalent ways of interpreting P are to assign to it the function $t\mapsto \{(a_1,\dots ,a_n):t\in |P|^{\mathcal {M}}(a_1,\dots ,a_n)\}$ from T to $U^n$ , or the subset $\{(t,a_1,\dots ,a_n):t\in |P|^{\mathcal {M}}(a_1,\dots ,a_n)$ } of $T\times U^n$ .

A variable assignment is a function f assigning to each $x\in \mathsf {Var}$ an element $fx$ of the universe U. Then f inductively assigns to each ${\cal L}$ -term $\tau $ a value $|\tau |^{\mathcal {M}}f\in U$ , by putting $|x|^{\mathcal {M}}f=fx$ ; $|{\mathsf c}|^{\mathcal {M}}f=|{\mathsf c}|^{\mathcal {M}}$ ; and $|F\tau _1\cdots \tau _n|^{\mathcal {M}}f = |F|^{\mathcal {M}}(|\tau _1|^{\mathcal {M}} f,\dots ,|\tau _n|^{\mathcal {M}} f$ ). If $\tau $ is a closed term, then $|\tau |^{\mathcal {M}}f=|\tau |^{\mathcal {M}}g$ for all variable assignments $f,g$ , and we denote this constant value by $|\tau |^{\mathcal {M}}$ . We use the notation $f[a/x]$ for the variable assignment that updates f by assigning the value a to x and otherwise acting identically to f.

A premodel $\mathcal {M}$ associates with each ${\cal L}$ -formula $\varphi $ and assignment f a subset $|\varphi |^{\mathcal {M}} f$ of T, viewed as the ‘truth set’ of all times at which $\varphi $ is true under f. This is defined by induction on the formation of $\varphi $ :

• • $|\tau _1\approx \tau _2|^{\mathcal {M}}f$ is T if $|\tau _1|^{\mathcal {M}}f=|\tau _2|^{\mathcal {M}}f$ , and is $\emptyset $ otherwise.

• • $|P\tau _1\cdots \tau _n|^{\mathcal {M}} f=|P|^{\mathcal {M}}(|\tau _1|^{\mathcal {M}} f,\dots ,|\tau _n|^{\mathcal {M}} f)$ .

• • $|\varphi \wedge \psi |^{\mathcal {M}} f=|\varphi |^{\mathcal {M}} f\cap |\psi |^{\mathcal {M}} f$ .

• • $|\neg \varphi |^{\mathcal {M}} f=T-|\varphi |^{\mathcal {M}} f$ .

• • $|\mathbf {G}\varphi |^{\mathcal {M}} f=[<]|\varphi |^{\mathcal {M}} f$ .

• • $|\mathbf {H}\varphi |^{\mathcal {M}} f=[>]|\varphi |^{\mathcal {M}} f$ .

• • .

Since $\exists x\varphi $ is $\neg \forall x\neg \varphi $ , it follows that

• • $| \exists x\varphi |^{\mathcal {M}} f = \mathop {\textstyle \bigsqcup }_{a\in U}|\varphi |^{\mathcal {M}} f[a/x]$ .

Writing $\mathcal {M},t,f\models \varphi $ to mean that $t\in |\varphi |^{\mathcal {M}} f$ , we have the following clauses for this truth/satisfaction relation:

• • $\mathcal {M},t,f\models \tau _1\approx \tau _2$ iff $|\tau _1|^{\mathcal {M}}f=|\tau _2|^{\mathcal {M}}f$ .

• • $\mathcal {M},t,f\models P\tau _{1}\cdots \tau _{n}$ iff $t\in |P|^{\mathcal {M}}(|\tau _1|^{\mathcal {M}} f,\dots ,|\tau _n|^{\mathcal {M}} f)$ .

• • $\mathcal {M},t,f\models \varphi \land \psi $ iff $\mathcal {M},t,f\models \varphi $ and $\mathcal {M},t,f\models \psi $ .

• • $\mathcal {M},t,f\models \neg \varphi $ iff $\mathcal {M},t,f\not \models \varphi $ .

• • $\mathcal {M},t,f\models \mathbf {G} \varphi $ iff for all $s\in T,\ t<s\ \text {implies}\ \mathcal {M},s,f\models \varphi $ .

• • $\mathcal {M},t,f\models \mathbf {H} \varphi $ iff for all $s\in T,\ s<t\ \text {implies}\ \mathcal {M},s,f\models \varphi $ .

• • $\mathcal {M},t,f\models \mathbf {F} \varphi $ iff for some $s\in T,\ t<s\ \text {and}\ \mathcal {M},s,f\models \varphi $ .

• • $\mathcal {M},t,f\models \mathbf {P} \varphi $ iff for some $s\in T,\ s<t\ \text {and}\ \mathcal {M},s,f\models \varphi $ .

• • $\mathcal {M},t,f\models \Box \varphi $ iff for all $s\in T,\ \mathcal {M},s,f\models \varphi $ .

• • $\mathcal {M},t,f\models \lozenge \varphi $ iff for some $s\in T,\ \mathcal {M},s,f\models \varphi $ .

• • $\mathcal {M},t,f\models \forall x\varphi $ iff there is an $X\in \mathit {Prop}$ such that $t\in X \subseteq \mathop {\textstyle \bigcap }_{a\in U}|\varphi |^{\mathcal {M}}{f[a/x]}$ .

From the clause for $\forall $ we see that

(3) $$ \begin{align} \mathcal{M},t,f\models\forall x\varphi \enspace only\ if \enspace \text{for all } a\in U, \ \mathcal{M},t,f[a/x]\models\varphi. \end{align} $$

The converse need not hold.

Reading off the semantics for the defined existential quantifier gives

1. $\mathcal {M},t,f\models \exists x\varphi $ iff for all $X\in \mathit {Prop}$ such that $t\in X$ , there exists $s\in X$ and $a\in U$ with $\mathcal {M},s,f[a/x]\models \varphi $ .

Consequently:

(4) $$ \begin{align} \text{If some}\ a\in U\ \text{has } \mathcal{M},t,f[a/x]\models\varphi, \text{ then } \mathcal{M},t,f\models\exists x\varphi. \end{align} $$

Again, the converse can fail.

The semantics of term substitution is given by the result [7, 1.6.2] that

(5) $$ \begin{align} \mathcal{M},t,f\models\varphi(\tau/x) \enspace \text{iff} \enspace \mathcal{M},t,f[\,|\tau|^{\mathcal{M}} f/x]\models\varphi. \end{align} $$

It can also be shown [7, 1.6.1] that if two assignments $f,g$ agree on all free variables of $\varphi $ , then $|\varphi |^{\mathcal {M}}f=|\varphi |^{\mathcal {M}}g$ . Hence if $\varphi $ is a sentence (no free variables), then $|\varphi |^{\mathcal {M}}f=|\varphi |^{\mathcal {M}}g$ for all assignments $f,g$ and we write this single truth set as $|\varphi |^{\mathcal {M}}$ . Also if $\varphi $ is a sentence and $\mathcal {M},t,f\models \varphi $ , then $\mathcal {M},t,g\models \varphi $ for all assignments g, which we just write as $\mathcal {M},t\models \varphi $ . Then $|\varphi |^{\mathcal {M}}=\{t\in T:\mathcal {M},t\models \varphi \}$ .

A formula $\varphi $ is valid in premodel $\mathcal {M}$ , written $\mathcal {M}\models \varphi $ , if $|\varphi |^{\mathcal {M}} f=T$ for all f, i.e., if $\mathcal {M},t,f\models \varphi $ for all $t\in T$ and all variable assignments f in $\mathcal {M}$ . $\varphi $ is admissible in premodel $\mathcal {M}$ if $|\varphi |^{\mathcal {M}}f\in \mathit {Prop}$ for all variable assignments f in $\mathcal {M}$ . A model for ${\cal L}$ is, by definition, an ${\cal L}$ -premodel in which every ${\cal L}$ -formula is admissible. We sometimes call this an admissible model for emphasis or contrast.

It follows from [7, sec. 1.7] that the Universal Instantiation and Universal Distribution axioms are valid in any premodel $\mathcal {M}$ (Instantiation depends on (5)), while the Universal Generalisation rule is sound for validity in $\mathcal {M}$ . Moreover an instance $\varphi \to \forall x\varphi $ of Vacuous Quantification is valid in $\mathcal {M}$ provided that $\varphi $ is admissible in $\mathcal {M}$ . Thus if $\mathcal {M}$ is a model, it validates Vacuous Quantification.

Validity of the Identity axioms in all premodels follows readily from the fact that the interpretation of $\approx $ is rigid, i.e., independent of time. Under a given variable assignment f, an identity $\tau _1\approx \tau _2$ is true at some time iff it is true at all times, as its truth is determined by the identity of the time-independent values $|\tau _i|^{\mathcal {M}}f$ .

A logic $\mathrm {L}$ is sound for validity in a class $\mathscr {C}$ of premodels if every $\mathrm {L}$ -theorem is valid in all members of $\mathscr {C}$ , or equivalently every formula that is satisfiable at a point in some member of $\mathscr {C}$ is $\mathrm {L}$ -consistent. Conversely $\mathrm {L}$ is complete over $\mathscr {C}$ if every $\mathrm {L}$ -consistent formula is satisfiable in a member of $\mathscr {C}$ , and is strongly complete if every $\mathrm {L}$ -consistent set of formulas is satisfiable in a member of $\mathscr {C}$ .

Putting the above observations about validity together we see that the logic $\mathrm {L}_{\mathbb {Q}}$ is sound for validity in all models based on the rational time flow. Likewise $\mathrm {L}_{\mathbb {R}}$ is validated by all models over the real time flow.

A premodel $\mathcal {M}$ will be called Kripkean if it always has

(6) $$ \begin{align} |\forall x\varphi|^{\mathcal{M}} f = \bigcap_{a\in U} |\varphi|^{\mathcal{M}} f[a/x]. \end{align} $$

This means that $\forall $ gets the classical semantics

(7) $$ \begin{align} \mathcal{M},t,f\models\forall x\varphi\enspace \text{iff} \enspace \text{for all } a\in U, \ \mathcal{M},t,f[a/x]\models\varphi, \end{align} $$

and correspondingly, the existential quantifier gets

(8) $$ \begin{align} \mathcal{M},t,f\models\exists x\varphi\enspace \text{iff} \enspace \text{for some } a\in U, \ \mathcal{M},t,f[a/x]\models\varphi \end{align} $$

(compare with (3) and (4)).

If a premodel $\mathcal {M}$ has every subset admissible, i.e., $\mathit {Prop}= \wp T$ , then $\mathcal {M}$ is a model and is just $\mathop {\textstyle \bigcap }$ , so $\mathcal {M}$ is Kripkean. Such an $\mathcal {M}$ will be called a standard model, and can be identified with the structure $(T,<,U,|\mathord {-}|^{\mathcal {M}})$ . In [5, secs. 4.3–4.5] a strong completeness theorem is proven for the logic $\mathrm {L}_{\mathbb {Q}}$ , showing that any $\mathrm {L}_{\mathbb {Q}}$ -consistent set is satisfiable in a standard model over the rational time flow. The method involves extending a consistent set to a saturated one over an enlarged signature, and then constructing a satisfying model for the saturated set. We distill from that work the following result.

Theorem 2. Let $\Delta $ be an $\mathrm {L}_{\mathbb {Q}}$ -saturated set of ${\cal L}$ -formulas, where ${\cal L}$ is a countable signature having constant terms. Then there is a standard ${\cal L}$ -model $\mathcal {M}$ over $(\mathbb {Q},<)$ in which $\Delta $ is satisfied, i.e., $\mathcal {M}, q_0,f_0\models \Delta $ for some rational $q_0$ and some variable assignment $f_0$ . Moreover each element of the universe of $\mathcal {M}$ is the value of some constant ${\cal L}$ -term.

In a premodel $\mathcal {M}$ for which each element $a\in U$ is the value of some constant term $\bar {a}$ , i.e., $|\bar {a}|^{\mathcal {M}}=a$ , any variable assignment $f:\mathsf {Var}\to U$ induces a substitution operator turning each formula $\varphi $ into a sentence $\varphi ^f$ by replacing each free variable x of $\varphi $ by the constant term $\overline {fx}$ . This allows us to reduce satisfaction of formulas by assignments to truth of sentences:

Lemma 3. $\mathcal {M},t,f\models \varphi $ iff $\mathcal {M},t\models \varphi ^f$ .

Proof. By the result (5), $\mathcal {M},t,f\models \varphi (\overline {fx}/x)$ iff $\mathcal {M},t,f[f(x)/x]\models \varphi $ . But $f[f(x)/x]=f$ . Applying this to all the free variables of $\varphi $ shows that $\mathcal {M},t,f\models \varphi ^f$ iff $\mathcal {M},t,f\models \varphi $ . But $\mathcal {M},t,f\models \varphi ^f$ iff $\mathcal {M},t\models \varphi ^f$ since $\varphi ^f$ is a sentence.

A further consequence of having every element of the universe of $\mathcal {M}$ being a value $|\bar {a}|^{\mathcal {M}}$ is that if $\mathcal {M}$ is Kripkean and $\forall x\varphi $ is a sentence, then by (7) and (5),

(9) $$ \begin{align} \mathcal{M},t\models\forall x\varphi\enspace \text{iff} \enspace \text{for all } a\in U, \ \mathcal{M},t\models\varphi(\bar{a}/x). \end{align} $$

4. Strong completeness over the reals

We will now prove that the logic $\mathrm {L}_{\mathbb {R}}$ over a countable signature ${\cal L}$ is strongly complete over the set of admissible ${\cal L}$ -models based on $(\mathbb {R},<)$ .

Let $\Delta $ be an $\mathrm {L}_{\mathbb {R}}$ -consistent set of ${\cal L}$ -formulas. Our task is to show that it is satisfied in a some model over $(\mathbb {R},<)$ . Let ${\cal L}^{+}$ be the signature obtained by adding denumerably many new constants to ${\cal L}$ . By Theorem 1 there is an $\mathrm {L}_{\mathbb {R}}$ -saturated set $\Delta ^+$ of ${\cal L}^{+}$ -formulas with $\Delta \subseteq \Delta ^+$ .

Now $\Delta ^+$ is also $\mathrm {L}_{\mathbb {Q}}$ -saturated over ${\cal L}^{+}$ : as well as being $\forall $ -complete it is $\mathrm {L}_{\mathbb {Q}}$ -consistent as $\mathrm {L}_{\mathbb {Q}}$ is a sublogic of $\mathrm {L}_{\mathbb {R}}$ , and is negation complete for ${\cal L}^{+}$ -formulas, hence is maximally $\mathrm {L}_{\mathbb {Q}}$ -consistent over ${\cal L}^{+}$ . So we can apply Theorem 2 to $\Delta ^+$ and ${\cal L}^{+}$ to conclude that $\Delta ^+$ is satisfiable in a standard model based on the rational time flow. So there is a standard ${\cal L}^{+}$ -model

$$ \begin{align*}\mathcal{M}=(\mathbb{Q},<,U,|\mathord{-}|^{\mathcal{M}}) \end{align*} $$

such that $\mathcal {M}, q_0,f_0\models \Delta ^+$ for some rational $q_0$ and some variable assignment $f_0$ . Also each $a\in U$ is $|\bar a|^{\mathcal {M}}$ for some closed ${\cal L}^{+}$ -term $\bar a$ .

Lemma 4. If a sentence $\varphi $ is an $\mathrm {L}_{\mathbb {R}}$ -theorem over ${\cal L}^{+}$ , then $\mathcal {M}\models \varphi $ .

Proof. If $\varphi $ is an $\mathrm {L}_{\mathbb {R}}$ -theorem, then so is $\Box \varphi $ , which thus belongs to the $\mathrm {L}_{\mathbb {R}}$ -saturated $\Delta ^+$ . That gives $\mathcal {M},q_0\models \Box \varphi $ . Hence every rational q has $\mathcal {M},q\models \varphi $ .

We will extend $\mathcal {M}$ to an ${\cal L}^{+}$ -model

$$ \begin{align*}\mathcal{M}^*=(\mathbb{R},<,\mathit{Prop},U,|\mathord{-}|^{\mathcal{M}^*}), \end{align*} $$

based on the real time flow, with the same universe U as $\mathcal {M}$ , and with $|\mathord {-}|^{\mathcal {M}^*}$ assigning the same interpretation as $|\mathord {-}|^{\mathcal {M}}$ to the individual constants and function symbols of ${\cal L}^{+}$ . To define $\mathit {Prop}$ , and $|P|^{\mathcal {M}^*}$ for predicate symbols P, we will assign to each $r\in \mathbb {R}$ a certain set $\Delta _r$ of ${\cal L}^{+}$ -sentences.

An $\mathrm {L}_{\mathbb {R}}$ -consistent set of ${\cal L}^{+}$ -sentences will be called $\mathrm {L}_{\mathbb {R}}$ -maximal if there is no $\mathrm {L}_{\mathbb {R}}$ -consistent set of ${\cal {\cal L}^{+}}$ -sentences that properly extends it, or equivalently if it is negation complete for sentences, i.e., it contains either $\varphi $ or $\neg \varphi $ for any ${\cal L}^{+}$ -sentence $\varphi $ . We define $\Delta _r$ to be $\mathrm {L}_{\mathbb {R}}$ -maximal for all $r\in \mathbb {R}$ . For $q\in \mathbb {Q}$ , let $\Delta _q$ be the set of all ${\cal L}^{+}$ -sentences $\varphi $ such that $\mathcal {M},q\models \varphi $ .

Lemma 5. For all $q\in \mathbb {Q}$ , $\Delta _q$ is $\mathrm {L}_{\mathbb {R}}$ -maximal over ${\cal L}^{+}$ .

Proof. $\Delta _q$ is negation complete for ${\cal L}^{+}$ -sentences, so it is enough to show that it is $\mathrm {L}_{\mathbb {R}}$ -consistent. Let $\varphi $ be the conjunction of any finite number of members of $\Delta _q$ . Then $\mathcal {M},q\models \varphi $ , so $\mathcal {M}\not \models \neg \varphi $ . Hence by Lemma 4, $\neg \varphi $ is not an $\mathrm {L}_{\mathbb {R}}$ -theorem, i.e., $\varphi $ is $\mathrm {L}_{\mathbb {R}}$ -consistent as required.

For $r\notin \mathbb {Q}$ , to define $\Delta _r$ we adapt a method used in [5, p. 190]. First define a set $\Delta _r^0$ to consist of each ${\cal L}^{+}$ -sentence $\varphi $ that is true in $\mathcal {M}$ throughout some open rational interval around r, i.e., those $\varphi $ for which there exist $s,t$ with $s<r<t$ such that $\mathcal {M},q\models \varphi $ for all rationals q having $s<q<t$ .

Lemma 6. A sentence $\psi $ belongs to $\Delta _r^0$ if it satisfies any of the following conditions.

1. (1) $\psi $ is $\mathbf {F}\varphi $ with $\mathcal {M},q\models \varphi $ for some $q\in \mathbb {Q}$ having $r<q$ .

2. (2) $\psi $ is $\mathbf {G}\varphi $ with $\mathcal {M},q\models \varphi $ for all $q\in \mathbb {Q}$ having $r<q$ .

3. (3) $\psi $ is $\mathbf {P}\varphi $ with $\mathcal {M},q\models \varphi $ for some $q\in \mathbb {Q}$ having $q<r$ .

4. (4) $\psi $ is $\mathbf {H}\varphi $ with $\mathcal {M},q\models \varphi $ for all $q\in \mathbb {Q}$ having $q<r$ .

5. (5) $\mathcal {M}\models \psi $ .

Proof.

1. (1) If $\mathcal {M},q\models \varphi $ with $r<q$ , then $\mathbf {F}\varphi $ is true in $\mathcal {M}$ throughout any rational interval around r whose members are less than q, hence $\mathbf {F}\varphi \in \Delta _r^0$ .

2. (2) Let $\mathcal {M},q\models \varphi $ for all rational q greater than r. Thus the truth set $|\varphi |^{\mathcal {M}}$ of $\varphi $ in $\mathcal {M}$ includes $\{q\in \mathbb {Q}:r<q\}$ . Hence $|\mathbf {G}\varphi |^{\mathcal {M}}$ includes $\{q\in \mathbb {Q}:r<q\}$ .

   Suppose, for the sake of contradiction, that $\mathbf {G}\varphi \notin \Delta _r^0$ . Then any open rational interval around r must contain a point at which $\mathbf {G}\varphi $ is false in $\mathcal {M}$ , and so this point must be less than r (n.b. $r\notin \mathbb {Q}$ ). In particular, for any rational $q<r$ , there must be a rational $q'$ with $q<q'<r$ and $\mathcal {M},q'\not \models \mathbf {G}\varphi $ , hence $\mathcal {M},q\not \models \mathbf {G}\varphi $ . Altogether this shows that $|\mathbf {G}\varphi |^{\mathcal {M}}$ is exactly equal to $\{q\in \mathbb {Q}:r<q\}$ .

   Therefore by density of the rationals in $\mathbb {R}$ , any point in $\mathcal {M}$ at which $\mathbf {G}\varphi $ is true has $\mathbf {PG}\varphi $ true, so $\mathcal {M}\models \Box (\mathbf {G}\varphi \to \mathbf {PG}\varphi )$ . At the same time any rational $q>r$ has $\mathcal {M},q\not \models \mathbf {G}\varphi \to \mathbf {H}\varphi $ , so we now have an instance of the $\mathrm {L}_{\mathbb {R}}$ -axiom (2) that is false in $\mathcal {M}$ at q. But that contradicts Lemma 4. The contradiction forces us to conclude that $\mathbf {G}\varphi \in \Delta _r^0$ .

3. (3) This is the mirror image of part (1).

4. (4) This is the mirror image of part (2), so can be proven using the mirror image of axiom (2). However it can also be shown from axiom (2) itself, so we only need a single Dedekind completeness axiom.

   To see this, suppose that $\mathcal {M},q\models \varphi $ for all rational $q<r$ , but $\mathbf {H}\varphi \notin \Delta _r^0$ . Then reasoning dual to part (2), we get $|\mathbf {H}\varphi |^{\mathcal {M}}=\{q\in \mathbb {Q}:q<r\}$ . Hence as $r\notin \mathbb {Q}$ , $ \{q\in \mathbb {Q}:r<q\}=|\neg \mathbf {H}\varphi |^{\mathcal {M}}. $ From this we see that $\{q\in \mathbb {Q}:r<q\}=|\mathbf {G}\psi |^{\mathcal {M}}$ , where $\psi $ is $\neg \mathbf {H}\varphi $ . Hence as in the proof of part (2) we get that $\mathcal {M}\models \Box (\mathbf {G}\psi \to \mathbf {PG} \psi )$ , while any rational $q>r$ has $\mathcal {M},q\not \models \mathbf {G}\psi \to \mathbf {H}\psi $ , so again we get the contradiction of an instance of axiom (2) falsifiable in $\mathcal {M}$ .

5. (5) If $\mathcal {M}\models \psi $ , then any open rational interval around r has $\psi $ true throughout it.

Lemma 7. $\Delta _r^0$ is $\mathrm{L}_{\mathbb {R}}$ -consistent.

Proof. Let $\varphi $ be the conjunction of any finite number of members of $\Delta _r^0$ . Each of these members is true in $\mathcal {M}$ throughout some rational interval around r. Choose a rational number q that belongs to all of these finitely many intervals. Then $\mathcal {M},q\models \varphi $ , so $\varphi \in \Delta _q$ . Hence $\varphi $ is $\mathrm {L}_{\mathbb {R}}$ -consistent as required, because $\Delta _q$ is $\mathrm {L}_{\mathbb {R}}$ -consistent by Lemma 5.

If follows that $\Delta _r^0$ has $\mathrm {L}_{\mathbb {R}}$ -maximal extensions. We choose one to be $\Delta _r$ . That completes the definition of $\Delta _r$ for all reals r.

For each ${\cal L}^{+}$ -sentence $\varphi $ define $|\varphi |_{\mathbb {R}} =\{r\in \mathbb {R}:\varphi \in \Delta _r\}$ , and put

$$ \begin{align*}\mathit{Prop}=\{|\varphi|_{\mathbb{R}}: \varphi \text{ is an } {\cal L}^{+}\text{-sentence}\}. \end{align*} $$

For an n-ary predicate symbol P, define $|P|^{\mathcal {M}^*}:U^n\to \mathit {Prop}$ by

$$ \begin{align*}|P|^{\mathcal{M}^*}(a_1,\dots,a_n)=|P\overline{a_1}\cdots\overline{a_n}|_{\mathbb{R}}. \end{align*} $$

That completes the definition of $\mathcal {M}^*$ as a premodel.

Lemma 8. For any ${\cal L}^{+}$ -sentence $\varphi $ , $\mathcal {M}\models \varphi $ iff $|\varphi |_{\mathbb {R}}=\mathbb {R}$ .

Proof. Let $\mathcal {M}\models \varphi $ . Then for any real r, if $r\in \mathbb {Q}$ we have $\mathcal {M},r\models \varphi $ , so $\varphi \in \Delta _r$ . But if $r\notin \mathbb {Q}$ , then $\varphi \in \Delta _r^0$ by Lemma 6(5), so again $\varphi \in \Delta _r$ . In both cases $r\in |\varphi |_{\mathbb {R}}$ .

For the converse, let $|\varphi |_{\mathbb {R}}=\mathbb {R}$ . Then for any $q\in \mathbb {Q}$ , $\varphi \in \Delta _q$ and so $\mathcal {M},q\models \varphi $ . Hence $\mathcal {M}\models \varphi $ .

Standard properties of maximally consistent sets ensure that

$$ \begin{align*}|\varphi|_{\mathbb{R}}\cap|\psi|_{\mathbb{R}}=|\varphi\land\psi|_{\mathbb{R}}, \enspace |\varphi|_{\mathbb{R}}\cup|\psi|_{\mathbb{R}}=|\varphi\lor\psi|_{\mathbb{R}}, \enspace \mathbb{R}-|\varphi|_{\mathbb{R}}= |\neg\varphi|_{\mathbb{R}}, \end{align*} $$

so $\mathit {Prop}$ is a Boolean set algebra. It is also closed under the temporal operators $[<]$ and $[>]$ , by

Lemma 9. For any ${\cal L}^{+}$ -sentence $\varphi $ , $[<]|\varphi |_{\mathbb {R}}=|\mathbf {G}\varphi |_{\mathbb {R}}$ and $[>]|\varphi |_{\mathbb {R}}=|\mathbf {H}\varphi |_{\mathbb {R}}$ .

Proof. Let $r\in [<]|\varphi |_{\mathbb {R}}$ . Then any s with $r<s$ has $s\in |\varphi |_{\mathbb {R}}$ , i.e., $\varphi \in \Delta _s$ . In particular, any rational $q>r$ has $\varphi \in \Delta _q$ , i.e., $\mathcal {M},q\models \varphi $ . If $r\in \mathbb {Q}$ , this implies $\mathcal {M},r\models \mathbf {G}\varphi $ , so $\mathbf {G}\varphi \in \Delta _r$ , hence $r\in |\mathbf {G}\varphi |_{\mathbb {R}}$ . If $r\notin \mathbb {Q}$ , it gives $\mathbf {G}\varphi \in \Delta _r^0\subseteq \Delta _r$ by Lemma 6(2), hence again $r\in |\mathbf {G}\varphi |_{\mathbb {R}}$ . That proves $[<]|\varphi |_{\mathbb {R}}\subseteq |\mathbf {G}\varphi |_{\mathbb {R}}$ .

For the converse inclusion, let $\mathbf {G}\varphi \in \Delta _r$ . If $r\in \mathbb {Q}$ , then $\mathcal {M},r\models \mathbf {G}\varphi $ , hence

(10) $$ \begin{align} \text{every rational } q\ \text{greater than } r \text{ has } \mathcal{M},q\models\varphi. \end{align} $$

But if $r\notin \mathbb {Q}$ , then since $\neg \mathbf {G}\varphi \notin \Delta _r$ and $\mathbf {F}\neg \varphi \to \neg \mathbf {G}\phi $ is an $\mathrm {L}_{\mathbb {R}}$ -theorem, we must have $\mathbf {F}\neg \varphi \notin \Delta _r$ , hence $\mathbf {F}\neg \varphi \notin \Delta _r^0$ . This also gives (10), by Lemma 6(1). Now to show that $r\in [<]|\varphi |_{\mathbb {R}}$ , take any s with $r<s$ . Then we need to show that $\varphi \in \Delta _s$ . If $s\in \mathbb {Q}$ , (10) immediately gives $\mathcal {M},s\models \varphi $ , hence $\varphi \in \Delta _s$ . If $s\notin \mathbb {Q}$ , take a rational $q_1$ with $r<q_1<s$ . Then (10) implies that every rational q greater than $q_1$ has $\mathcal {M},q\models \varphi $ . Hence $\mathcal {M},{q_1}\models \mathbf {G}\varphi $ . Therefore $\mathbf {PG}\varphi \in \Delta _s^0$ by Lemma 6(3). By the $\mathrm {L}_{\mathbb {R}}$ -theorem $\mathbf {PG}\varphi \to \varphi $ , this implies $\varphi \in \Delta _s$ as required.

That concludes the proof of the first equation of the lemma. The proof of the second is its mirror image.

Lemma 10. If $\forall x\varphi $ is an ${\cal L}^{+}$ -sentence, then in $\mathcal {M}^*$ , .

Proof. For any $r\in \mathbb {R}$ , if $\forall x\varphi \in \Delta _r$ , then for all $a\in U$ , by the Universal Instantiation axiom we get $\varphi (\bar {a}/x)\in \Delta _r$ , as maximal sets are closed under modus ponens. Thus $|\forall x\varphi |_{\mathbb {R}}\subseteq \mathop {\textstyle \bigcap }_{a\in U}|\varphi (\bar {a}/x)|_{\mathbb {R}}$ . But $|\forall x\varphi |_{\mathbb {R}}\in \mathit {Prop}$ , so then .

Conversely, let . Then there is some $X\in \mathit {Prop}$ with $r\in X$ and

(11) $$ \begin{align} X\subseteq \mathop{\textstyle\bigcap}_{a\in U}|\varphi(\bar{a}/x)|_{\mathbb{R}}. \end{align} $$

Now $X=|\psi |_{\mathbb {R}}$ for some sentence $\psi $ . We show that $\mathcal {M}\models \psi \to \forall x\varphi $ . For if $\mathcal {M},q\models \psi $ , then $\psi \in \Delta _q$ , hence $q\in X$ , so by (11), for all $a\in U$ we get $q\in |\varphi (\bar {a}/x)|_{\mathbb {R}}$ , so $\mathcal {M},q\models \varphi (\bar {a}/x)$ . Then $\mathcal {M},q\models \forall x\varphi $ as $\mathcal {M}$ is Kripkean (9). This shows that $\mathcal {M},q\models \psi \to \forall x\varphi $ for all q in $\mathbb {Q}$ as claimed.

By Lemma 8 it follows that $|\psi \to \forall x\varphi |_{\mathbb {R}}=\mathbb {R}$ . This yields $|\psi |_{\mathbb {R}}\subseteq |\forall x\varphi |_{\mathbb {R}}$ . But $r\in |\psi |_{\mathbb {R}}$ , so we get $r\in |\forall x\varphi |_{\mathbb {R}}$ as required to complete the proof.

Theorem 11. For any ${\cal L}^{+}$ -sentence $\varphi $ , $|\varphi |^{\mathcal {M}^*}=|\varphi |_{\mathbb {R}}$ , i.e., for all $r\in \mathbb {R}$ , $\mathcal {M}^*,r\models \varphi $ iff $\varphi \in \Delta _r$ .

Proof. By induction on the number of connectives and quantifiers of $\varphi $ .

If $\varphi $ is an atomic sentence $P\tau _1\cdots \tau _n$ , then the $\tau _i$ are closed terms and the semantics gives

$$ \begin{align*}|\varphi|^{\mathcal{M}^*}=|P|^{\mathcal{M}^*}(|\tau_1|^{\mathcal{M}^*},\dots,|\tau_n|^{\mathcal{M}^*}). \end{align*} $$

Putting $a_i=|\tau _i|^{\mathcal {M}^*}$ , the definition of $|P|^{\mathcal {M}^*}$ yields $|\varphi |^{\mathcal {M}^*}= |P\overline {a_1}\cdots \overline {a_n}|_{\mathbb {R}}$ .

Now the models $\mathcal {M}$ and $\mathcal {M}^*$ agree on all constant terms, so $|\overline {a_i}|^{\mathcal {M}}=a_i=|\tau _i|^{\mathcal {M}}$ . Hence the sentence

$$ \begin{align*}P\overline{a_1}\cdots\overline{a_n} \leftrightarrow P\tau_1\cdots\tau_n \end{align*} $$

is true throughout $\mathcal {M}$ , so belongs to every $\Delta _r$ by Lemma 8. Therefore $|P\overline {a_1}\cdots \overline {a_n}|_{\mathbb {R}} =|P\tau _1\cdots \tau _n|_{\mathbb {R}}$ , giving $|P\tau _1\cdots \tau _n|^{\mathcal {M}^*} =|P\tau _1\cdots \tau _n|_{\mathbb {R}}$ as required.

The other base case is when the sentence $\varphi $ is an identity $\tau _1\approx \tau _2$ . Then we either have $|\tau _1|^{\mathcal {M}^*}=|\tau _2|^{\mathcal {M}^*}$ and $|\tau _1\approx \tau _2|^{\mathcal {M}^*}=\mathbb {R}$ , or $|\tau _1|^{\mathcal {M}^*}\ne |\tau _2|^{\mathcal {M}^*}$ and ${|\tau _1\approx \tau _2|^{\mathcal {M}^*}=\emptyset} $ . Since $|\tau _i|^{\mathcal {M}^*}=|\tau _i|^{\mathcal {M}}$ , the first option gives $|\tau _1|^{\mathcal {M}}=|\tau _2|^{\mathcal {M}}$ , hence $\mathcal {M}\models \tau _1\approx \tau _2$ , and so $|\tau _1\approx \tau _2|_{\mathbb {R}}=\mathbb {R}$ by Lemma 8. The second option gives $|\tau _1|^{\mathcal {M}}\ne |\tau _2|^{\mathcal {M}}$ , hence $\mathcal {M}\models \neg (\tau _1\approx \tau _2)$ , so $|\neg (\tau _1\approx \tau _2)|_{\mathbb {R}}=\mathbb {R}$ , and thus $|\tau _1\approx \tau _2|_{\mathbb {R}}=\emptyset $ . Both options have $|\tau _1\approx \tau _2|^{\mathcal {M}^*}=|\tau _1\approx \tau _2|_{\mathbb {R}}$ as required.

The inductive cases for the Boolean connectives are standard by properties of maximal sets, e.g., assuming the result for $\varphi $ we have

$$ \begin{align*}|\neg\varphi|^{\mathcal{M}^*}=\mathbb{R}-|\varphi|^{\mathcal{M}^*}= \mathbb{R}-|\varphi|_{\mathbb{R}}=|\neg\varphi|_{\mathbb{R}}. \end{align*} $$

For the temporal modalities we have

$$ \begin{align*}\begin{array}{ll@{\qquad}l} |\mathbf{G}\varphi|^{\mathcal{M}^*}\kern-10pt &= [<] |\varphi|^{\mathcal{M}^*} &\text{semantics of }\mathbf{G} \\ &= [<] |\varphi|_{\mathbb{R}} &\text{induction hypothesis} \\ &= |\mathbf{G}\varphi|_{\mathbb{R}} &\text{Lemma 9}, \end{array} \end{align*} $$

and similarly for $\mathbf {H}$ . For the quantifiers we have

Corollary 12. $\mathcal {M}^*$ is an ${\cal L}^{+}$ -model, i.e., any ${\cal L}^{+}$ -formula $\varphi $ is admissible in $\mathcal {M}$ .

Proof. For any variable assignment $f:\mathsf {Var}\to U$ , by the version of Lemma 3 that holds for $\mathcal {M}^*$ we have $|\varphi |^{\mathcal {M}^*}f=|\varphi ^f|^{\mathcal {M}^*}=|\varphi ^f|_{\mathbb {R}}\in \mathit {Prop}$ , as required.

Corollary 13.

1. (1) For any sentence $\varphi $ and $q\in \mathbb {Q}$ , $\mathcal {M}^*,q\models \varphi $ iff $\mathcal {M},q\models \varphi $ .

2. (2) For any formula $\varphi $ , $q\in \mathbb {Q}$ , and $f:\mathsf {Var}\to U$ , $\mathcal {M}^*,q,f\models \varphi $ iff $\mathcal {M},q,f\models \varphi $ .

Proof. (1) This follows from the Theorem, as $\varphi \in \Delta _q$ iff $\mathcal {M},q\models \varphi $ .

(2) This follows from part (1) and Lemma 3 for $\mathcal {M}$ and $\mathcal {M}^*$ , using the sentence $\varphi ^f$ .

From the last result and the fact that $\mathcal {M},q_0,f_0\models \Delta ^+$ we infer that $\mathcal {M}^*,q_0,f_0\models \Delta ^+$ , hence $\mathcal {M}', q_0,f_0\models \Delta $ , where $\mathcal {M}'$ is the ${\cal L}$ -reduct of $\mathcal {M}^*$ . That concludes the proof of strong completeness of $\mathrm {L}_{\mathbb {R}}$ for admissible ${\cal L}$ -models over $(\mathbb {R},<)$ .

The model $\mathcal {M}^*$ need not be Kripkean. Indeed there must be an $\mathrm {L}_{\mathbb {R}}$ -consistent formula $\varphi $ that is not satisfiable in any Kripkean model over $\mathbb {R}$ . Otherwise, $\mathrm {L}_{\mathbb {R}}$ would be complete for validity in such models, contrary to Scott’s non-axiomatisability result. So an $\mathcal {M}^*$ satisfying this $\varphi $ , as produced by the above construction, must be non-Kripkean.

The Barcan formulas (1) are valid in Kripkean models, and play an essential role in the completeness proof for $\mathrm {L}_{\mathbb {Q}}$ of Theorem 2, in showing that certain sets are $\forall $ -complete, which enables a Kripkean model to be constructed [5, p. 121]. But $\mathcal {M}^*$ validates $\mathrm {L}_{\mathbb {R}}$ , since it is an admissible model over $(\mathbb {R},<)$ , and hence it validates the Barcan formulas, since they are $\mathrm {L}_{\mathbb {R}}$ -theorems, even though $\mathcal {M}^*$ is not in general Kripkean.

The $\mathcal {M}^*$ construction only requires $\Delta _r$ to be maximally consistent, not $\forall $ -complete as would be required to get a Kripkean model. While the Kripkean condition is sufficient for validity of the Barcan formulas, we see now that it is not necessary.

5. Non-axiomatisability over $\mathbb {Z}$

Scott’s work on non-axiomatisability of the temporal logic of standard models is not published. A detailed treatment of the topic is given in [5, sec. 4.6]. We now analyse this further to show that the temporal logic of admissible models over $\mathbb {Z}$ is not recursively axiomatisable.

Let ${\cal L}_{\mathrm {a}}=\{0,{}',+,\times \}$ be the signature for the first-order language of arithmetic, with identity. Let ${\cal N}=(\omega ,0,{}',+,\times )$ be the standard model of arithmetic, comprising the set of natural numbers on which $0,{}',+,\times $ have their standard arithmetical meanings.

Let ${\cal L}={\cal L}_{\mathrm {a}} \cup \{e,q,\prec \}$ where e and q are unary predicate symbols and $\prec $ is a binary predicate symbol. We will be concerned with admissible models for this signature based on the integer time flow, i.e., models of the form

(12) $$ \begin{align} \mathcal{M}=(\mathbb{Z},<,\mathit{Prop},U,|\mathord{-}|^{\mathcal{M}}). \end{align} $$

The symbols of ${\cal L}_{\mathrm {a}}$ are interpreted as operations on the universe U. We will abbreviate the interpretation $|0|^{\mathcal {M}}$ of $0$ to $0^{\mathcal {M}}$ , and write the interpretations $|'|^{\mathcal {M}}$ , $|+|^{\mathcal {M}}$ , $|\times |^{\mathcal {M}}$ of the other function symbols just as ${}',+,\times $ , allowing the context to determine what is intended. The role of the predicate e will be to provide an embedding of U into $\mathbb {Z}$ by associating with each $a\in U$ a unique time in $\mathbb {Z}$ at which a satisfies e. The symbol $\prec $ will rigidly define an ordering on U that matches $<$ under this embedding. The role of q will be to single out a subset $U_q$ of U that is closed under the operations interpreting ${\cal L}_{\mathrm {a}}$ and forms an isomorphic copy of the standard model ${\cal N}$ . The interpretation $|q|^{\mathcal {M}}:U\to \mathit {Prop}$ of q will also be rigid, so $|q|^{\mathcal {M}}(a)$ is either $\mathbb {Z}$ or $\emptyset $ .

Let $\mu $ be the conjunction of the following sentences:

1. (i) $\forall x\lozenge \big (e(x)\land \mathbf {G}\neg e(x) \land \mathbf {H}\neg e(x)\big )$ .

2. (ii) $\Box \forall x\forall y(e(x)\land e(y)\to x\approx y)$ .

3. (iii) $\Box \forall x\forall y\big ( x\prec y \leftrightarrow \lozenge (e(x)\land \mathbf {F} e(y)\big )$ .

4. (iv) $\Box \forall x(q(x)\to \Box q(x))$ .

5. (v) $\Box [ q(0)\land \forall y (y\prec 0 \to \neg q(y)) ]$ .

6. (vi) $\Box \forall x[q(x) \to (x\prec x'\land q(x')\land \forall z(x\prec z\land z\prec x' \to \neg q(z)))]$ .

7. (vii) $\Box \forall x\forall y[q(x)\land q(y) \to q(x+y)\land q(x\times y)]$ .

8. (viii) $\Box \forall x(q(x) \to x+0\approx x)$ .

9. (ix) $\Box \forall x\forall y[q(x)\land q(y) \to x+y'\approx (x+y)' ]$ .

10. (x) $\Box \forall x(q(x) \to x\times 0\approx 0)$ .

11. (xi) $\Box \forall x\forall y[q(x)\land q(y) \to x\times y'\approx (x\times y)+x]$ .

These correspond to the sentences (1)–(11) in [5, p. 130], except for (ii) which replaces the stronger

$$ \begin{align*}\Box\exists x (e(x)\land \forall y(x\not \approx y \to \neg e(y))) \end{align*} $$

used in that reference. It is significant that $\mu $ as defined here contains no existential quantifiers, and its occurrences of $\forall $ allow us to apply the principle that

(3) $$ \begin{align} \mathcal{M},t,f\models\forall x\varphi \text{ implies}\quad \mathcal{M},t,f[a/x]\models\varphi \text{ for all } a\in U, \end{align} $$

which holds in all admissible models (but its converse may not). For instance, if sentence (iv) holds at some time in $\mathcal {M}$ , then the sentence $\forall x(q(x)\to \Box q(x))$ holds at all times, so from (3), for each $a\in U$ , if a satisfies q at some t, i.e., $t\in |q|^{\mathcal {M}}(a)$ , then a satisfies q at every time, hence $|q|^{\mathcal {M}}(a)=\mathbb {Z}$ . Otherwise $|q|^{\mathcal {M}}(a)=\emptyset $ . Thus q is interpreted rigidly in $\mathcal {M}$ . In what follows, the use of sentences (i)–(xi) all depend in this sort of way on (3) but not its converse.

Let $U_q=\{a\in U: |q|^{\mathcal {M}}(a)\ne \emptyset \}$ . We now show that the sentence $\mu $ forces $U_q$ to be a copy in $\mathcal {M}$ of the standard model of arithmetic.

Theorem 14. Let $\mathcal {M}$ be an admissible ${\cal L}$ -model over integer time as in (12). If the sentence $\mu $ holds at some point of $\mathbb {Z}$ in $\mathcal {M}$ , then $U_q$ is closed under the operations interpreting $0,{}',+,\times $ and forms an ${\cal L}_{\mathrm {a}}$ -model ${\cal U}_q$ isomorphic to ${\cal N}$ .

Proof. Assume $\mu $ holds at some point in $\mathcal {M}$ , hence each of its conjuncts does. Applying principle (3) to sentence (i) we get that for each $a\in U$ there is exactly one time $t\in \mathbb {Z}$ at which a satisfies e. Put $\theta (a)=t$ . This defines a function $\theta :U\to \mathbb {Z}$ . By sentence (ii), $\theta $ is injective.

By sentence (iii), for any $a,b\in U$ and any time $t\in \mathbb {Z}$ , we have $t\in |{\prec }|^{\mathcal {M}}(a,b)$ iff $\theta (a)<\theta (b)$ . So $\prec $ is interpreted rigidly in $\mathcal {M}$ and defines a binary relation $\prec ^{\mathcal {M}}$ on U by putting $a\prec ^{\mathcal {M}} b$ iff $|{\prec }|^{\mathcal {M}}(a,b)\ne \emptyset $ iff $|{\prec }|^{\mathcal {M}}(a,b)=\mathbb {Z}$ , making $a\prec ^{\mathcal {M}} b$ iff $\theta (a)<\theta (b)$ . It follows that $\prec ^{\mathcal {M}}$ inherits many properties of the ordering $<$ , including transitivity, irreflexivity and linearity.

As noted above, (iv) ensures that q is interpreted rigidly, so $U_q=\{a\in U: |q|^{\mathcal {M}}(a)=\mathbb {Z}\}$ . Sentence (v) ensures that $0^{\mathcal {M}}$ belongs to $U_q$ , while sentences (vi) and (vii) yield that $U_q$ is closed under the operations ${}',+,\times $ , so forms an ${\cal L}_{\mathrm {a}}$ -structure ${\cal U}_q$ .

A sequence $\{a_n:n<{\omega }\}$ of distinct elements of $U_q$ can be defined inductively by putting $a_0=0^{\mathcal {M}}$ and $a_{n+1}=a_n^{\prime }$ . By (vi), $a_n\prec ^{\mathcal {M}} a_{n+1}$ , so we have a strictly increasing sequence

$$ \begin{align*}a_0\prec^{\mathcal{M}} a_1\prec^{\mathcal{M}}\cdots \cdots a_n\prec^{\mathcal{M}} a_{n+1}\prec^{\mathcal{M}} \cdots\cdots\cdots \end{align*} $$

Now we show that $U_q=\{a_n:n<\omega \}$ . First, (v) ensures that $a_0$ is the $\prec ^{\mathcal {M}}$ -least member of $U_q$ , and (vi) ensures that there is no member of $U_q$ that is $\prec ^{\mathcal {M}}$ -between $a_n$ and $a_{n+1}$ for any $n<\omega $ . Therefore if there exists some $b\in U_q$ with $b\ne a_n$ for all $n<\omega $ , then we must have $a_n\prec ^{\mathcal {M}} b$ for all n. Applying the injective order-preserving $\theta $ then gives $\theta (a_0)< \theta (a_{n})<\theta (b)$ for all $n>0$ . But this is impossible, as there are infinitely many $\theta (a_n)$ ’s, but only finitely many integers between $\theta (a_0)$ and $\theta (b)$ . So we conclude that b cannot exist, and therefore $U_q=\{a_n:n<\omega \}$ .

The sentences (viii)–(xi) can be used to show, by induction on n, that in general $a_{m+n}=a_m+a_n$ and $a_{m\times n}=a_m\times a_n$ . Thus the map $n\mapsto a_n$ is an isomorphism from ${\cal N}$ onto ${\cal U}_q=(U_q,0^{\mathcal {M}},{}',+,\times )$ .

To discuss the language of arithmetic within $\mathcal {M}$ we relativise the quantifiers of ${\cal L}_{\mathrm {a}}$ -formulas to range over $U_q$ . A translation is inductively defined, taking each ${\cal L}_{\mathrm {a}}$ -formula $\varphi $ to an ${\cal L}_{\mathrm {a}}\cup \{q\}$ -formula $\varphi _q$ , by putting $\varphi _q=\varphi $ if $\varphi $ is atomic; letting the map $\varphi \mapsto \varphi _q$ commute with the Boolean connectives, i.e., $(\neg \varphi )_q=\neg (\varphi _q)$ , $(\varphi \land \psi )_q=\varphi _q\land \psi _q$ etc.; and $(\forall x\varphi )_q=\forall x(q(x)\to \varphi _q)$ .

Lemma 15. Let $\mathcal {M}=(T,<,\mathit {Prop},U,|\mathord {-}|^{\mathcal {M}})$ be any admissible ${\cal L}$ -model in which $q$ is interpreted rigidly and $U_q$ is a subalgebra of $(U,0^{\mathcal {M}},{}',+,\times )$ . Let $\varphi $ be any ${\cal L}_{\mathrm {a}}$ -formula. Then for any variable assignment $f:\mathsf {Var}\to U_q$ and any $t\in T$ , we have ${\cal U}_q,f\models \varphi $ iff $\mathcal {M},t,f\models \varphi _q$ .

Proof. Since $U_q$ is closed under $0,{}',+,\times $ , it forms an ${\cal L}_{\mathrm {a}}$ -structure ${\cal U}_q$ in which any interpretation $|\tau |^{{\cal U}_q}f$ of any ${\cal L}_{\mathrm {a}}$ -term is identical to $|\tau |^{\mathcal {M}}f$ . The notation ${\cal U}_q,f\models \varphi $ expresses the classical (non-modal) satisfaction relation in this structure. In particular

(13) $$ \begin{align} {\cal U}_q,f\models\forall x\varphi \text{ iff every } a\in U_q \text{ has } {\cal U}_q,f[a/x]\models\varphi. \end{align} $$

The statement of the lemma implies that the formulas $\varphi _q$ are interpreted rigidly in $\mathcal {M}$ : if $\mathcal {M},t,f\models \varphi _q$ holds for some t then it holds for all.

We prove the lemma by induction on the formation of ${\cal L}_{\mathrm {a}}$ -formulas, which are constructed from atomic formulas by Boolean connectives and $\forall $ . If $\varphi $ is atomic, then it is an equation $\tau _1\approx \tau _2$ , and is equal to $\varphi _q$ . We have ${\cal U}_q,f\models \tau _1\approx \tau _2$ iff $|\tau _1|^{{\cal U}_q}f=|\tau _2|^{{\cal U}_q}f$ iff $|\tau _1|^{\mathcal {M}}f=|\tau _2|^{\mathcal {M}}f$ , which is precisely the condition for $\mathcal {M},t,f\models \tau _1\approx \tau _2 $ to hold for any $t\in T$ . Hence the lemma holds for atomic formulas.

The inductive cases of the Boolean connectives are straightforward. For the case of $\forall $ , assume inductively that the result holds for $\varphi $ . Suppose ${\cal U}_q,f\models \forall x\varphi $ . For any $t\in T$ and $a\in U$ , if $\mathcal {M},t,f[a/x]\models q(x)$ , then $t\in |q|^{\mathcal {M}}(a)$ so $a\in U_q$ , hence ${\cal U}_q,f[a/x]\models \varphi $ by (13), therefore $\mathcal {M},t,f[a/x]\models \varphi _q$ by the induction hypothesis on $\varphi $ .

This shows that $\mathcal {M},t,f[a/x]\models q(x)\to \varphi _q$ for every $t\in T$ and $a\in U$ . Hence

(14) $$ \begin{align} \bigcap\nolimits_{a\in U}| q(x)\to\varphi_q|^{\mathcal{M}}f[a/x]=T. \end{align} $$

But $T\in \mathit {Prop}$ , so any $t\in T$ belongs to a member of $\mathit {Prop}$ that is included in the left side of this last equation. By the admissible semantics of $\forall $ , this means that $\mathcal {M},t,f\models \forall x(q(x)\to \varphi _q)$ , i.e., $\mathcal {M},t,f\models (\forall x \varphi )_q$ .

Conversely, suppose $\mathcal {M},t,f\models (\forall x \varphi )_q$ . Then each $a\in U_q$ has $\mathcal {M},t,f[a/x]\models q(x)\to \varphi _q$ (see (3)), and $\mathcal {M},t,f[a/x]\models q(x)$ as $|q|^{\mathcal {M}}(a)=\mathbb {Z}$ , so then $\mathcal {M},t,f[a/x]\models \varphi _q$ . Hence ${\cal U}_q,f[a/x]\models \varphi $ by the induction hypothesis on $\varphi $ . This shows ${\cal U}_q,f\models \forall x\varphi $ by (13).

Altogether now we have shown that the lemma holds for $\forall x\varphi $ , completing the inductive case of $\forall $ , and hence the inductive proof for all formulas.

Theorem 16. An ${\cal L}_{\mathrm {a}}$ -sentence $\varphi $ is true in ${\cal N}$ iff the ${\cal L}$ -sentence $\mu \to \varphi _q$ is valid in all admissible ${\cal L}$ -models over $(\mathbb {Z},<)$ .

Proof. Suppose ${\cal N}\models \varphi $ . If $\mathcal {M}$ is admissible over $(\mathbb {Z},<)$ and $\mathcal {M},t\models \mu $ , then by Theorem 14 the ${\cal L}_{\mathrm {a}}$ -structure ${\cal U}_q$ within $\mathcal {M}$ is isomorphic to ${\cal N}$ , hence ${\cal U}_q\models \varphi $ , so $\mathcal {M},t\models \varphi _q$ by Lemma 15. This shows $\mathcal {M},t\models \mu \to \varphi _q$ for any $t\in \mathbb {Z}$ , i.e., $\mu \to \varphi _q$ is valid in $\mathcal {M}$ .

Conversely let $\mu \to \varphi _q$ be valid in all admissible models over the time flow $(\mathbb {Z},<)$ . Define such a model $\mathcal {M}$ by putting $\mathit {Prop}=\wp \mathbb {Z}$ , the full powerset of $\mathbb {Z}$ , and $U=\mathbb {Z}$ , with the symbols of ${\cal L}_{\mathrm {a}}$ having their standard interpretations in $\mathbb {Z}$ . Interpret e in $\mathcal {M}$ by defining $|e|^{\mathcal {M}}(a)=\{a\}\in \mathit {Prop}$ for all $a\in U$ . For q define $|q|^{\mathcal {M}}(a)$ to be $\mathbb {Z}$ if $a\in \omega $ , and $\emptyset $ otherwise. Then q is interpreted rigidly in $\mathcal {M}$ , and $U_q=\omega $ , so $U_q$ is closed under the ${\cal L}_{\mathrm {a}}$ -operations. For $\prec $ define $|{\prec }|^{\mathcal {M}}(a,b)$ to be $\mathbb {Z}$ if $a<b$ , and $\emptyset $ otherwise. Then the relation $\prec ^{\mathcal {M}}$ on $U (=\mathbb {Z})$ is $<$ .

Taking any $t\in \mathbb {Z}$ , we have that $\mathcal {M},t\models \mu $ , with $\theta :U\to \mathbb {Z}$ being the identity function on $\mathbb {Z}$ . By the assumed validity of $\mu \to \varphi _q$ we get $\mathcal {M},t\models \varphi _q$ , so by Lemma 15, ${\cal U}_q\models \varphi $ . But the ${\cal L}_{\mathrm {a}}$ -structure ${\cal U}_q$ in this case is just ${\cal N}$ , so ${\cal N}\models \varphi $ as required.

Corollary 17. The set of formulas valid in all admissible ${\cal L}$ -models over integer time is not recursively axiomatisable.

Proof. This is a well-known argument. Any recursively axiomatisable logic has a recursively enumerable set of theorems [3, theorem 7.1]. But from a recursive enumeration of the formulas valid in all admissible ${\cal L}$ -models over $\mathbb {Z}$ we could obtain via Theorem 16 a recursive enumeration of the true sentences of the standard model of arithmetic, something that does not exist.

In Theorem 14 the negative members of $\mathbb {Z}$ do not play a particular role and can be dispensed with. The theorem remains true if $\mathbb {Z}$ is replaced by $\omega $ as the time flow, leading to a proof that the logic of formulas valid in admissible models over natural number time is not recursively axiomatisable.

This non-axiomatisability of logics over $\mathbb {Z}$ or $\omega $ is covered by the more general fact that it holds for the temporal logic of admissible models over any scattered linear order, which is one that does not contain any dense suborder, i.e., one into which $\mathbb {Q}$ cannot be order-embedded. Hausdorff showed that if ${\cal O}$ is the class of all well-orderings and their inverses, then the scattered linear orders form the smallest class of linear orderings that includes ${\cal O}$ and is closed under lexicographical sums indexed by a member of ${\cal O}$ [12, sec. 5.3].

If the ${\cal L}$ -sentence $\mu $ is modified by adding the sentences (12)–(15) of [5, p. 131] as conjuncts, then by the analysis given in that reference, if the sequence $\{a_n:n<\omega \}$ in the proof of our Theorem 14 did not exhaust $U_q$ , then there would exist an order-embedding $\eta :(\mathbb {Q}\,<)\to (U_q,\prec ^{\mathcal {M}})$ . The modified $\mu $ has a single subformula of the form $\exists z\psi $ , but the formula $\psi $ there is rigid, so the existential quantifier gets the Kripkean interpretation (8). Hence the analysis of [5] for a standard model holds also for an admissible one. Then composing $\eta $ with the map $\theta $ from the proof of Theorem 14 would give an order-embedding of $\mathbb {Q}$ into the time flow of $\mathcal {M}$ , showing that the latter was not scattered. Accordingly, if the time flow is scattered, then $U_q=\{a_n:n<\omega \}$ . This leads to a proof that the logic of formulas valid in admissible models over a scattered time flow is not recursively axiomatisable.

Finally, noting that our results imply that Theorem 14 must fail in general for models over the real time flow, we construct an ${\cal L}$ -model $\mathcal {M}=(\mathbb {R},<,\mathit {Prop},U,|\mathord {-}|^{\mathcal {M}})$ that exhibits this failure. $\mathcal {M}$ satisfies the sentence $\mu $ but does not have ${\cal U}_q$ isomorphic to the standard model of arithmetic ${\cal N}$ .

Let $\mathit {Prop}=\wp \mathbb {R}$ . Take ${\cal U}=(U,0,{}',+,\times )$ to be a countable nonstandard model of arithmetic, say a proper elementary ${\cal L}_{\mathrm {a}}$ -extension of ${\cal N}$ . Interpret q to hold rigidly in $\mathcal {M}$ of every member of this structure, i.e., $|q|^{\mathcal {M}}(a)=\mathbb {R}$ for all $a\in U$ . Then ${\cal U}_q$ is just ${\cal U}$ , which is not isomorphic to ${\cal N}$ . Interpret $\prec $ rigidly to be the ordering relation of ${\cal U}$ .

To interpret e, suppose temporarily that we have an injective order-preserving function $\theta $ from U to $\mathbb {R}$ . Then we use it to define $|e|^{\mathcal {M}}(a)=\{\theta (a)\}$ for all $a\in U$ , completing the definition of $\mathcal {M}$ . It can then be seen that $\mathcal {M},t\models \mu $ for any $t\in \mathbb {R}$ .

So it remains to show that a $\theta $ as described does exist. We use the well-known description of non-standard models of arithmetic [11, sec. 3.1.]: ${\cal U}$ comprises a standard part, a copy of ${\cal N}$ , followed linearly by countably many pairwise disjoint copies of $(\mathbb {Z},{}')$ , called galaxies. A typical galaxy looks like

$$ \begin{align*}\cdots\cdots\prec^{\mathcal{M}}\bullet \prec^{\mathcal{M}} a\prec^{\mathcal{M}} a'\prec^{\mathcal{M}} a"\prec^{\mathcal{M}}\cdots\cdots. \end{align*} $$

The set of galaxies is linearly ordered by declaring one galaxy to be less than another if every member of the first is $\prec ^{\mathcal {M}}$ -less than every member of the second in ${\cal U}$ . There is no least galaxy in this ordering and no greatest, while between any two galaxies there lies a third. So the set of galaxies forms a countable dense linear ordering without endpoints, and hence is isomorphic to the ordered set $(\mathbb {Q},<)$ of rationals, by a celebrated theorem of Cantor [12, theorem 2.8].

Any galaxy $\varGamma $ can be embedded into any open interval I of the real line. Let $\varGamma =\{a_j:j\in \mathbb {Z}\}$ with $a_j\prec ^{\mathcal {M}} a_k$ iff $j<k$ . Use the density of the reals to find a subset $\{t_j:j\in \mathbb {Z}\}$ of I with $t_j < t_k$ iff $j<k$ . Then the map $a_j\mapsto t_j$ is an order preserving embedding of $(\varGamma ,\prec ^{\mathcal {M}})$ into $(I,<)$ .

To define $\theta $ we need a countable collection ${\cal I}$ of pairwise disjoint open intervals of $\mathbb {R}$ that we can match bijectively with the galaxies, and with ${\cal I}$ having the same order type as $(\mathbb {Q},<)$ under the linear ordering $\lessdot $ that puts $(s,t)\lessdot (s',t')$ iff $(s,t)$ is strictly to the left of $(s',t')$ , i.e., iff $t<s'$ . We can find such an ${\cal I}$ within any given open interval $(r,s)$ on the real line. As a first step choose some proper subinterval $(r_1,s_1)$ of $(r,s)$ and put it into ${\cal I}$ .

$$ \begin{align*}r \text{ --------------------------- } r_1 \cdots\cdots s_1 \text{ --------------------------- } s. \end{align*} $$

This leaves two ‘open pieces’ $(r,r_1)$ and $(s_1,s)$ within $(r,s)$ . At step two choose proper subintervals $(r_{21},s_{21})$ and $(r_{22},s_{22})$ of $(r,r_1)$ and $(s_1,s)$ , respectively, and put them into ${\cal I}$ .

$$ \begin{align*}r \text{ ------ } r_{21} \cdots s_{21} \text{ ------ } r_1 \cdots\cdots s_1 \text{ ------ } r_{22}\cdots s_{22} \text{ ------ } s. \end{align*} $$

That leaves four open pieces within $(r,s)$ to have proper subintervals chosen. Iterating these steps countably many times gives the desired ${\cal I}$ whose ordering $\lessdot $ is dense and without end-points.

For the definition of $\theta $ , start with the standard part of ${\cal U}$ , which can be identified as an ordered set with $(\omega ,<)$ , and put $\theta (n)=\frac {n}{n+1}$ for all $n\in \omega $ to give an order-preserving injection of $(\omega ,<)$ into the interval $[0,1)$ of $\mathbb {R}$ . Then take any open interval $(r,s)$ with $1\leq r$ and let $({\cal I},\lessdot )$ be the ordered set of open subintervals of $(r,s)$ constructed above. There is an order-isomorphism $\eta $ from the set of galaxies onto $({\cal I},\lessdot )$ , because both structures have the same order type as $(\mathbb {Q},<)$ . Extend $\theta $ to act on each galaxy $\varGamma $ as an order preserving embedding of $(\varGamma ,\prec ^{\mathcal {M}})$ into $(\eta (\varGamma ),<)$ , as described above. That completes the construction of $\theta $ as an order-preserving injection of $(U,\prec ^{\mathcal {M}})$ into the real line, and hence completes the counter-example to Theorem 14 over $\mathbb {R}$ .

5.1. Until and Since

We conclude with some observations about temporal logic based on the binary connectives $\mathbf {U}$ (‘until’) and $\mathbf {S}$ (‘since’). $\mathbf {G}$ and $\mathbf {H}$ are definable from these, so the non-recursive-enumerability of the formulas in the first-order $\mathbf {G,H}$ -language that are valid in standard models over $(\mathbb {R},<)$ implies non-recursive-enumerability of the formulas in the first-order $\mathbf {U,S}$ -language that are valid in such models. Hence the first-order $\mathbf {U,S}$ -logic of standard models over the reals is not recursively axiomatisable.

Now the propositional $\mathbf {U,S}$ -logic of the reals fails to have compactness. There is a set $\Sigma $ of propositional $\mathbf {U,S}$ -formulas that is not satisfiable in any model on $(\mathbb {R},<)$ , while each of its finite subsets has such a satisfying model [5, proposition 6.9.2]. We can turn $\Sigma $ into a set $\Sigma '$ of quantifier-free first-order $\mathbf {U,S}$ -formulas by replacing each propositional variable by a distinct atomic formula of the form $Px$ with P a unary predicate symbol. Then $\Sigma '$ shows that compactness fails for the first-order $\mathbf {U,S}$ -logic of admissible models over the reals (not just the standard ones). But a logic that is strongly complete over a class of models will have compactness over that class, provided it has the kind of finitary proof theory we have dealt with here, making a set consistent whenever each finite subset is consistent, and provided it is sound over the class, so that every finite satisfiable set is consistent.

We infer from all this that, unlike the $\mathbf {G,H}$ case, there can be no strongly complete axiomatisation of the first-order $\mathbf {U,S}$ -logic of admissible models over the reals. It remains to be seen whether there is a simply complete recursive axiomatisation.