# Strong completeness of a first-order temporal logic for real time

Robert Goldblatt School of Mathematics and Statistics, Victoria University of
Wellington, New Zealand. sms.vuw.ac.nz/$\sim$rob

###### 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.

#### Keywords.

temporal logic, recursively axiomatisable, admissible model

MSC2020 classification: 03B44

##  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 [2, §7]. For instance, if the flow of time is modelled
by the linearly ordered set $(\mathbb{R},<)$ of real numbers, then the
resulting temporal logic of valid _propositional_ formulas is recursively
axiomatisable. This was shown by Robert Bull [1], using finitely many axioms
and inference rules.

The situation of _first-order_ temporal logic is quite different. Dana Scott
proved in the 1960’s that the logic of first-order temporal models over the
reals has in general 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?

We give a positive answer to this question by adapting the ‘admissible”
semantics for quantified modal logic developed in [6, 5]. 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

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

An admissible model has instead that

$|\forall
x\varphi|^{\mathcal{M}}=\mathop{\textstyle\bigsqcap}\\{|\varphi(a/x)|^{\mathcal{M}}:a\in
U\\},$

where $\mathop{\textstyle\bigsqcap}$ 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

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

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
[5, §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

$\dfrac{\varphi,\ \varphi\to\psi}{\psi}$ |   _Modus Ponens_
---|---
$\dfrac{\varphi}{\mathbf{G}\varphi}$ , $\dfrac{\varphi}{\mathbf{H}\varphi}$ |   _Temporal Generalisation_
$\dfrac{\varphi}{\forall x\varphi}$ |   _Universal Generalisation_

We adopt the following axioms about quantifiers.

$\forall x\varphi\to\varphi(\tau/x)$, where $\tau$ is free for $x$ in $\varphi$. |   _Universal Instantiation_
---|---
$\forall x(\varphi\to\psi)\to(\forall x\varphi\to\forall x\psi)$ |   _Universal Distribution_
$\varphi\to\forall x\varphi$, where $x$ is not free in $\varphi$. |   _Vacuous Quantification_

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

$\tau\approx\tau$ |   _Self Identity_
---|---
$\tau\approx\tau^{\prime}\to(\varphi\to\varphi(\tau^{\prime}/\\!/\tau))$, with $\varphi$ atomic. |   _Substitution of Identicals_
$\tau\approx\tau^{\prime}\to\Box(\tau\approx\tau^{\prime})$ |   _Rigid Identity_

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.

$\mathbf{G}(\varphi\to\psi)\to(\mathbf{G}\varphi\to\mathbf{G}\psi)$ |
---|---
$\varphi\to\mathbf{G}\mathbf{P}\varphi$ |

Members of $\mathrm{L}$ are called _$\mathrm{L}$ -theorems_. The last two
schemes and their mirror images axiomatise the propositional logic Kt due to
E. J. Lemmon and known as the “minimal tense-logic” [8, p.176].

It is significant that the _Barcan formulas_

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

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 [8, p.147] or [3,
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):

$\mathbf{G}\varphi\to\mathbf{G}\mathbf{G}\varphi$ |   _transitivity_
---|---
$\mathbf{F}\varphi\land\mathbf{F}\psi\to\mathbf{F}(\varphi\land\psi)\lor\mathbf{F}(\varphi\land\mathbf{F}\psi)\lor\mathbf{F}(\mathbf{F}\varphi\land\psi)$ |   _linear future_
$\mathbf{G}\varphi\to\mathbf{F}\varphi$ |   _endless future_
$\mathbf{G}\mathbf{G}\varphi\to\mathbf{G}\varphi$ |   _density_

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 schemes together axiomatise the propositional temporal
logic of $(\mathbb{Q},<)$ [1].

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

$\Box(\mathbf{G}\varphi\to\mathbf{P}\mathbf{G}\varphi)\to(\mathbf{G}\varphi\to\mathbf{H}\varphi)\qquad\qquad\qquad\text{\emph{Dedekind
completeness}}$ (2)

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 [7].

######  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 $\SS=(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

$\displaystyle[<]X$ $\displaystyle=\\{t\in T:\forall s\in T(t<s\text{ implies
}s\in X)\\},$ $\displaystyle[>]X$ $\displaystyle=\\{t\in T:\forall s\in
T(t>s\text{ implies }s\in X)\\};$

and $U$ is a set, called the _universe_ of $\SS$. 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 $\SS$.

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

$\displaystyle\mathop{\textstyle\bigsqcap}{\cal Z}$
$\displaystyle=\mathop{\textstyle\bigcup}\\{Y\in\mathit{Prop}:Y\subseteq\mathop{\textstyle\bigcap}{\cal
Z}\\},$ $\displaystyle\mathop{\textstyle\bigsqcup}{\cal Z}$
$\displaystyle=\mathop{\textstyle\bigcap}\\{Y\in\mathit{Prop}:\mathop{\textstyle\bigcup}{\cal
Z}\subseteq Y\\}.$

We emphasise that $\mathop{\textstyle\bigsqcap}{\cal Z}$ and
$\mathop{\textstyle\bigsqcup}{\cal Z}$ are defined for arbitrary ${\cal
Z}\subseteq\wp W$. They need not be admissible, even when all members of
${\cal Z}$ are admissible. If ${\cal Z}\subseteq\mathit{Prop}$ and
$\mathop{\textstyle\bigsqcap}Z$ is admissible, then
$\mathop{\textstyle\bigsqcap}{\cal Z}$ 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 [5, §1.5].

Another perspective is that $\mathit{Prop}$ is a base for a topology on $T$
for which $\mathop{\textstyle\bigsqcap}{\cal Z}$ 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}=(\SS,|\mathord{-}|^{\mathcal{M}})$ for ${\cal L}$
based on $\SS$ is given by an interpretation function
$|\mathord{-}|^{\mathcal{M}}$ that assigns to each individual constant $\sf
c\in{\cal L}$ an element $|{\sf 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 W$. 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$.

  * •

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

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

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

The converse need not hold.

Reading off the semantics for the defined existential quantifier gives

  * $\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$

$\mathcal{M},w,f\models\exists x\varphi$ iff with
$\mathcal{M},s,f[a/x]\models\varphi$.

Consequently:

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

Again, the converse can fail.

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

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

It can also be shown [5, 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 [5, §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

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

This means that $\forall$ gets the classical semantics

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

and correspondingly, the existential quantifier gets

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

(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
$\mathop{\textstyle\bigsqcap}$ 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 [4, §§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),

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

##  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

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

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

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

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 [4,
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^{\prime}$ with $q<q^{\prime}<r$ and
$\mathcal{M},q^{\prime}\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

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

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

$|P|^{\mathcal{M}^{*}}(a_{1},\dots,a_{n})=|P\overline{a_{1}}\cdots\overline{a_{n}}|_{\mathbb{R}}.$

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

$|\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}},$

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

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

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}^{*}$, $|\forall
x\varphi|_{\mathbb{R}}=\mathop{\textstyle\bigsqcap}_{a\in
U}|\varphi(\bar{a}/x)|_{\mathbb{R}}$.

###### 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 $|\forall
x\varphi|_{\mathbb{R}}\subseteq\mathop{\textstyle\bigsqcap}_{a\in
U}|\varphi(\bar{a}/x)|_{\mathbb{R}}$.

Conversely, let $r\in\mathop{\textstyle\bigsqcap}_{a\in
U}|\varphi(\bar{a}/x)|_{\mathbb{R}}$. Then there is some $X\in\mathit{Prop}$
with $r\in X$ and

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

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

$|\varphi|^{\mathcal{M}^{*}}=|P|^{\mathcal{M}^{*}}(|\tau_{1}|^{\mathcal{M}^{*}},\dots,|\tau_{n}|^{\mathcal{M}^{*}}).$

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

$P\overline{a_{1}}\cdots\overline{a_{n}}\leftrightarrow
P\tau_{1}\cdots\tau_{n}$

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}^{*}}\neq|\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}}\neq|\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

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

For the temporal modalities we have

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

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

$\begin{array}[]{ll@{\qquad}l}|\forall
x\varphi|^{\mathcal{M}^{*}}&=\mathop{\textstyle\bigsqcap}_{a\in
U}|\varphi(\bar{a}/x)|^{\mathcal{M}^{*}}&\text{semantics of $\forall$ and
Substitution \eqref{termsub} }\\\ &=\mathop{\textstyle\bigsqcap}_{a\in
U}|\varphi(\bar{a}/x)|_{\mathbb{R}}&\text{induction hypothesis}\\\ &=|\forall
x\varphi|_{\mathbb{R}}&\text{Lemma \ref{allchar}.}\end{array}$

∎

######  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}^{\prime},q_{0},f_{0}\models\Delta$, where $\mathcal{M}^{\prime}$
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 [4, 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 [4, §2.8]. We
now analyse this further to show that the temporal logic of admissible models
over $\mathbb{Z}$ is not recursively axiomatisable.

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

Let ${\cal L}={\cal L}_{\rm 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

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

The symbols of ${\cal L}_{\rm 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
$|^{\prime}|^{\mathcal{M}}$, $|+|^{\mathcal{M}}$, $|\times|^{\mathcal{M}}$ of
the other function symbols just as ${}^{\prime},+,\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}_{\rm 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^{\prime}\land q(x^{\prime})\land\forall
z(x\prec z\land z\prec x^{\prime}\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^{\prime}\approx(x+y)^{\prime}]$

  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^{\prime}\approx(x\times
y)+x]$

These correspond to the sentences (1)–(11) in [4, p130], except for (ii) which
replaces the stronger

$\Box\exists x(e(x)\land\forall y(x\not\approx y\to\neg e(y)))$

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

$\mathcal{M},t,f\models\forall x\varphi$ implies
$\mathcal{M},t,f[a/x]\models\varphi$ for all $a\in U$, (2)

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)\neq\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,{}^{\prime},+,\times$ and forms an ${\cal L}_{\rm 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)\neq\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 ${}^{\prime},+,\times$, so
forms an ${\cal L}_{\rm 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

$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$

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\neq 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}},{}^{\prime},+,\times)$. ∎

To discuss the language of arithmetic within $\mathcal{M}$ we relativise the
quantifiers of ${\cal L}_{\rm a}$-formulas to range over $U_{q}$. A
translation is inductively defined, taking each ${\cal L}_{\rm a}$-formula
$\varphi$ to an ${\cal L}_{\rm 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}},{}^{\prime},+,\times)$. Let $\varphi$ be
any ${\cal L}_{\rm 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,{}^{\prime},+,\times$, it forms an ${\cal
L}_{\rm a}$-structure ${\cal U}_{q}$ in which any interpretation
$|\tau|^{{\cal U}_{q}}f$ of any ${\cal L}_{\rm 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

${\cal U}_{q},f\models\forall x\varphi$ iff every $a\in U_{q}$ has ${\cal
U}_{q},f[a/x]\models\varphi$ . (13)

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}_{\rm
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

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

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}_{\rm 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}_{\rm 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}_{\rm 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}_{\rm 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}_{\rm 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 [2, 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}$ [10, §5.3].

If the ${\cal L}$-sentence $\mu$ is modified by adding the sentences (12)–(15)
of [4, p131] 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 [4] 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.

As a final topic, 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,{}^{\prime},+,\times)$
to be a countable nonstandard model of arithmetic, say a proper elementary
${\cal L}_{\rm 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 [9, Section 3.1.]:
${\cal U}$ comprises a standard part, a copy of ${\cal N}$, followed linearly
by countably many pairwise disjoint copies of $(\mathbb{Z},{}^{\prime})$,
called _galaxies_. A typical galaxy looks like

$\cdots\cdots\prec^{\mathcal{M}}\bullet\prec^{\mathcal{M}}a\prec^{\mathcal{M}}a^{\prime}\prec^{\mathcal{M}}a^{\prime\prime}\prec^{\mathcal{M}}\cdots\cdots$

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 [10, 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^{\prime},t^{\prime})$ iff $(s,t)$ is strictly to the left of
$(s^{\prime},t^{\prime})$, i.e. iff $t<s^{\prime}$. We can find such a ${\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}$.

$r\text{ --------------------------- }r_{1}\cdots\cdots s_{1}\text{
--------------------------- }s$

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}$.

$r\text{ ------ }r_{21}\cdots s_{21}\text{ ------ }r_{1}\cdots\cdots
s_{1}\text{ ------ }r_{22}\cdots s_{22}\text{ ------ }s.$

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}$.

### Acknowledgment

I thank Ian Hodkinson for helpful discussions and suggestions that improved
the presentation, including extending the non-axiomatisability result for
integer time to scattered orders.

## References

  * [1] R. A. Bull.  An algebraic study of tense logics with linear time.  The Journal of Symbolic Logic, 33:27–38, 1968.
  * [2] Herbert B. Enderton.  Elements of recursion theory.  In Jon Barwise, editor, Handbook of Mathematical Logic, pages 527–566. North-Holland, 1977.
  * [3] Dov M. Gabbay.  Investigations in Modal and Tense Logics with Applications to Problems in Philosophy and Linguistics.  D. Reidel, 1976.
  * [4] Dov M. Gabbay, Ian Hodkinson, and Mark Reynolds.  Temporal Logic. Mathematical Foundations and Computational Aspects, Volume 1. Oxford University Press, 1994.
  * [5] Robert Goldblatt.  Quantifiers, Propositions and Identity: Admissible Semantics for Quantified Modal and Substructural Logics.  Number 38 in Lecture Notes in Logic. Cambridge University Press and the Association for Symbolic Logic, 2011.
  * [6] Robert Goldblatt and Edwin D. Mares.  A general semantics for quantified modal logic.  In Guido Governatori, Ian Hodkinson, and Yde Venema, editors, Advances in Modal Logic, Volume 6, pages 227–246. College Publications, 2006\.  http://www.aiml.net/volumes/volume6/.
  * [7] Leon Henkin.  A generalisation of the concept of $\omega$-completeness.  The Journal of Symbolic Logic, 22:1–14, 1957.
  * [8] Arthur N. Prior.  Past, Present and Future.  Oxford University Press, 1967.
  * [9] A. Robinson.  Non-Standard Analysis.  North-Holland, 1966.
  * [10] Joseph G. Rosenstein.  Linear Orderings.  Academic Press, 1982.


# Tuning magnetostructural phase transition in CoMn0.88Cu0.12Ge by application
of hydrostatic pressure

Aleksandra Deptuch  Institute of Nuclear Physics Polish Academy of Sciences,
Radzikowskiego 152, PL-31-342 Kraków, Poland  Ryszard Duraj  Institute of
Physics, Cracow University of Technology, Podchorążych 1, PL-30-084 Kraków,
Poland  Andrzej Szytuła  M. Smoluchowski Institute of Physics, Jagiellonian
University, prof. Stanisława Łojasiewicza 11, PL-30-348 Kraków, Poland
Bogusław Penc  M. Smoluchowski Institute of Physics, Jagiellonian University,
prof. Stanisława Łojasiewicza 11, PL-30-348 Kraków, Poland  Ewa Juszyńska-
Gałązka  Institute of Nuclear Physics Polish Academy of Sciences,
Radzikowskiego 152, PL-31-342 Kraków, Poland  Department of Chemistry,
Graduate School of Science, Osaka University, 1-1 Machikaneyama, Toyonaka,
560-0043, Osaka, Japan  Stanisław Baran<EMAIL_ADDRESS>M.
Smoluchowski Institute of Physics, Jagiellonian University, prof. Stanisława
Łojasiewicza 11, PL-30-348 Kraków, Poland

###### Abstract

Structural and magnetic properties of the CoMn0.88Cu0.12Ge compound have been
investigated using X-ray diffraction (XRD) and differential scanning
calorimetry (DSC) accompanied with investigation of magnetic properties under
applied hydrostatic pressure up to 12 kbar. It has been found that the
orthorhombic crystal structure of the TiNiSi-type, which is dominant at low
temperatures, turns into the hexagonal Ni2In-type one, slightly above 200 K.
The structural transition is of the first-order type as confirmed by presence
of distinct thermal hysteresis exceeding 20 K. The ac magnetic measurements
indicate a ferromagnetic order below the Curie temperature $T_{C}$ of 238 K,
followed by additional anomaly at lower temperatures – the latter one being
related to the structural transition. Application of hydrostatic pressure
leads to temperature separation of the purely magnetic transition, whose Curie
temperature $T_{C}$ slowly increases with applied pressure, and the
magnetostructural transition characterized by critical temperature showing
much rapid decrease with increasing pressure. Comparison of the DSC data for
the investigated compound and the isostructural CoMn0.95Cu0.05Ge one has made
it possible to determine both the structural and magnetic components of
entropy change.

keywords: intermetallic compounds, X-ray diffraction (XRD), ferromagnetic
materials, magnetic properties, pressure-temperature phase diagram

##  I Introduction

Magnetostructural coupling in the MM’Ge compounds, where M and M’ are
transition 3d elements, has been extensively investigated in recent years. The
coupling is strictly related to the structural phase transition between the
low-temperature orthorhombic martensite (M) phase and the high-temperature
hexagonal austenite (A) one. Stoichiometric CoMnGe has an orthorhombic crystal
structure of the TiNiSi-type (space group $Pnma$) at room temperature. The
structure undergoes a martensite structural transformation into the high-
temperature hexagonal Ni2In-type structure (space group $P6_{3}/mmc$) around
$T_{s}\approx 500$ K. The compound shows also a second order magnetic
transition from para- to ferromagnetic state at the Curie temperature
$T_{C}\approx 350$ K [1, 2, 3]. Doping of substitutional and/or interstitial
atoms as well as introducing metal vacancies leads to gradual reduction of the
difference between $T_{s}$ and $T_{C}$, finally resulting in appearance of a
magnetostructural phase transition where both the structural and magnetic
transitions occur at the same temperature. This magnetostructural transition
is accompanied with large magnetocaloric effect [4, 5].

Especially interesting are compounds with the Mn atoms partially substituted
by the Cu atoms, as the neutron diffraction studies indicate that the Mn
sublattice is a dominant source of magnetism in this class of materials [6,
7]. Until now, the X-ray diffraction data at room temperature as well as the
calorimetric and magnetic properties in function of temperature for the
CoMn1-xCuxGe system with $x=0-0.15$ [2, 3] and $x=0.08-0.1$ [8] have been
reported. On the basis of these data, the structural and magnetic $(T,x)$
phase diagram has been determined (see Fig. 6b in Ref. [2] and Fig. 5 in Ref.
[3]). The temperature of the structural phase transition between the high-
temperature hexagonal phase and the low-temperature orthorhombic one has been
reported to decrease with increasing Cu content $x$ from about 500 K for $x=0$
down to about 100 K for $x=0.15$, while the Curie temperature decreases from
about 350 K for $x=0$ down to about 250 K for $x=0.15$ [2, 3]. The X-ray
diffraction data, collected at room temperature, show dominant contribution
arising from the orthorhombic structure for $x=0.08$, while the hexagonal
structure being dominant for $x>0.08$ [8]. A giant magnetocaloric effect has
been reported for the Cu concentration range where the first-order
magnetostructural transition occurs, i.e. the temperatures of the structural
and magnetic transitions coincide. According to Refs. [2, 3], the
magnetostructural coupling has been found for $0.09\leq x\leq 0.11$, while
partial coupling has been reported for $x=0.12$. Ref. [8] reports
magnetostructural coupling even for $x=0.08$ and 0.085. Magnetic entropy
change, under magnetic flux change of 0-5 T, has been reported to reach around
50 J$\cdot$kg${}^{-1}\cdot$K-1 for $x=0.11$ [2, 3] or for $x=0.08$ and 0.085
[8].

In order to better understand the complex magnetostructural properties of the
CoMn1-xCuxGe system, in this work we report the results of X-ray diffraction
(XRD) and differential scanning calorimetry (DSC) measurements accompanied
with investigation of magnetic properties under applied hydrostatic pressure
up to 12 kbar, as performed for CoMn0.88Cu0.12Ge, i.e. the composition showing
partial magnetostructural coupling, according to the $(T,x)$ phase diagram
presented in Refs. [2, 3]. On the basis of our data, the $(p,T)$ phase diagram
has been determined. In addition, the comparison of the DSC data for the
investigated compound and the isostructural CoMn0.95Cu0.05Ge one has made it
possible to determine both the structural and magnetic components of entropy
change.

##  II Experimental details and results

###  II.1 Sample synthesis

Polycrystalline sample of CoMn0.88Cu0.12Ge has been obtained by arc melting of
the constituent elements (purity better than 99.9 wt. %) under argon
atmosphere, followed by annealing in vacuum ($\sim$$10^{-3}$ mbar) for 5 days
at 1123 K (850 ∘C) and subsequent furnace cooling down to room temperature.

###  II.2 Crystal structure

Figure 1:  XRD patterns of CoMn0.88Cu0.12Ge: (a) Reprezentative patterns
collected at different temperatures on heating. (b) Pattern collected at 100 K
with the results of Rietveld refinement (background subtracted). The first and
second row of vertical bars indicates the peak positions originating from the
orthorhombic phase (88.8(9) wt. %) and hexagonal one (11.2(8) wt. %),
respectively. (c) Pattern collected at 300 K with the results of Rietveld
refinement (background subtracted). The vertical bars indicate the peak
positions from the hexagonal phase.

Thermal evolution of the powder X-ray diffraction pattern for CoMn0.88Cu0.12Ge
clearly indicates a temperature-induced structural transition – see Fig. 1a.
In purpose to determine the exact crystal structures, a Rietveld refinement of
the X-ray diffraction data has been performed using the FullProf software [9].
Figs. 1b and 1c show the XRD patterns collected at 100 and 300 K,
respectively, together with the results of the Rietveld refinement. The
experimental data indicate that CoMn0.88Cu0.12Ge at 100 K (Fig. 1b) is a
mixture of two crystal phases, namely, the orthorhombic one (88.8 wt. %) of
the TiNiSi-type (space group $Pnma$, No. 62) in which each element occupy the
$4c$ site $(x,\frac{1}{4},z)$ with different values of the $x$ and $z$
parameters, and the hexagonal phase (11.2 wt. %) of the Ni2In-type (space
group $P6_{3}/mmc$, No. 194) with the Co atoms occupying the $2d$ site
$(\frac{1}{3},\frac{2}{3},\frac{3}{4})$, while the Mn and Cu atoms occupying
the same $2a$ site $(0,0,0)$ and the Ge atoms located in the $2c$ site
$(\frac{1}{3},\frac{2}{3},\frac{1}{4})$. CoMn0.88Cu0.12Ge at 300 K (see Fig.
1c) is single-phase, consisting of the hexagonal phase solely.

Figure 2:  Phase fraction (weight percentage), unit cell volume and lattice
constants vs. temperature for CoMn0.88Cu0.12Ge. Unit cell parameters of the
hexagonal phase have been recalculated to those of the orthorhombic phase
using the following relations: $a_{o}=c_{h}$, $b_{o}=a_{h}$,
$c_{o}=\sqrt{3}a_{h}$ and $V_{o}=2V_{h}$.

Figure 2 shows thermal evolution of: fractions of the orthorhombic and
hexagonal phases, lattice parameters $a$, $b$ and $c$ as well as unit cell
volume $V$, as determined from X-ray powder diffraction. The orthorhombic
phase, which is dominant at low temperatures, undergoes an inverse martensitic
transition to the hexagonal phase at 219 K, while the high-temperature
hexagonal phase transforms into the orthorhombic one on cooling (martensitic
transition) at 193 K. The transition temperatures have been defined as
inflection points in the phase fraction vs. temperature curves. A comparison
of the lattice parameters characterizing the orthorhombic and hexagonal phases
can be done considering the relationships: $a_{o}=c_{h}$, $b_{o}=a_{h}$,
$c_{o}=\sqrt{3}a_{h}$ and $V_{o}=2V_{h}$. A first order character of the
structural transition is confirmed by a large volume contraction $\frac{\Delta
V}{V}=3.7$ %, step change of selected lattice parameters, namely,
$\frac{\Delta a}{a_{o}}=10.2$ % and $\frac{\Delta b}{b_{o}}=7.2$ % as well as
thermal hysteresis visible in the phase fraction vs. temperature curves.

Table 1:  Lattice parameters $a$, $b$ and $c$ and the unit cell volume $V$ of the orthorhombic and hexagonal phases together with the phase fraction of the hexagonal phase, as determined from the X-ray diffraction data collected at 100, 300 and 480 K. T [K] |  $a_{o}$ [Å] |  $b_{o}$ [Å] |  $c_{o}$ [Å] |  $V_{o}$ [Å3] |  $a_{h}$ [Å] |  $c_{h}$ [Å] |  $V_{h}$ [Å3] | hex [%]
---|---|---|---|---|---|---|---|---
100 | 5.876(2) | 3.8104(8) | 7.066(2) | 158.22(7) | 4.075(1) | 5.291(4) | 76.10(6) | 11.2(8)
300 | - | - | - | - | 4.0889(4) | 5.3158(5) | 76.97(2) | 100
480 | - | - | - | - | 4.0976(4) | 5.3472(6) | 77.75(2) | 100

The values of refined lattice parameters and the unit cell volumes at 100, 300
and 480 K are listed in Table 1. The data presented in Fig. 2 and Table 1
indicate almost linear thermal expansion of lattice parameters of the
hexagonal phase.

###  II.3 Thermal properties

Figure 3:  DSC thermograms of (a) CoMn0.88Cu0.12Ge and (b) CoMn0.95Cu0.05Ge at
cooling and subsequent heating with the rate of 10 K/min. The $T_{s}$ and
$T_{f}$ symbols refer respectively to the start and finish of the structural
transition during cooling and heating. In (a), the characteristic temperatures
of transitions from austenite to martensite ($T_{A-M}$) and from martensite to
austenite ($T_{M-A}$) are defined as the peak positions. In (b), $T_{C}$
denotes the Curie temperature, while the small anomalies at 160 and 260 K
correspond to the magnetic transitions in the impurity hexagonal phase which
is observed for the samples with large Cu content (the XRD analysis of the
sample indicates about 9.6 wt. % of the impurity phase).

Differential scanning calorimetry (DSC) measurements were carried in the
temperature range 100-350 K with the temperature rate of 10 K/min in DSC 2500
(TA Instruments) calorimeter. The results of the DSC measurements are shown in
Fig. 3a.

Table 2:  Enthalpy ($\Delta H$) and total entropy ($\Delta S$) changes associated with the structural phase transition in CoMn1-xCuxGe, $x$ = 0.05 and 0.12, as determined from the DSC data collected during heating and cooling. | $\Delta H$ | $\Delta H$ | $\Delta S$ | $\Delta S$
---|---|---|---|---
compound | [J/g] | [kJ/mol] |  [J/(kg$\cdot$K)] |  [J/(mol$\cdot$K)]
$x$ = 0.05, cooling | 1.79 | 0.34 | 5.83 | 1.09
$x$ = 0.05, heating | 1.79 | 0.34 | 5.72 | 1.07
$x$ = 0.12, cooling | 4.97 | 0.93 | 23.7 | 4.44
$x$ = 0.12, heating | 5.95 | 1.12 | 25.5 | 4.79

A difference between the peak temperatures obtanined during heating and
cooling is marked by vertical dashed lines in Fig. 3a. A noticeable thermal
hysteresis of 21 K indicates first order character of the structural phase
transition. Determined values of the enthalpy ($\Delta H$) and total entropy
($\Delta S$) changes are given in Table 2.

###  II.4 Magnetic properties

High pressure magnetic measurements were carried out in the temperature range
80-400 K under fully hydrostatic conditions. Helium was used as a pressure-
transmitting medium. The pressure cell (made of beryllium bronze) was
connected to the UNIPRESS GCA-10 three stage gas compressor by a manganin
gauge placed in the highest pressure stage of the compressor. Temperature was
controlled by a temperature controller equipped with a thermocouple placed
directly at the sample position. The ac magnetic susceptibility measurements
were carried out in a weak magnetic field of 1 mT (10 Oe) amplitude and
frequency of 300 Hz. The voltage induced in the pick-up coils was measured by
a lock-in amplifier.

Figure 4:  (a) Temperature dependence of the ac magnetic susceptibility of
CoMn0.88Cu0.12Ge at selected hydrostatic pressures up to 12 kbar. (b)
Magnetostructural $(p,T)$ phase diagram of CoMn0.88Cu0.12Ge. $T_{C}$ and
$T_{s}$ denote the Curie and structural phase transitions, respectively, while
(h) and (c) indices refer to heating and cooling. The error bars are smaller
than the plot symbols.

Fig. 4a shows temperature dependence of the ac magnetic susceptibility $\chi$
for CoMn0.88Cu0.12Ge during heating and cooling within the temperature range
80-360 K and selected hydrostatic pressures up to 12 kbar. At ambient
pressure, a sharp increase of ac magnetic susceptibility with deacreasing
temperature, characteristic of transition from para- to ferromagnetic state,
is visible at $T_{C}=238$ K. The Curie temperature has been defined as an
inflection point in the $\chi(T)$ curve. A slow increase of $T_{C}$ with
increasing pressure is observed.

A distinct thermal hysteresis in the $\chi(T)$ curves is noticeable below the
respective Curie points. An anomaly, defined as a second inflection point in
the $\chi(T)$ curve, can be attributed to the magnetostructural transition
associated with the (inverse) martensitic transition in CoMn0.88Cu0.12Ge. The
temperature of anomaly ($T_{s}$) decreases with increasing pressure and shows
thermal hysteresis of almost 20 K.

On the basis of the collected ac magnetic measurements, the magnetostructural
pressure-temperature $(p,T)$ phase diagram has been determined (see Fig. 4b).
The Curie temperature is found to increase slowly with increasing pressure
($\textrm{d}T_{C}/\textrm{d}p=0.7(1)$ K/kbar). The characteristic temperature
of the magnetostructural transition is lower than the Curie one, and decreases
with increasing pressure with much higher rate
($\textrm{d}T_{s}/\textrm{d}p=-10.4(5)$ K/kbar). The first order character of
the latter transition is confirmed by presence of distinct thermal hysteresis
of $T_{s}$.

##  III Discussion

The X-ray powder diffraction data show that the low-temperature orthorhombic
crystal structure (TiNiSi-type) of CoMn0.88Cu0.12Ge undergoes an (inverse)
martensitic transition into the hexagonal one (Ni2In-type) with increasing
temperature. Distinct jumps in the unit cell volume $V$ as well as the lattice
parameters $a$ and $b$ (see Fig. 2) are characteristic of the first order-type
transition. The first order of the structural transition is confimed by
thermal hysteresis found in both the DSC (Fig. 3a) and ac magnetic data (Fig.
4a). The magnetic data, taken at ambient pressure, reveal that further
increase od temperature leads to another phase transition from the low-
temperature ferromagnetic state to the high-temperature paramagnetic one.
Proximity of two transition temperatures leads to partial coupling of the
structural and magnetic transitions at ambient pressure.

The pressure-temperature $(p,T)$ phase diagram, determined on the basis of the
ac magnetic measurements under hydrostatic pressures up to 12 kbar (see Fig.
4b), shows that increasing pressure breaks the partial coupling of the
structural and magnetic transitions, as the Curie temperature increases slowly
with increasing pressure ($\textrm{d}T_{C}/\textrm{d}p=0.7(1)$ K/kbar) while
the temperature of the second transition (having magnetostructural character)
decreases with increasing pressure with much higher rate
($\textrm{d}T_{s}/\textrm{d}p=-10.4(5)$ K/kbar). A similar effect can be
obtained by applying a chemical pressure – compare with the $(T,x)$ phase
diagram (Fig. 6b in Ref. [2] and Fig. 5 in Ref. [3]), where $x$ denotes the
copper content in CoMn1-xCuxGe. The chemical pressure increases with
increasing copper content as the copper radius ($r_{Cu}\approx 1.28$ Å) is
smaller than that of manganese ($r_{Mn}\approx 1.30$ Å) [10].

Total entropy change $\Delta S_{T}$, associated with a magnetostructural
transition, is a sum of the magnetic entropy change $\Delta S_{m}$ and entropy
difference $\Delta S_{s}$ between two different crystallographic polymorphs,
i.e. $\Delta S_{T}=\Delta S_{m}+\Delta S_{s}$ [11]. In order to determine
individual components of the sum for CoMn0.88Cu0.12Ge, additional DSC
measurements have been performed for the isostructural CoMn0.95Cu0.05Ge, where
purely magnetic transition occurs for the low-temperature orthorhombic phase,
as the temperature of structural transition is found to be around 100 K higher
(Fig. 6b in Ref. [2] and Fig. 5 in Ref. [3]). The DSC curves, collected for
CoMn0.95Cu0.05Ge, show broad peaks at 308 K for heating and 303 K for cooling
(see Fig. 3b). The corresponding magnetic entropy changes equal 5.7
J$\cdot$kg${}^{-1}\cdot$K-1 for heating and 5.8 J$\cdot$kg${}^{-1}\cdot$K-1
for cooling, respectively. The magnetic entropy change is not sensitive to
small changes in chemical composition as the value for stoichiometric CoMnGe
has been reported to equal 5.8 J$\cdot$kg${}^{-1}\cdot$K-1 under magnetic flux
change of 0-5 T [12]. Assuming the same value of magnetic entropy change (i.e.
5.8 J$\cdot$kg${}^{-1}\cdot$K-1) for CoMn0.88Cu0.12Ge and the average total
entropy change of 24.6 J$\cdot$kg${}^{-1}\cdot$K-1 (see Tab. 2) leads to the
estimated value of the structural component of around 19
J$\cdot$kg${}^{-1}\cdot$K-1. Therefore, the structural component plays the
dominant role in the total entropy change associated with the
magnetostructural transition in CoMn0.88Cu0.12Ge.

##  IV Conclusions

The current work reports the results of a systematic investigation of
structural and magnetic phase transitions in CoMn0.88Cu0.12Ge by complementary
experimental techniques including X-ray diffraction (XRD) and differential
scanning calorimetry (DSC) accompanied with investigation of magnetic
properties under applied hydrostatic pressure up to 12 kbar. The compound
shows at ambient pressure a partial coupling of the structural martensitic
transition and the magnetic transition between the ferro- and paramagnetic
states. Increasing pressure breaks the partial coupling of the structural and
magnetic transitions, as the Curie temperature increases slowly with
increasing pressure while the temperature of the second transition (having
magnetostructural character) decreases with increasing pressure with much
higher rate. Comparison of the DSC data for CoMn0.88Cu0.12Ge and
CoMn0.95Cu0.05Ge reveals that the structural component dominates over the
magnetic one in the total entropy change associated with the magnetostructural
transition in CoMn0.88Cu0.12Ge.

## Acknowledgements

The research was partially carried out with the equipment purchased thanks to
the financial support of the European Regional Development Fund in the
framework of the Polish Innovation Economy Operational Program [contract no.
POIG.02.01.00-12-023/08] and the European Regional Development Fund
Operational Program Infrastructure and Environment [contract no. POIS
13.01.00-00-062/08].

## References

  * Johnson [1975] V. Johnson,  Diffusionless orthorhombic to hexagonal transitions in ternary silicides and germanides,  Inorganic Chemistry 14 (1975) 1117–1120. 10.1021/ic50147a032.
  * Pal et al. [2019] S. Pal, C. Frommen, S. Kumar, B. Hauback, H. Fjellvåg, T. Woodcock, K. Nielsch, G. Helgesen,  Comparative phase transformation and magnetocaloric effect study of Co and Mn substitution by Cu in MnCoGe compounds,  Journal of Alloys and Compounds 775 (2019) 22–29. 10.1016/j.jallcom.2018.10.040.
  * Pal et al. [2020] S. Pal, C. Frommen, S. Kumar, B. Hauback, H. Fjellvåg, G. Helgesen,  Enhancing giant magnetocaloric effect near room temperature by inducing magnetostructural coupling in Cu-doped MnCoGe,  Materials & Design 195 (2020) 109036. 10.1016/j.matdes.2020.109036.
  * Hamer et al. [2009] J. Hamer, R. Daou, S. Özcan, N. Mathur, D. Fray, K. Sandeman,  Phase diagram and magnetocaloric effect of CoMnGe1-xSnx alloys,  Journal of Magnetism and Magnetic Materials 321 (2009) 3535–3540. 10.1016/j.jmmm.2008.03.003, current Perspectives: Magnetocaloric Materials.
  * Trung et al. [2010] N. T. Trung, V. Biharie, L. Zhang, L. Caron, K. H. J. Buschow, E. Brück,  From single- to double-first-order magnetic phase transition in magnetocaloric Mn1-xCrxCoGe compounds,  Applied Physics Letters 96 (2010) 162507. 10.1063/1.3399774.
  * Nizioł et al. [1982] S. Nizioł, A. Bombik, W. Bażela, A. Szytuła, D. Fruchart,  Crystal and magnetic structure of CoxNi1-xMnGe system,  Journal of Magnetism and Magnetic Materials 27 (1982) 281–292. 10.1016/0304-8853(82)90087-7.
  * Szytuła et al. [1981] A. Szytuła, A. Pędziwiatr, Z. Tomkowicz, W. Bażela,  Crystal and magnetic structure of CoMnGe, CoFeGe, FeMnGe and NiFeGe,  Journal of Magnetism and Magnetic Materials 25 (1981) 176–186. 10.1016/0304-8853(81)90116-5.
  * Samanta et al. [2012] T. Samanta, I. Dubenko, A. Quetz, S. Stadler, N. Ali,  Giant magnetocaloric effects near room temperature in Mn1-xCuxCoGe,  Applied Physics Letters 101 (2012) 242405. 10.1063/1.4770379.
  * Rodríguez-Carvajal [1993] J. Rodríguez-Carvajal,  Recent advances in magnetic structure determination by neutron powder diffraction,  Physica B: Condensed Matter 192 (1993) 55–69. 10.1016/0921-4526(93)90108-I.
  * Pearson [1972] W. Pearson, The Crystal Chemistry and Physics of Metals and Alloys, Wiley-Interscience, New York, 1972.
  * Gschneidner Jr. et al. [2012] K. Gschneidner Jr., Y. Mudryk, V. Pecharsky,  On the nature of the magnetocaloric effect of the first-order magnetostructural transition,  Scripta Materialia 67 (2012) 572–577. 10.1016/j.scriptamat.2011.12.042, viewpoint Set No. 51: Magnetic Materials for Energy.
  * Lai et al. [2014] J. Lai, Z. Zheng, R. Montemayor, X. Zhong, Z. Liu, D. Zeng,  Magnetic phase transitions and magnetocaloric effect of MnCoGe1-xSix,  Journal of Magnetism and Magnetic Materials 372 (2014) 86–90. 10.1016/j.jmmm.2014.07.035.