# Spectroscopic Confirmation of Two Luminous Post-AGB Stars in the Globular
Cluster M19

Howard E. Bond Department of Astronomy & Astrophysics, Pennsylvania State
University, University Park, PA 16802, USA  Space Telescope Science Institute,
3700 San Martin Drive, Baltimore, MD 21218, USA  Visiting Astronomer, Cerro
Tololo Inter-American Observatory, National Optical Astronomy Observatory,
operated by the Association of Universities for Research in Astronomy under a
cooperative agreement with the National Science Foundation.  Jacob E. Jencson
Steward Observatory, University of Arizona, 933 N Cherry Ave., Tucson, AZ
85721-0065, USA  Robin Ciardullo Department of Astronomy & Astrophysics,
Pennsylvania State University, University Park, PA 16802, USA  Institute for
Gravitation and the Cosmos, Pennsylvania State University, University Park, PA
16802, USA  Brian D. Davis Department of Astronomy & Astrophysics,
Pennsylvania State University, University Park, PA 16802, USA  Michael H.
Siegel Department of Astronomy & Astrophysics, Pennsylvania State University,
University Park, PA 16802, USA

###### Abstract

The visually brightest stars in globular clusters (GCs) are the ones evolving
off the asymptotic giant branch (AGB) and passing through spectral types F and
A—the “yellow” post-AGB (yPAGB) stars. yPAGB stars are potentially excellent
“Population II” standard candles for measuring extragalactic distances. A
recent survey of the Galactic GC system, using uBVI photometry to identify
stars of low surface gravities with large Balmer discontinuities, discovered a
candidate luminous yPAGB star in the GC M19 (NGC 6273), designated ZNG 4. The
same survey also identified a bright, hotter candidate blue PAGB star, ZNG 2,
lying near the top of the white-dwarf cooling sequence. Both PAGB candidates
have proper motions and parallaxes in the recent Gaia Early Data Release 3
consistent with cluster membership, but they still lacked spectroscopic
verification. Here we present moderate-resolution spectra of both stars,
confirming them as low-gravity objects that are extremely likely to be cluster
members. Through comparison with a library of synthetic spectra, we made
approximate estimates of the stars’ atmospheric parameters. We find that the
yPAGB star ZNG 4 has an effective temperature of $T_{\rm eff}\simeq 6500$ K, a
surface gravity of $\log g\simeq 1$, and a metallicity of
$\rm[Fe/H]\simeq-1.5$, similar to that of the host cluster. The blue PAGB star
ZNG 2 has $T_{\rm eff}\simeq 18000$ K, $\log g\simeq 3$, and an apparently low
metallicity in the range of $\rm[Fe/H]\simeq-2.0$ to $-2.5$. Both stars are
bright ($V=12.5$ and 13.3, respectively). We urge high-dispersion
spectroscopic follow-up to determine detailed atmospheric parameters and
chemical compositions, and to monitor radial velocities.

††facilities: Bok 2.3m; CTIO 0.9m, 1.5m

##  1 Two Bright Post-AGB Candidates in M19

The most luminous objects in globular clusters (GCs) and other old stellar
populations are stars that are in their final evolution from the top of the
asymptotic giant branch (AGB) toward higher temperatures in the Hertzsprung-
Russell diagram—the post-AGB (PAGB) stars. Evolving at nearly constant
bolometric luminosity, PAGB stars attain their brightest visual magnitudes as
they pass through spectral types F and A, where the bolometric correction is
smallest. These luminous and non-variable “yellow” PAGB (yPAGB) stars have
been proposed as potentially useful Population II standard candles for
measuring extragalactic distances, based on their expected narrow luminosity
function in old populations, and ease of detection because of their large
Balmer discontinuities (Bond, 1997a, b; Ciardullo et al., 2022).

Due to the rapid evolutionary timescales of yPAGB stars, they are very rare
objects. In a recent paper, Davis et al. (2022, hereafter D22) described their
search of nearly the entire population of Galactic GCs for yPAGB stars, and
other evolved stars lying above the horizontal branch (HB) in the clusters’
color-magnitude diagrams (CMDs). The D22 survey was based on photometry in the
uBVI system, which is optimized for detection of low-surface-gravity A-, F-,
and G-type stars with large Balmer jumps (Bond 2005; D22), combined with
verification of cluster membership using astrometry from the recent Gaia Early
Data Release 3 (EDR3; Gaia Collaboration et al. 2021). As summarized by D22,
only ten yPAGB stars are known in the Milky Way GC system, of which five are
blueward of the Cepheid/RV Tauri instability strip and are thus non-variable.

As PAGB objects evolve to still higher temperatures, they become “blue” PAGB
(bPAGB) stars, potentially ionizing surrounding ejecta and becoming central
stars of planetary nebulae. A recent review of bPAGB objects and other hot
stars in GCs (Moehler et al., 2019) lists about two dozen luminous bPAGB stars
known in Galactic GCs. These stars then begin their descent of white-dwarf
cooling tracks, at first fading rapidly to lower luminosities, and then
cooling more slowly.

One of the results of the D22 survey was their discovery of a luminous yPAGB
star, and a bright bPAGB star, in the Galactic GC M19 (NGC 6273). These two
stars were discussed in more detail by Bond et al. (2021, hereafter B21). The
yPAGB and bPAGB stars in M19 had been cataloged five decades ago as candidate
“UV-bright” stars by Zinn et al. (1972, hereafter ZNG), respectively
designated M19 ZNG 4 and M19 ZNG 2. However, the uBVI study by B21 and D22 was
the first to show that both objects have large Balmer jumps, consistent with
the low surface gravities of luminous stars. This property distinguishes them
from foreground stars, which are a substantial contaminant of the ZNG UV-
bright catalog (see Bond, 2021). Table 1 in B21 lists the coordinates,
photometry, and other parameters of these two stars; that paper also presents
a finding chart.

Both of M19’s PAGB stars have Gaia EDR3 proper motions and parallaxes that are
consistent with cluster membership. But, without spectroscopic confirmation of
their natures, they remained PAGB “candidates,” albeit very strong ones. In
this paper, we discuss the evolutionary status of ZNG 4 and ZNG 2, and we then
present spectroscopy of both stars, which strongly confirms them as luminous
PAGB stars. This makes them worthy of further and more detailed study.

##  2 Evolutionary Status

Figure 2 presents the CMD [visual absolute magnitude, $M_{V}$, versus
dereddened color, $(B-V)_{0}$] for a nearly complete catalog of bright members
of M19. These data are from D22, and were obtained with CCD cameras on the
0.9- and 1.5-m telescopes at Cerro Tololo Inter-American Observatory. Field
interloper stars—which are numerous at M19’s low Galactic latitude of
$b=+9\fdg 4$—have been removed from the CMD based on EDR3 proper motions and
parallaxes. We have retained only stars with membership probabilities greater
than 0.8, as described in D22. The $BV$ data have been corrected for a mean
cluster reddening of $E(B-V)=0.37$ (Johnson et al., 2017), and we have assumed
$R_{V}=3.1$. M19 suffers from considerable differential extinction, which
accounts for the broadening of the red-giant branch and HB in its CMD. For the
two PAGB stars themselves, plotted in Figure 2 as large filled circles, we
obtained their reddenings from the detailed extinction maps of M19 given by
Alonso-García et al. (2012) and Johnson et al. (2017): $E(B-V)=0.344$ and
0.342 for ZNG 4 and ZNG 2, respectively. For the cluster distance, we adopt
8340 pc [$(m-M)_{0}=14.61$] from the recent compilation of Galactic GC
distances assembled by Baumgardt & Vasiliev (2021), which is based on Gaia
parallaxes and other sources. This gives the stars visual absolute magnitudes
of $M_{V}=-3.16$ and $-2.38$, respectively, with uncertainties of about
$\pm$0.09 mag.

Color-magnitude diagram for bright members of M19, based on data from Davis et
al. (2022), and converted to visual absolute magnitude and dereddened $B-V$
color, as described in the text and using parameters given in the figure
legend. Filled gray circles are stars with high cluster membership
probabilities based on Gaia proper motions and parallaxes, as described by
Davis et al. (2022). The two large filled circles mark the post-AGB stars ZNG
2 and ZNG 4. Small filled green circles plot the five known variable stars.
Superposed are theoretical post-horizontal-branch evolutionary tracks from
Moehler et al. (2019), for a metallicity of $\rm[M/H]=-1.5$, and for the three
zero-age-horizontal-branch masses indicated in the labels. The tracks have
been converted to the observational quantities as described in the text. Time
steps are marked on the tracks with the symbols given in the legend.

Superposed on the CMD in Figure 2 are three theoretical post-HB evolutionary
tracks computed by Moehler et al. (2019).111We thank Marcelo Miller Bertolami
for sending us tables of these tracks with a finer time resolution than given
in the Moehler et al. paper. As described in more detail in D22, we have
edited and smoothed these tracks to remove several rapid excursions due to
thermal pulses. We then converted the tracks from the theoretical quantities
of luminosity and effective temperature to $M_{V}$ and $B-V$, using the online
PARSEC YBC web tool222http://stev.oapd.inaf.it/YBC/ (Chen et al., 2019). These
tracks are for a metal content of $\rm[M/H]=-1.5$. This is the nearest
metallicity value in the Moehler et al. track library to that of M19. Harris
(2010) gives $\rm[Fe/H]=-1.74$ in his compilation of GC properties,333The
Harris compilation of GC properties, 2010 December version, is available
online at http://physwww.mcmaster.ca/~harris/mwgc.dat while a spectroscopic
study (Johnson et al., 2017) of over 300 red giants and AGB stars in the
cluster revealed a range of iron contents among the members, from about
$\rm[Fe/H]=-2$ to $-1$, but concentrated around $-1.75$ and $-1.5$. Symbols
along the tracks mark time steps of 10, 1, and 0.01 Myr, as indicated in the
figure legend.

The HB in M19 is extremely blue, containing virtually no stars redder than
$(B-V)_{0}\simeq 0.15$. Filled green circles in Figure 2 mark the D22
photometry of the five known variable stars in M19, which consist of only one
RR Lyrae variable, and four Type II Cepheids.444As explained in D22, the data
were obtained at a small number of epochs, and thus do not represent the mean
locations of the variables in the CMD. The three Moehler et al. tracks that
are plotted are for masses on the zero-age HB (ZAHB) of 0.55, 0.60, and
$0.65\,M_{\odot}$. These values encompass the range of ZAHB masses seen in
this cluster.

The yPAGB star ZNG 4 lies close to the track for a ZAHB mass of
$0.55\,M_{\odot}$. This is consistent with the finding discussed by D22 that
all of the known yPAGB stars in Galactic GCs belong to clusters with blue
horizontal branches. The explanation proposed by D22 is that this arises from
the relatively slow evolutionary timescales on the PAGB for stars with low
ZAHB masses. In this picture, stars with higher ZAHB masses do produce PAGB
stars, but they evolve across the CMD extremely rapidly—as illustrated by the
time marks on the tracks in Figure 2—and are thus so transient that none of
them are present in the GC population.

The ZAHB mass of progenitor of the bPAGB star ZNG 2 star is less certain,
since the tracks at its location in the CMD are so close together. However,
its ZAHB mass is statistically likely to be low, again because of the much
more rapid evolutionary timescales for the more massive stars. In fact, it is
remarkable that the two PAGB stars in M19 have nearly the same bolometric
luminosity (see Table 1 in B21); their locations in the CMD are consistent
with them both lying on nearly the same evolutionary track.

##  3 Spectroscopic Observations and Reductions

Optical spectra of ZNG 4 and ZNG 2 were obtained on 2021 May 9 with the Boller
& Chivens spectrograph mounted on the 2.3-m Bok Telescope at the Steward
Observatory station on Kitt Peak. A 1200 line mm-1 grating was used in first
order with a $1\farcs 5$ slit, providing a wavelength coverage of 3520–4650 Å
at a 2.5-pixel resolution of 2.5 Å. Exposure times were $3\times 600$ s for
ZNG 4 and $3\times 300$ s for ZNG 2. HeArNe comparison-lamp spectra were
obtained at the positions of both stars for wavelength calibration. M19 lies
at a declination of $-26^{\circ}$, and the mean airmasses for the exposures
were 2.0 and 2.3, respectively. The slit was oriented east-west, which
unfortunately is roughly perpendicular to the parallactic angle.

We performed bias-subtraction, flat-fielding, and cosmic-ray removal on the
CCD frames, using standard tasks in IRAF.555IRAF was distributed by the
National Optical Astronomy Observatories, operated by AURA, Inc., under
cooperative agreement with the National Science Foundation. We then extracted
the spectra from the CCD images, wavelength-calibrated them, and finally
normalized them to a flat continuum, again employing standard IRAF tools.
There is clear evidence of wavelength-dependent losses of flux due to
atmospheric refraction, a consequence of the high airmasses and an east-west
slit; therefore we did not attempt to flux-calibrate the spectra, nor measure
radial velocities.

##  4 Atmospheric Parameters

Here we compare the spectra of the two PAGB stars with the extensive library
of synthetic spectra computed by Allende Prieto et al. (2018, hereafter AP18),
and available online from the Strasbourg Astronomical Data
Center.666http://cdsarc.u-strasbg.fr/viz-bin/qcat?J/A+A/618/A25 These
theoretical spectra are tabulated with a wavelength spacing of $\sim$0.13 Å,
and have a resolution of $\sim$0.4 Å. For the purpose of comparison with our
observations, we smoothed the synthetic spectra to a resolution of 2.5 Å,
using the boxcar task in IRAF.

###  4.1 Yellow PAGB Star ZNG 4

The spectrum of ZNG 4 is plotted as a black curve in Figure 4.1. The uBVI
photometry (B21, D22) shows that ZNG 4 has an extremely large Balmer
discontinuity (B21 give a color of $u-B=1.47$), indicating a very low surface
gravity. However, the normalization to a flat continuum, as shown in the
figure, largely suppresses its depth when there is only a small amount of
wavelength coverage below the jump. The spectrum of ZNG 4 is clearly that of a
very low-surface-gravity star, as indicated by its narrow and deep Balmer
lines, and the relatively strong lines of ionized species such as Fe II, Sr
II, and Ba II, a few of which are marked in the figure.

Observed and model-atmosphere spectra for the yellow PAGB star M19 ZNG 4,
normalized to flat continua. Lines of several species are marked. Black curve:
observed spectrum of ZNG 4. Note the sharp and deep Balmer absorption lines
and relatively strong lines of Fe II, Sr II, and Ba II, indicative of a very
low surface gravity. Blue curve: synthetic spectrum of a star with $T_{\rm
eff}=6500$ K, $\log g=1.0$, and $\rm[Fe/H]=-1.5$, shifted upward by 0.8 times
the continuum level. It gives a good match to the observed spectrum.

To estimate the atmospheric parameters of the star, we compared its spectrum
with a sequence of theoretical spectra from AP18 with a metallicity of
$\rm[Fe/H]=-1.5$, surface gravity of $\log g=1.0$ (near the gravity
anticipated from the star’s location in the CMD), and effective temperatures
with a spacing of 500 K. The closest match in this grid to the observed
spectrum is for $T_{\rm eff}=6500$ K, placing it blueward of the instability
strip. The smoothed synthetic spectrum for this temperature is plotted as the
blue curve in Figure 4.1. It provides a good match to the observed spectrum.
(We also compared the spectrum to the grid at metallicity $\rm[Fe/H]=-2.0$,
but the higher metal content gave a better fit to the metallic-line spectrum,
as shown in the figure.)

A number of yellow PAGB stars in the field (e.g., Bond, 1991; Oomen et al.,
2019, and references therein), as well as the yPAGB star in the GC M79 (Şahin
& Lambert, 2009), show photospheric depletions of refractory heavy elements.
These depletions, which can be extreme (e.g., Takeda et al., 2002; Rao et al.,
2012), are generally attributed to condensation onto grains which are then
lost from the atmosphere. Yet ZNG 4 does not appear to be significantly more
metal-poor than its host cluster, based on our modest-resolution spectrum. A
high-dispersion abundance analysis of ZNG 4 would be of considerable interest,
as would a radial-velocity study to search for binarity.

###  4.2 Blue PAGB Star ZNG 2

In Figure 4.2 the spectrum of ZNG 2 is shown as a black curve. As in the case
of ZNG 4, the normalization to a flat continuum has reduced the apparent depth
of its Balmer discontinuity, which is actually large (B21 give a color of
$u-B=0.61$). Numerous lines of He I are present, indicative of a fairly high
temperature.

Observed and model-atmosphere spectra for the blue PAGB star M19 ZNG 2,
normalized to flat continua. Lines of several species are marked. Black curve:
observed spectrum of ZNG 2. Note the sharp and deep Balmer absorption lines,
indicative of a low surface gravity. Blue curve: synthetic spectrum of a star
with $T_{\rm eff}=18000$ K, $\log g=3.0$, and $\rm[Fe/H]=-2.0$, shifted upward
by 0.8 times the continuum level. It gives a fairly good match to the observed
spectrum, although the lines of Mg II and Si II in ZNG 2 are slightly weaker
than in the synthetic spectrum. The Ca II lines in ZNG 2 are likely mostly
interstellar.

As in the case of the yPAGB star, we compared this spectrum with spectra from
the AP18 grid, assuming a surface gravity of $\log g=3.0$ (once again near the
anticipated gravity). Spectra for $\rm[Fe/H]=-1.5$ gave metal lines
consistently stronger than in ZNG 2, so we adopted $\rm[Fe/H]=-2.0$. We then
examined theoretical spectra to find the best fit to the overall strengths of
the He I lines, which proved to be for $T_{\rm eff}=18,000$ K (the grid
spacing is 2000 K at this temperature). This synthetic spectrum, smoothed to
2.5 Å resolution, is plotted as the blue curve in Figure 4.2. It gives a
fairly good match to the observed spectrum, although lines of Mg II and Si II
are weaker in the star than in the model, and a few of the He I lines are not
well matched. (Conversely, the Ca II K line is stronger in the star than in
the model, but it is likely to have a strong interstellar component, given the
relatively large reddening.) However, adopting models with $\rm[Fe/H]=-2.5$
would give lines of Mg II and Si II weaker than in the star, so the star’s
metallicity is likely in the range $-2.5<\rm[Fe/H]<-2.0$. There is thus some
suggestion that ZNG 2 is more metal-deficient than the red giants in M19,
raising the possibility that depletion onto grains has occurred—but this
suggestion needs to be confirmed with a high-dispersion abundance analysis.

##  5 Conclusions

We have obtained moderate-resolution spectra of the two candidate luminous
PAGB stars in the Galactic GC M19 discovered by B21. We estimated the
atmospheric parameters of the two stars through comparison with a grid of
model-atmosphere synthetic spectra.

The effective temperatures. low surface gravities, and low metallicities that
we find are fully consistent with both stars being members of the cluster. Now
that the cluster memberships of these very luminous and extremely rare stars
appear to be firmly established, we urge high-dispersion spectroscopic studies
of the their detailed chemical compositions, along with radial-velocity
monitoring.

We thank Paul Smith for conducting the spectcroscopic observations presented
in this work, and Nathan Smith for donating observing time. This research has
made use of the VizieR catalogue access tool, CDS, Strasbourg, France (DOI:
10.26093/cds/vizier). The original description of the VizieR service was
published in 2000, A&AS 143, 23. The Institute for Gravitation and the Cosmos
is supported by the Eberly College of Science and the Office of the Senior
Vice President for Research at The Pennsylvania State University.

## References

  * (1)
  * Allende Prieto et al. (2018) Allende Prieto, C., Koesterke, L., Hubeny, I., et al. 2018, A&A, 618, A25 (AP18)
  * Alonso-García et al. (2012) Alonso-García, J., Mateo, M., Sen, B., et al. 2012, AJ, 143, 70
  * Baumgardt & Vasiliev (2021) Baumgardt, H. & Vasiliev, E. 2021, MNRAS, 505, 5957
  * Bond (1991) Bond, H. E. 1991, in IAU Symp. 145, Evolution of Stars: the Photospheric Abundance Connection, ed. G. Michaud & A. Tutukov (Dordrecht: Kluwer), 341
  * Bond (1997a) Bond, H. E. 1997a, in IAU Symp. 180, Planetary Nebulae, ed. H. J. Habing & H. J. G. L. M. Lamers (Dordrecht: Kluwer), 460
  * Bond (1997b) Bond, H. E. 1997b, in The Extragalactic Distance Scale, ed. M. Livio, M. Donahue, & N. Panagia (Cambridge: Cambridge Univ. Press), 224
  * Bond (2005) Bond, H. E. 2005, AJ, 129, 2914
  * Bond (2021) Bond, H. E. 2021, AJ, 161, 204
  * Bond et al. (2021) Bond, H. E., Davis, B. D., Siegel, M. H., et al. 2021, AJ, 161, 125 (B21)
  * Chen et al. (2019) Chen, Y., Girardi, L., Fu, X., et al. 2019, A&A, 632, A105
  * Ciardullo et al. (2022) Ciardullo, R., Bond, H. E., Davis, B. D., et al. 2022, arXiv:2204.06084
  * Davis et al. (2022) Davis, B. D., Bond, H. E., Siegel, M. H., et al. 2022, ApJ, 926, 99 (D22)
  * Gaia Collaboration et al. (2021) Gaia Collaboration, Brown, A. G. A., Vallenari, A., et al. 2021, A&A, 649, A1
  * Harris (2010) Harris, W. E. 2010, arXiv:1012.3224
  * Johnson et al. (2017) Johnson, C. I., Caldwell, N., Rich, R. M., et al. 2017, ApJ, 836, 168
  * Moehler et al. (2019) Moehler, S., Landsman, W. B., Lanz, T., et al. 2019, A&A, 627, A34
  * Oomen et al. (2019) Oomen, G.-M., Van Winckel, H., Pols, O., et al. 2019, A&A, 629, A49
  * Rao et al. (2012) Rao, S. S., Giridhar, S., & Lambert, D. L. 2012, MNRAS, 419, 1254
  * Şahin & Lambert (2009) Şahin, T., & Lambert, D. L. 2009, MNRAS, 398, 1730
  * Takeda et al. (2002) Takeda, Y., Parthasarathy, M., Aoki, W., et al. 2002, PASJ, 54, 765
  * Zinn et al. (1972) Zinn, R. J., Newell, E. B., & Gibson, J. B. 1972, A&A, 18, 390 (ZNG)


First-order logic fragments mixing quantifiers, arithmetic, and uninterpreted predicates are often undecidable, as is, for instance, Presburger arithmetic extended with a single uninterpreted unary predicate.  In the SMT world, difference logic is a quite popular fragment of linear arithmetic which is less expressive than Presburger arithmetic.  Difference logic on integers with uninterpreted unary predicates is known to be decidable, even in the presence of quantifiers.  We here show that (quantified) difference logic on real numbers with a single uninterpreted unary predicate is undecidable, quite surprisingly. Moreover, we prove that difference logic on integers, together with order on reals, combined with uninterpreted unary predicates, remains decidable.

§ INTRODUCTION

The success of satisfiability modulo theories (SMT) solvers in verification can be attributed to several things, but one of them is indisputably the omnipresence, in the combination of theories, of arithmetic reasoners.  As SMT solvers get stronger in quantified reasoning, it becomes more interesting to get a clear picture of decidability frontiers when arithmetic is used in a quantified SMT context.  Some pure arithmetic theories are already undecidable, even in their quantifier-free fragment, e.g., Peano arithmetic [11], i.e., a first-order theory of the natural numbers with addition and multiplication.  However, Presburger arithmetic, somehow the linear restriction of Peano arithmetic, is decidable even in the quantified case [9], but augmenting Presburger arithmetic with a single unary uninterpreted predicate already yields undecidability [6, 10, 18].  To obtain a decidable fragment mixing arithmetic and uninterpreted predicates, one must further restrict the expressiveness.

In the SMT world, difference logic used to be a popular fragment of arithmetic,
because of its low complexity in the quantifier-free case.  In this fragment,
arithmetic is limited to difference constraints of the form $x - y \bowtie c$
where $x$ and $y$ are variables, $c$ is an integer constant and $\bowtie$
belongs to $\{<, \leq, =, \geq, >\}$.  Difference constraints can, e.g., express conditions on
the distance between two variables, the atomic formula $x - y = 2$ stating that
the distance between the values of $x$ and $y$ must be exactly $2$.  Notice that
since difference constraints involve only two variables ($c$ is an integer
constant) those constraints are strictly less expressive than linear
constraints in Presburger arithmetic.  The decidability of the logic mixing
difference constraints and unary uninterpreted predicates, when interpreted over
$\mathbb{N}$ (or similarly $\mathbb{Z}$) reduces to the decidability of the
monadic second-order theory of one successor, usually referred to as S1S.  The
decidability of S1S has been established thanks to the concept of infinite-word
automaton [3].

On the real domain, it is well known that the first-order theory of real-closed
fields, which is in a sense the real counterpart of Peano arithmetic, is
decidable [19] even in the presence of quantifiers.  Whereas this
might give the impression that decidability is more often obtained on the reals
than on the integers, we here prove that the logic mixing difference constraints
and unary uninterpreted predicates, when interpreted over $\mathbb{R}$, is

Further restricting the arithmetic language, and considering order on the real
domain only, it is known that the monadic second-order theory of order is
undecidable [8, 16], but its universal
fragment is decidable [4]. In this work, we establish that
the fragment mixing unary uninterpreted predicates, difference constraints over
integer variables, and order constraints over real variables is decidable.

Section <ref> provides some prerequisites and the precise definition of the studied fragments.  In Section <ref>, we prove the decidability of the fragment mixing unary uninterpreted predicates, difference constraints over integer variables, and order constraints over real variables.  This was already the subject of a work-in-progress workshop paper [1].  In Section <ref>, we prove that the fragment of quantified difference constraints over real variables extended with a single unary uninterpreted predicate is undecidable.

§ PRELIMINARIES

We refer to e.g., [7] for a general
introduction to first-order logic with equality, and assume that the
reader is familiar with the notions of signature, term, variable, and
formula.  We use the usual logical connectives ($\lor$, $\land$,
$\lnot$, $\Rightarrow$, $\Leftrightarrow$) and first-order quantification
$\exists x.\, \varphi$ and $\forall x.\, \varphi$, respectively equivalent to writing $\exists x\, (\varphi)$ and $\forall x\, (\varphi)$, i.e., the dot stands for an opening parenthesis that is closed at the end of the formula.
Variable symbols are denoted by $x$, $y$, $z$, … and are meant to be interpreted as real numbers.

Our signature contains the interpreted arithmetic symbols $0$, $1$, $+$, $-$, $<$,
$\leq$, $\geq$, $>$, $=$, and other constants in $\mathbb{N}$ that stand for terms $1 + 1 +
\cdots + 1$.  We furthermore use a monadic (i.e., unary) interpreted predicate $x \in\mathbb{Z}$ to
denote that $x$ has an integer value.  The signature also contains
uninterpreted predicate symbols $P$, $Q$, … In the whole article, we only
consider unary predicate symbols. Indeed, including binary uninterpreted predicates without restriction on first-order quantification directly yields undecidability. Our language is the set of all well-formed
formulas, in the usual sense, built using symbols from the signature.  Further specific restrictions will be introduced later.

An interpretation specifies a domain (i.e., a set of elements), assigns a value
in the domain to each free variable, and assigns relations of appropriate arity
on the domain to predicate symbols in the signature.  Throughout the article,
the interpretation domain is always $\mathbb{R}$.  The arithmetic symbols $0$,
$1$, $+$, $-$, $<$, $\leq$, $\geq$, $>$, $=$ are interpreted as expected on
$\mathbb{R}$, and $x\in\mathbb{Z}$ is true if and only if $x$ has an integer
value[In the current context, this choice of notation for mixed
integer-real arithmetic is simpler than using a multi-sorted logic.].  An
interpretation assigns an arbitrary subset of the domain $\mathbb{R}$ to each
unary predicate.  By extension, an interpretation assigns a value in
$\mathbb{R}$ to every term, and a truth value to every formula. We denote the
interpretation $I$ of a variable $x$ by $I[x]$, and the interpretation of a
predicate $P$ by $I[P]$. A model of a formula is an interpretation that assigns
true to this formula.  A formula is satisfiable on a domain (here $\mathbb{R}$)
if it has a model on that domain.

§.§ Difference Arithmetic with Unary Predicates

We consider several fragments where the language is
restricted, in particular in the way that the arithmetic relations can be used.  A fragment is
decidable if there exists a procedure to check whether a given formula in
this fragment is satisfiable.

In the various fragments introduced below, all arithmetic atoms are either
order constraints of the form $x\!\bowtie\!y$, or difference
constraints of the form $x - y \bowtie c$, where $x$ and $y$ are variables,
$c$ is a constant in $\mathbb{Z}$, and $\bowtie \ \in \{<, \leq, =, \geq, >\}$.
As a reminder, the language of our formulas only contains unary	predicates.
The only atoms besides the arithmetic ones are of the form
$P(x)$ where $P$ is an uninterpreted predicate symbol and $x$ is a variable, and
$x \in \mathbb{Z}$ where $x$ is a variable.
Note that the addition of constraints of the form $x \bowtie c$, where $x$ is a variable and $c$ is an integer constant, to fragments that already admit difference constraints does not increase their expressive power: a constraint $x \bowtie c$ is equivalent to the difference constraint $x-v_0 \bowtie c$, where $v_0$ is a particular variable intended to be interpreted as zero.

It is worth mentioning that the models of the formulas in our fragments are invariant by an integer shift, i.e., mapping every real $x$ to the real $x + j$, where $j$ is an integer.
Conjunctions of order constraints will be merged to improve readability, i.e., we will often write $x<y<z$ rather than $x<y \land y<z$.
Finally, we use the shorthand $P(x+c)$ instead of $\exists y.\, y - x = c \land P(y)$, where $x$ is a free variable and $c\in \mathbb{Z}$.

We now introduce our fragments of interest. Their names are inspired from the SMT-LIB nomenclature, where acronyms stand for the theories that appear in the combinations:

* : the theory of uninterpreted functions, with the restriction that uninterpreted symbols may only correspond to monadic predicates;

* : the theory of order on the reals only;

* : the theory of order on the reals and integers;

* : difference logic on the integers;

* : difference logic on the reals.

The fragment is the fragment with unary uninterpreted predicates and
order constraints between variables interpreted over $\mathbb{R}$.
Difference logic constraints and atoms of the form $x\in\mathbb{Z}$ are not

The formula	$\forall x\,\exists\,y,z\,.\, y<x<z \land \forall t\,.\, (y<t<z \land P(t) ) \Rightarrow t= x$ describes a predicate $P$ that is true only on isolated real numbers.

The fragment is the extension of where atoms of the form
$x\in\mathbb{Z}$ are allowed.  This fragment can express order relations between
real and integer variables.

The formula $\forall x, y.\, (x<y \land x \in \mathbb{Z} \land y \in \mathbb{Z}) \Rightarrow \exists v.\, x<v<y \land P(v)$ describes a predicate $P$ that is true for at least one value located between any two integers.

The fragment is an extension of the fragment (and therefore of
). It is also interpreted over $\mathbb{R}$.  Order constraints between
variables and atoms of the form $x\in\mathbb{Z}$ are allowed. Additionally,
difference logic constraints are allowed, but they can only involve integer-guarded variables.

In order to enforce this integer-guard restriction on difference logic
constraints, formulas must be well-guarded, i.e.,
difference logic constraints can only appear in the two following contexts:

* $x \in \mathbb{Z} \land y \in \mathbb{Z} \land x - y \bowtie c$,

* $(x \in \mathbb{Z} \land y \in \mathbb{Z}) \Rightarrow x - y \bowtie c$,

where $x$ and $y$ are variables, $c \in \mathbb{Z}$ is a constant, and $\bowtie \ \in \{<, \leq, =, \geq, >\}$.

The following formula describes a predicate that is either true on all odd numbers and false on all even numbers, or the opposite, as well as true on all non-integer numbers:

$\mbox{\hspace{20pt}} \big[ \forall x,y.\, \big(x \in \mathbb{Z} \land y \in \mathbb{Z} \land y-x=2 \big) \Rightarrow \big( P(x) \Leftrightarrow P(y)\big) \big]\\
\mbox{\hspace{20pt}} \land \big[\exists x,y.\, x \in \mathbb{Z} \land y \in \mathbb{Z} \land P(x) \land \lnot P(y)\big] \land \big[\forall z.\, \lnot(z \in \mathbb{Z}) \Rightarrow P(z)\big]$

The fragment is the fragment interpreted over $\mathbb{R}$, where order
constraints, difference logic constraints and unary predicate atoms are allowed
without any restriction. The use of atoms of the form $x\in\mathbb{Z}$ is
forbidden. Since order constraints are a special case of difference logic constraints, the name of the fragment only refers to and not .

The formula $\forall x\, \exists y.\, 0 < y-x < 3 \land P(y)$ describes a predicate $P$ such that any subinterval of $\mathbb{R}$ of length greater or equal to $3$ contains a value for which $P$ is true.

Note: It might appear to the reader that a missing logic in this nomenclature is , with difference logic constraints on both real and integer variables.  We will later show that is already undecidable, so it makes little sense to introduce any extension of it.

§ DECIDABILITY OF

The fragment is actually a restriction of the universal fragment of the monadic second-order theory of the real order $\mathbb{R}$, i.e., augmented with universal quantification of predicate variables. It has been established in [4] that the universal fragment of the monadic second-order theory of the real order $\mathbb{R}$ is decidable, which trivially implies the decidability of . We show here that its extension (and therefore ) is also decidable, by a reduction to .

and are decidable.

Note that the decidability of is a direct consequence of the decidability of , since is an extension of .
The remaining of this section is thus dedicated to proving that is decidable.

§.§ Recognizing Integer Values

We first show how to define in a predicate $\pz$ over $\mathbb{R}$ that is  to $\mathbb{Z}$, i.e., such that there exists a bijection between the sets described by $\pz$ and $\mathbb{Z}$ that preserves the order relation over their elements.  Integer guards in will later be translated using $\pz$.  Intuitively, an integer-guarded variable in a formula will correspond to a variable taking its value in the set described by $\pz$ in the translated formula.

We axiomatize $\pz$ in as follows:

$\bullet$ Every element of $\pz$ is isolated:

$\forall x\, \exists\, y,z.\ y < x < z \land \forall t.\ [y < t < z \land \pz(t)] \Rightarrow t = x $.

$\bullet$ Every point in $\mathbb{R}$ has a unique successor in $\pz$:

$\forall x\, \exists\, y.\ x < y \land \pz(y) \land \forall t.\ x < t < y \Rightarrow \neg \pz(t)$.

$\bullet$ Similarly, every point in $\mathbb{R}$ has a unique predecessor in $\pz$:

$\forall x\, \exists\, y.\ y < x \land \pz(y) \land \forall t.\ y < t < x \Rightarrow \neg \pz(t)$.

The set of all integers is a model for $\pz$, therefore the above axiomatization is consistent.
The set of elements satisfying $\pz$ is necessarily infinite and does not admit a maximal or a minimal element. This is a direct consequence of the successor and predecessor axioms.
More interestingly, this set is also necessarily countable. Indeed, since each point is isolated, there exists an application that maps the elements satisfying $\pz$ to disjoint open intervals. Any set of disjoint intervals in $\mathbb{R}$ with non-zero length is necessarily countable [17], since each of them contains a rational value that does not belong to the others.

It is now possible to define a successor relation on the real numbers satisfying $\pz$ with the formula  $\textit{Succ}(x,y) \! = \! \pz(x) \land \pz(y) \land y \! < \! x \land \forall z.\, y \! < \! z \! < \! x \Rightarrow \lnot \pz(z)$, i.e., $x$ is the successor of $y$, or equivalently, $y$ is the predecessor of $x$.

The axiomatization of $\pz$ is, in fact, precise enough to have the following lemma.

For any model $M$ of $\pz$, the set $M[\pz]$ is $<$-isomorphic to $\mathbb{Z}$.

For convenience in the proof, we define $0_{\textit{int}}$ as an arbitrary existentially quantified value that belongs to the set described by $\pz$.

Given a model $M$ of the axiomatization of $\pz$, we need to define a bijection between the set $M[\pz]$ and $\mathbb{Z}$ that preserves order.

Let us define an application $f$ from $M[\pz]$ to $\mathbb{Z}$.  We set $f(0_{\textit{int}}) = 0$, and then define recursively:

* $f(y) = f(x) + 1$ for each $x,y \in M[\pz]$ such that $y > 0_{\textit{int}}$ and $\textit{Succ}(y,x)$,

* $f(y) = f(x) - 1$ for each $x,y \in M[\pz]$ such that $y < 0_{\textit{int}}$ and $\textit{Succ}(x,y)$.

Thanks to the fact that every element of $M[\pz]$ has a unique predecessor and successor, it
follows that $f$ ranges over the whole set $\mathbb{Z}$, proving that $f$ is surjective. Since it is clear that
$f$ preserves order, it follows that $f$ is strictly increasing, and therefore injective.  It remains to show that $f$ is well defined for every
element in $M[\pz]$.

If there exists some element $y \in M[\pz]$ for which $f$ is not
defined, it means that $f$ is not well-defined, in the sense that there exists either an element
$y > 0_{\textit{int}}$ such that the interval $[0_{\textit{int}},y]$ contains an infinite number of elements
satisfying $\pz$, or there exists an element $y < 0_{\textit{int}}$ such that the interval
$[y,0_{\textit{int}}]$ contains an infinite number of elements satisfying $\pz$.  Since both cases are
symmetric, we only address the former.  There must exist a strictly increasing
infinite series of elements in $M[\pz]$ bounded by $y$.  Let us
consider its limit $z\in \mathbb{R}$.  Because there must exist an element of
$M[\pz]$ smaller than $z$ and arbitrarily close to $z$, it follows that $z$ cannot have a predecessor, which contradicts an axiom.  Therefore $f$ is well-defined, and
every element of $M[\pz]$ is associated to an integer number. The application $f$ is therefore a bijection.

§.§ Translating Formulas

We are now able to describe the satisfiability-preserving translation of
formulas from to .  Consider a formula $\varphi$.  Without
loss of generality, we assume that $\pz$ does not appear in $\varphi$.  The
translation of $\varphi$ is defined as

$$\textit{AXIOMS}_{int}(\pz) \land \llbracket\varphi\rrbracket$$

where $\textit{AXIOMS}_{int}(\pz)$ is the conjunction of the axioms of $\pz$, and $\llbracket \cdot \rrbracket$ is a translation operator. This translation operator $\llbracket \cdot \rrbracket$ distributes over all Boolean operators and quantifiers, and corresponds to the identity transformation for most considered atoms, except in the following cases:

* $\llbracket x \in \mathbb{Z} \rrbracket = \pz(x)$;

* $\llbracket x - y \bowtie c \rrbracket = \exists z_0,\dots z_c\,.\  (y = z_0) \land (x \bowtie z_c) \land \bigwedge_{0 \leq i < c} \textit{Succ}(z_{i+1}, z_i)$,
for $c \in \mathbb{N}$ and $\bowtie \ \in \{<, \leq, =, \geq, >\}$. We assume that $z_0, \dots z_c$ are fresh variables w.r.t. $x$ and $y$.

$\llbracket x - y \leq 2 \rrbracket = \exists z_0, z_1, z_2.\ y = z_0 \land \textit{Succ}(z_1, z_0) \land \textit{Succ}(z_2, z_1) \land x \leq z_2$.

Notice that we only deal with the case $c \! \in \! \mathbb{N}$ since every atom of the form $x - y \bowtie c$ with $c \in \mathbb{Z} \setminus \mathbb{N}$ and $\bowtie \ \in \{<, \leq, =, \geq, >\}$ can be rewritten as $y - x \bowtie^\prime -c$ with the following correspondences: $(\bowtie, \bowtie') \in \{{(=, =)}, {(<, >)}, {(>, <)}, {(\geq, \leq)}, {(\leq, \geq)}\}$.

§.§ Establishing Equisatisfiability

Given a formula $\varphi$, the translation that we have introduced generates a corresponding formula $\psi$. To establish that they are equisatisfiable, we need to prove that if $\varphi$ admits a model, then $\psi$ also admits one, and reciprocally.

Given a formula $\varphi$, consider its translation into $\psi = \textit{AXIOMS}_{int}(\pz) \land \llbracket\varphi\rrbracket$. The formulas $\varphi$ and $\psi$ are equisatisfiable.

If $\varphi$ is satisfiable, let $M$ be one of its models. Then, since $\psi$ shares the same free variables and predicates than $\varphi$ with the only addition of $\pz$, we can directly construct a model $M'$ of $\psi$ that is similar to $M$ for the shared variables and predicates, and that interprets $\pz$ so that $\pz(x)$ holds whenever $x \in \mathbb{Z}$. This is always possible since the only constraints on $\pz$ generated by the construction of $\psi$ are the axioms stated above.

If $\psi$ is satisfiable, then there exists a model $M$ of $\psi$. Let us construct a model $M'$ of $\varphi$. Let $0_\textit{int} \in \mathbb{R}$ be an arbitrary element of $M[\pz]$. We define an automorphism $g$ of $\mathbb{R}$, such that $g(0_\textit{int}) = 0$, and recursively $g(y) = g(x) + 1$ for $x,y \in M[\pz]$, $y>0_\textit{int}$ and $\textit{Succ}(y,x)$, and $g(y) = g(x) - 1$ for $x,y \in M[\pz]$, $y<0_\textit{int}$ and $\textit{Succ}(x,y)$. The automorphism $g$ maps each open interval between the $k$-th and  successors (resp. predecessors) of $0_\textit{int}$ in $M[\pz]$, onto the open interval $(k, k+1)$ (resp. $(-(k\!+\!1), -k)$) while preserving order.

$M'$ is defined by $M'[x] = g(M[x])$ for each free variable $x$ of the formula $\varphi$, and $M'[P] = \{g(x) \, | \, x \in M[P]\}$ for each uninterpreted predicate $P$ of $\varphi$. No unary predicate atom can be violated by $M'$ by definition. Furthermore, no order constraint can be violated by $M'$ either since $g$ preserves order. Regarding the difference logic constraints, the intermediate variables $z_i$ introduced in the translation are necessarily mapped to values in $M[\pz]$ since the Succ relation enforces this property. Hence for each such variable, we have $g(M[z_i]) \in \mathbb{Z}$. Intuitively, this ensures that in $M'$ the difference between the values taken by the integer variables is consistent with the difference logic constraints.
It follows that $M'$ is a model of $\varphi$.

§ UNDECIDABILITY OF

The result presented in the previous section establishes a lower bound for the decidability of our family of fragments.  A natural follow-up problem is to establish a corresponding upper bound, i.e., to find an extension of this logic that yields undecidability.  We show here that, when combined with uninterpreted unary predicates, as soon as difference logic constraints on reals are allowed, the logic becomes undecidable.

We actually show a stronger result which is that a single unary predicate symbol is enough to yield undecidability. More precisely, we establish the undecidability of the restriction of where only one predicate symbol is allowed, by reducing the halting problem of a Turing machine to the satisfiability problem over this restriction of .

Satisfiability is undecidable for with a single predicate.

Satisfiability is undecidable for .

The remaining of this section is dedicated to proving Theorem <ref>. We consider w.l.o.g. Turing machines defined over an alphabet with only two symbols and no explicit blank symbol [15]. This choice leads to a simpler proof.

§.§ Definitions

The proof is by reduction from the halting problem for a Turing machine with a single bi-infinite tape,
starting from a blank tape (i.e., a tape filled with the symbol $0$).  Consider a Turing machine
${\cal M} = (Q, \Sigma, q_I, q_F, \Delta)$, where

* $Q$ is a finite nonempty set of states,

* $\Sigma$ is the alphabet $\{ 0, 1 \}$,

* $q_I \in Q$ is the initial state,

* $q_F \in Q$ is the halting state,

* $\Delta \subseteq \{(Q \setminus \{ q_F\}) \times \Sigma
\times Q \times \Sigma \times \{L, R\} \}$
is the transition relation, assumed to be total over its first two components, i.e., for any pair $(q, \alpha) \in (Q \setminus \{ q_F\}) \times \Sigma$, there exists a tuple $(q, \alpha, q', \alpha', \lambda) \in \Delta$.

A configuration $C$ of such a Turing machine is a triplet containing the current state $q$, the content of the tape $t \in \{0,1\}^\mathbb{Z}$ and the position of the head $h \in \mathbb{Z}$.
Since the machine starts from a blank tape, the initial configuration is $C_0 = (q_I, 0^\mathbb{Z}, 0)$.

A run $\rho$ of length $n \in \mathbb{N}$ (resp. $n = + \infty$) of such a Turing machine is a finite (resp. infinite) sequence of configurations $(C_i)_{i \in [0,n]}$ (resp. $(C_i)_{i \in \mathbb{N}}$), such that for any two consecutive configurations $C_i = (q_i, t_i, h_i)$ and $C_{i+1} = (q_{i+1}, t_{i+1}, h_{i+1})$ there exists a transition $(q, \alpha, q', \alpha', \lambda) \in \Delta$ such that:

* $q=q_i$ and $q' = q_{i+1}$,

* $t_i[h_i] = \alpha$, i.e., the tape cell at position $h_i$ contains the symbol $\alpha$,

* $t_{i+1}[h_i] = \alpha'$,

* $t_{i+1}[k] = t_i[k]$, for every $k\in \mathbb{Z}$,  $k \neq h_i$,

* $h_{i+1} = h_i + 1$ if $\lambda = R$, and $h_{i+1} = h_i - 1$ if $\lambda = L$.

A halting run is a finite run such that the state of its last configuration is the halting state $q_F$.

§.§ Encoding Runs

Our goal is to encode a run of a Turing machine (as described before), i.e., encode the state, the tape content, and the position of the head for each configuration of such a run.
Starting from the initial configuration, we must also ensure the coherence of the run w.r.t. the Turing machine transition relation, by connecting every two consecutive configurations.
Our idea is to define an infinite sequence of intervals on the real line, such that each interval contains the encoding of its corresponding configuration (i.e., the first interval will contain the first configuration of the run, and so on). Difference constraints can then be used to connect consecutive configurations.

Let $N = \lceil\log_2 (|Q|) \rceil$. Each state $q \in Q$ of $\mathcal{M}$ can therefore be uniquely encoded with $N$ Boolean values $b^q_1, \dots b^q_N$.
We want to encode consecutive configurations of the Turing machine using a single predicate $P$ over $\mathbb{R}$. In order to do so, we first need to describe a subset of $\mathbb{R}$ that will act as a grid supporting the encoding of the state, the tape content, and the head position of the current configuration.

We use the concept of linear ordering [14] to describe the shape of the grid. A linear ordering $J$ is a totally ordered set, i.e., a set equipped with a binary relation $<$ which is irreflexive (for all $j$ in $J$,  $j\not<j$), asymmetric (for all $j,k$ in $J$, if $j<k$, then $k\not<j$), transitive (for all $i,j,k$ in $J$, if $i<j$ and $j<k$, then $i<k$), and complete (for all $j,k \in J$, either $j = k$, $j<k$, or $k<j$). The order type of a linear ordering $J$ is the class of all linear orderings $<$-isomorphic to $J$.
The order types of a singleton, the set composed of the $N$ first natural numbers, $\mathbb{N}$, and $\mathbb{Z}$ are respectively denoted by $1$, $N$, $\omega$, and $\zeta$.
The concatenation of two linear orderings $J$ and $K$ (where their associated order relations are respectively $<_J$ and $<_K$) is denoted by $J + K$. It corresponds to the linear ordering composed of the set of pairs $\{(j, 1) \,|\, j \in J\} \cup \{(k, 2)\,|\, k \in K\}$, and equipped with the order relation $<$, defined by $(j_1, 1) < (j_2, 1)$ if $j_1 <_J j_2$, $(k_1, 2) < (k_2, 2)$ if $k_1 <_K k_2$, and $(j, 1)<(k, 2)$ for every $j\in J$ and $k\in K$.
More generally, given two linear orderings $J$ and $K$, the linear ordering $(J)^K$ is the set of pairs $(j, k)$ with $j \in J$ and $k \in K$, with the order relation $<$ such that $(j_1, k_1) < (j_2, k_2)$ if either $k_1 <_K k_2$, or $k_1 =_K k_2$ and $j_1 <_J j_2$. These operators are naturally extended on order types. For instance, the order type $(\omega)^\omega$ is the class of all linear orderings $<$-isomorphic to $\mathbb{N}^2$.

The grid we consider is a linear ordering that is a subset of $\mathbb{R}$, of order type $\big(N + \zeta + 1 + \zeta \big)^{\omega}$. An ordering of order type $N + \zeta + 1 + \zeta$ within the interval $[0,3)$ is depicted in Figure <ref>. Each dot corresponds to a natural number and each vertical line corresponds to an element of the linear ordering. The first $N$ points will support the encoding of a state. The first subordering that is  to $\mathbb{Z}$ (i.e., of order type $\zeta$) will be used to encode the position of the head, while the second one will support the encoding of the tape content. The whole grid is composed of an infinite repetition of the subordering $N + \zeta + 1 + \zeta$ (i.e., it is repeated on the intervals $[3k,3k+3)$ for all $k \in \mathbb{N}$), hence the $\omega$ exponent.

[scale=.9,node distance=2cm]
[use as bounding box] (-1, 4.6) rectangle (8.5, 7);
[] at (0,4.4) $0$;
[] at (2,4.4) $1$;
[] at (4,4.4) $2$;
[] at (6,4.4) $3$;

[] at (8,4.4) $\dots$;

[thick] (0,5.2) – (0,4.8);
[thick] (2,5.2) – (2,4.8);
[thick] (4,5.2) – (4,4.8);

[circle, fill, scale=.5] at (0,5) ;
[circle, fill, scale=.5] at (2,5) ;
[circle, fill, scale=.5] at (4,5) ;
[circle, fill, scale=.5] at (6,5) ;

(3,5.2) – (3,4.8);
(3.1,5.15) – (3.1,4.85);
(2.9,5.15) – (2.9,4.85);
(3.2,5.15) – (3.2,4.85);
(2.8,5.15) – (2.8,4.85);
(3.3,5.12) – (3.3,4.88);
(2.7,5.12) – (2.7,4.88);
(3.4,5.1) – (3.4,4.9);
(2.6,5.1) – (2.6,4.9);
(3.5,5.1) – (3.5,4.9);
(2.5,5.1) – (2.5,4.9);
(3.6,5.1) – (3.6,4.9);
(2.4,5.1) – (2.4,4.9);
(3.7,5.08) – (3.7,4.92);
(2.3,5.08) – (2.3,4.92);

(0.2,5.15) – (0.2,4.85);
(0.4,5.15) – (0.4,4.85);
(0.6,5.15) – (0.6,4.85);
(0.8,5.15) – (0.8,4.85);
[dotted] (1, 4.9) – (1.6, 4.9);
(1.8,5.15) – (1.8,4.85);

[thick] [decorate, decoration = calligraphic brace] (-0.15,5.3) – (2.05,5.3);
[] at (1,5.6) $N$;

(5,5.2) – (5,4.8);
(5.1,5.15) – (5.1,4.85);
(4.9,5.15) – (4.9,4.85);
(5.2,5.15) – (5.2,4.85);
(4.8,5.15) – (4.8,4.85);
(5.3,5.12) – (5.3,4.88);
(4.7,5.12) – (4.7,4.88);
(5.4,5.1) – (5.4,4.9);
(4.6,5.1) – (4.6,4.9);
(5.5,5.1) – (5.5,4.9);
(4.5,5.1) – (4.5,4.9);
(5.6,5.1) – (5.6,4.9);
(4.4,5.1) – (4.4,4.9);
(5.7,5.08) – (5.7,4.92);
(4.3,5.08) – (4.3,4.92);

[thick] (-1, 5) – (7.5,5);
[dotted] (7.5,5) – (8.5,5);

[ultra thick] [decorate, decoration = calligraphic brace] (-0.15,5.9) – (2.06,5.9);
[] at (1,6.25) $\textit{State}$;

[ultra thick] [decorate, decoration = calligraphic brace] (2.15,5.9) – (3.85,5.9);
[] at (3,6.25) $\textit{Head}$;

[ultra thick] [decorate, decoration = calligraphic brace] (4.15,5.9) – (5.85,5.9);
[] at (5,6.25) $\textit{Tape}$;

[ultra thick] [decorate, decoration = calligraphic brace] (-0.15,6.6) – (5.85,6.6);
[] at (2.85,6.95) $\textit{Complete encoding of one configuration}$;

[dotted] (-0.15, 6.6) – (-0.15, 5);
[dotted] (5.85, 6.6) – (5.85, 5);

A visual representation of a linear ordering of order type $N + \zeta + 1 + \zeta$.

§.§ Defining the Support of the Encoding

Let us first define concretely the support of the encoding of the Turing machine configurations.
The difficulty lies in describing the grid using a single predicate $P$, without meddling with the actual encoding of the configurations afterwards. Our solution is to characterize the points that belong to the grid by enforcing that such a point is surrounded by an open interval where $P$ is uniformly true on the left, and by an open interval where $P$ is uniformly false on the right, such as depicted in Figure <ref>. We do not specify yet how $P$ behaves on $x$, as this is how the configurations will actually be encoded later.

[use as bounding box] (3, 5) rectangle (7, 5.3);
[] (3,4.85) rectangle ++(2,0.3);
[] (5,4.85) rectangle ++(2,0.3);
at (4, 5.4) $P$;
at (6, 5.4) $\lnot P$;
(5,5.25) – (5,4.75);
at (5,5.4) $x$;

The real number $x$ belongs to the grid, since it is surrounded by a true (black) open interval on the left, and a false (white) open interval on the right.

Such a characterization is easy to express in our restriction of :

$$\rel(x) \! = \! (\exists y.\, y \! <\! x \land \forall z.\, y \! < \! z \! < \! x \Rightarrow P(z)) \land (\exists y.\, x \! < \! y \land \forall z.\, x \! < \! z \! < \! y \Rightarrow \lnot P(z))$$

Let us now partially axiomatize the predicate $P$ such that the set of supporting points constitutes a linear ordering of order type $\big(N + \zeta + 1 + \zeta \big)^{\omega}$:

* Let $\mathbf{0}$ be a variable and $\mathbf{1}, \mathbf{2}$ and $\mathbf{3}$ be respectively the $+1$-successor of $\mathbf{0}$, $\mathbf{1}$ and $\mathbf{2}$:

$\textit{Axiom}_1 = (\mathbf{1} = \mathbf{0} + 1) \land (\mathbf{2} = \mathbf{1} + 1) \land (\mathbf{3} = \mathbf{2} + 1)$

These free variables are implicitly existentially quantified in the final formula.

Notice that the variable $\mathbf{0}$ can be interpreted as any real value, which only acts as a landmark for the beginning of the grid.

* $\mathbf{0}$, $\mathbf{1}$ and $\mathbf{2}$ are supporting points:

$\textit{Axiom}_2 = \rel(\mathbf{0}) \land \rel(\mathbf{1}) \land \rel(\mathbf{2})$

* $P$ is uniformly true before $\mathbf{0}$, i.e., there are no supporting points before $\mathbf{0}$:

$\textit{Axiom}_3 = \forall x.\, x<\mathbf{0} \Rightarrow P(x)$

* There are exactly $N-2$ supporting points within the interval $(\mathbf{0},\mathbf{1})$:

$\textit{Axiom}_4 = \exists x_1, x_2, \dots x_{N}.\, x_1 = \mathbf{0} \land x_{N} = \mathbf{1} \\
\mbox{\hspace{45pt}} \land \bigwedge_{1\leq i<N} \big(\mathbf{0} \leq x_i< \mathbf{1} \land \onesucc(x_{i+1}, x_i)\big)$

where $\onesucc(x,y)$ is a formula that states that $x$ is the first supporting real value that is strictly greater than $y$, i.e., $x$ is the successor of $y$ on the grid. It is defined as follows:

$\onesucc(x,y) \! = \! y \! < \! x \land \rel(x) \land \rel(y) \land \forall z.\, y \! < \! z \! < \! x \Rightarrow \lnot \rel(z)$

We also define an analogous formula to express that $x$ is the predecessor of $y$: $\onepred(x, y) = \onesucc(y, x)$.

* The set of supporting points within $(\mathbf{1},\mathbf{2})$ is $<$-isomorphic to $\mathbb{Z}$. This is done similarly to the axiomatization of $\pz$ (cf. Section <ref>). But because $\mathbf{1}$ (resp. $\mathbf{2}$) is a supporting point, there must exist a uniformly false (resp. true) interval of $P$ at its right (resp. left) where no other supporting points can appear. All the supporting points will therefore be constrained to appear within a smaller interval $(b_1, b_2)$ with , as illustrated in Figure <ref>.

\begin{align}
\textit{Axiom}_5 = \,& [\exists b_1, b_2.\, \mathbf{1}<b_1<b_2<\mathbf{2}] \label{line:case1}\\
%\land \ &[\exists x.\, b_1<x<b_2 \land \rel(x)] \label{line:case2}\\
\land \ &[\forall x.\, (b_1<x<b_2) \Rightarrow \exists y.\, x<y<b_2 \land \rel(y) \nonumber \\
& \qquad \qquad \qquad \qquad \qquad \qquad \land \forall z.\, x<z<y \Rightarrow \lnot \rel(z)] \label{line:case3}\\
\land \ &[\forall x.\, (b_1<x<b_2) \Rightarrow \exists y.\, b_1<y<x \land \rel(y) \nonumber \\
& \qquad \qquad \qquad \qquad \qquad \qquad \land \forall z.\, y<z<x \Rightarrow \lnot \rel(z)] \label{line:case4}\\
\land \ &[\forall x.\, (1<x<2 \land \rel(x)) \Rightarrow b_1<x<b_2] \label{line:case5}
\end{align}

This axiom can be broken down into these elementary pieces:

(<ref>) there exists an open interval $(b_1, b_2)$ such that $\mathbf{1}<b_1<b_2<\mathbf{2}$,

(<ref>) each real value in $(b_1, b_2)$ has a supporting successor,

(<ref>) each real value in $(b_1,b_2)$ has a supporting predecessor,

(<ref>) there are no supporting points within $(\mathbf{1}, b_1)$, nor within $(b_2, \mathbf{2})$.

* The pattern of supporting points within $(\mathbf{1},\mathbf{2})$ is repeated onto the interval $(\mathbf{2},\mathbf{3})$ with an exact offset of $1$:

$\textit{Axiom}_6 = \forall x.\, \mathbf{1}<x<\mathbf{2} \Rightarrow (\rel(x) \Leftrightarrow \rel(x+1))$

* The pattern of supporting points within $[\mathbf{0},\mathbf{3})$ is repeated onto every interval $[\mathbf{3k}, \mathbf{3k+3})$ for $k \in \mathbb{N}$:

$\textit{Axiom}_7 = \forall x.\, x\geq \mathbf{0} \Rightarrow (\rel(x) \Leftrightarrow \rel(x+3))$

Notice that for $\textit{Axiom}_7$, it is not enough that a similar pattern appears within each interval $[\mathbf{3k}, \mathbf{3k+3})$: there must be an exact offset of $3$ with the previous interval. This is mandatory to connect two consecutive configurations and ensure that they are coherent with the transition relation of the Turing machine, as defined later. The same goes for $\textit{Axiom}_6$, where the exact offset of $1$ will allow to connect the position of the head to the tape content within a single configuration.

[scale=.7,node distance=2cm]
[use as bounding box] (0, 4.7) rectangle (9, 5.3);

[dotted] (1.7,5) – (1.95,5);
[dotted] (7.05,5) – (7.35,5);

[] (0,4.8) rectangle ++(-1.5,0.4);
[] (0,4.8) rectangle ++(1.5,0.4);

[] (7.5,4.8) rectangle ++(1.5,0.4);
[] (9,4.8) rectangle ++(1.5,0.4);

[] (3.7,4.8) rectangle ++(0.8,0.4);
[] (4.5,4.8) rectangle ++(0.8,0.4);

[] (2.6,4.85) rectangle ++(0.4,0.3);
[] (3,4.85) rectangle ++(0.4,0.3);

[] (5.6,4.85) rectangle ++(0.4,0.3);
[] (6,4.85) rectangle ++(0.4,0.3);

[] (2,4.9) rectangle ++(0.2,0.2);
[] (2.2,4.9) rectangle ++(0.2,0.2);

[] (6.6,4.9) rectangle ++(0.2,0.2);
[] (6.8,4.9) rectangle ++(0.2,0.2);

[thick] (0,5.3) – (0,4.7);
[thick] (9,5.3) – (9,4.7);
[] at (0,4.4) $\mathbf{1}$;
[] at (9,4.4) $\mathbf{2}$;

[thick] (1.65,5.4) – (1.65,4.6);
[thick] (7.4,5.4) – (7.4,4.6);
[] at (1.65,4.4) $b_1$;
[] at (7.4,4.4) $b_2$;

The points of the grid surrounded by open true (black) and false (white) intervals within $(\mathbf{1},\mathbf{2})$.

The formula $\paxiom = \underset{1 \leq k \leq 7}{\bigwedge} \textit{Axiom}_k$ axiomatizes the predicate $P$.

The formula $\paxiom$ is consistent.

The proof sketch below provides the key ideas to construct a model of $\paxiom$. The complete construction is described in the Appendix.

Let us construct a subset $S$ of $\mathbb{R}$ that is a model of $\paxiom$.
Firstly, we make every negative number belong to $S$, which ensures that there do not exist negative supporting points. The interval $[0,1]$ is then cut into $2N-2$ intervals of equal length, which alternate between being included in $S$, and being disjoint from $S$. This ensures the existence of exactly $N-1$ supporting points within the interval $(- \infty, 1)$, $0$ being the first; $1$ will be considered later. These $N-1$ supporting points are referred to as $s_1, s_2, \dots s_{N-1}$ and are depicted in Figure <ref>. Recall that the supporting points are exactly those surrounded by an interval of $S$ (i.e., black on the figure) on the left, and an interval disjoint from $S$ (i.e., white) on the right.

[scale=.7,node distance=2cm]
[use as bounding box] (-3.5, 4.6) rectangle (10, 5.4);

(0,4.8) rectangle ++(-3.5,0.4);

(0,4.8) rectangle ++(.75, 0.4);
(.75,4.8) rectangle ++(.75, 0.4);

(1.5,4.8) rectangle ++(.75, 0.4);
(2.25,4.8) rectangle ++(.75, 0.4);

(3,4.8) rectangle ++(.75, 0.4);
(3.75,4.8) rectangle ++(.75, 0.4);
(4.5,4.8) rectangle ++(.75, 0.4);

[thick, dotted] (5.25, 5) – (7.75, 5);

(10,4.8) rectangle ++(-.75, 0.4);
(9.25,4.8) rectangle ++(-.75, 0.4);
(8.5,4.8) rectangle ++(-.75, 0.4);

[thick] (1.5,5.3) – (1.5,4.7);
[thick] (3,5.3) – (3,4.7);
[thick] (4.5,5.3) – (4.5,4.7);
[thick] (8.5,5.3) – (8.5,4.7);
[] at (0,5.6) $s_1$;
[] at (1.5,5.6) $s_2$;
[] at (3,5.6) $s_3$;
[] at (4.5,5.6) $s_4$;
[] at (8.5,5.6) $s_{N-1}$;
[] at (10,5.6) $s_N$;

[thick] (0,5.3) – (0,4.7);
[thick] (10,5.3) – (10,4.7);
[] at (0,4.4) $0$;
[] at (10,4.4) $1$;
[] at (-3.5,4.4) $-\infty$;

A model for the axiomatization of $P$ over the interval $(-\infty, 1)$.

In order to make the real value $1$ the $N$-th supporting point, it is enough to make an interval on its right disjoint from $S$, e.g., the interval $(1,1+\frac{1}{4})$. Symmetrically, we make the interval $(2 - \frac{1}{4}, 2)$ included in $S$, satisfying the left part of the requirement for the real value $2$ to be a supporting point.

We further characterize $S$ such that the set of supporting points within the interval $(1+\frac{1}{4}, 2-\frac{1}{4})$ is $<$-isomorphic to $\mathbb{Z}$. This can be done by partitioning the open interval $(1+\frac{1}{4}, 2-\frac{1}{4})$ into a bi-infinite sequence of open intervals alternating between being included and disjoint from $S$, as depicted in Figure <ref>.

[scale=.9,node distance=2cm]
[use as bounding box] (0, 4.6) rectangle (10, 6.5);
[] (0,4.75) rectangle ++(1.5,0.5);

[] (10,4.75) rectangle ++(-1.5,0.5);

[thick] (0,5.3) – (0,4.7);
[thick] (10,5.3) – (10,4.7);
[] at (0,4.4) $1$;
[] at (10,4.4) $2$;

[] (5,4.75) rectangle ++(-1.55,0.5);
[] (5,4.75) rectangle ++(1.55,0.5);

[] (3.05,4.8) rectangle ++(-.4,0.4);
[] (3.05,4.8) rectangle ++(.4,0.4);

[] (6.95,4.8) rectangle ++(-.4,0.4);
[] (6.95,4.8) rectangle ++(.4,0.4);

[] (2.45,4.85) rectangle ++(-.2,0.3);
[] (2.45,4.85) rectangle ++(.2,0.3);

[] (7.55,4.85) rectangle ++(-.2,0.3);
[] (7.55,4.85) rectangle ++(.2,0.3);

[] (2.15,4.9) rectangle ++(-.1,0.2);
[] (2.15,4.9) rectangle ++(.1,0.2);

[] (7.85,4.9) rectangle ++(-.1,0.2);
[] (7.85,4.9) rectangle ++(.1,0.2);

[dotted] (1.5, 5) – (2.05, 5);
[dotted] (7.95, 5) – (8.5, 5);

[thick] (1.5,5.4) – (1.5,4.6);
[thick] (8.5,5.4) – (8.5,4.6);
[] at (1.5,4.3) $1.25$;
[] at (8.5,4.3) $1.75$;
[] at (1.5,5.7) $b_1$;
[] at (8.5,5.7) $b_2$;
[thick] (5,5.4) – (5,4.6);
[] at (5,4.3) $1.5$;

[] [decorate, decoration = calligraphic brace] (3.45,5.5) – (5,5.5);
[] at (4.225,5.9) $\frac{1}{8}$;

[] [decorate, decoration = calligraphic brace] (2.65,5.5) – (3.45,5.5);
[] at (3.05,5.9) $\frac{1}{16}$;

[] [decorate, decoration = calligraphic brace] (2.25,5.5) – (2.65,5.5);
[] at (2.45,5.9) $\frac{1}{32}$;

[] [decorate, decoration = calligraphic brace] (1.5,6.2) – (5,6.2);
[] at (3.25,6.55) $\frac{1}{4}$;

A model for the axiomatization of $P$ over the interval $(1,2)$.

The whole pattern described on the interval $(1,2)$ can be directly transposed onto the interval $(2,3)$ with an exact offset of $+1$. Similarly, the distribution of $S$ over the interval $(0,3)$ can be transposed onto every interval $(3k,3k+3)$ with an offset of $+3k$, for $k>0$.
The only real values for which we do not describe their relation with $S$ are the points surrounded by an interval included in $S$ on one side, and an interval disjoint from $S$ on the other side. These points never conflict with the axiomatization $\paxiom$ which only deals with non-empty open intervals.

By construction, $S$ satisfies each axiom of the formula $\paxiom$, and is therefore a model of this formula.

§.§ Encoding a Configuration of the Turing Machine

Now that the supporting grid has been properly defined, the actual encoding of a given configuration can be addressed. That is, the state, the tape content and the head position of the $(k+1)$-th configuration of a run are encoded on the supporting points contained within the interval $[3k, 3k+3)$.

§.§.§ Encoding the State

Encoding the state of a given configuration is rather direct since we defined the grid to contain $N$ consecutive supporting points within every interval $[3k, 3k+1]$ for $k \in \mathbb{N}$, that can support the encoding of a state.
We only need to indicate that we start reading the encoding on a multiple of $3$. However the logic does not allow to express periodicity constraints on variables.

Nevertheless, thanks to our axiomatization, $0$ and every other positive multiple of $3$ are the only points that simultaneously have no supporting predecessor, while admitting a supporting successor. These properties are expressible as follows:

$\mbox{\hspace{8pt}} \leftcvg(x) = \forall z.\, (z<x \land \rel(z)) \Rightarrow \exists y.\, z<y<x \land \rel(y)$

$\mbox{\hspace{8pt}} \rsucc(x) = \exists z.\, x<z \land \rel(z) \land \forall y.\, x<y<z \Rightarrow \lnot \rel(y)$

For convenience, we introduce the formula to characterize a real value $x$ on which the encoding of a state starts:

$\mbox{\hspace{8pt}} \encodbeg(x) = \rel(x) \land \leftcvg(x) \land \rsucc(x)$

Furthermore, the formula $\state{q}$ expresses that a state $q \in Q$ is encoded on a given real number $x$ and its $N-1$ supporting successors:

\begin{align*}
\state{q}(x) = &\ \encodbeg(x) \land \exists y_1, \dots y_{N}.\, x = y_1 \\
&  \quad \land  \bigwedge_{1\leq i<N} \textit{Succ}_{\textit{Sup}}(y_{i+1}, y_i) \land \bigwedge_{1\leq i \leq N} P(y_i) = b^q_i
\end{align*}

where $P(y_i) = b^q_i$ is a shorthand for $P(y_i)$ if $b^q_i = \top$, and $\lnot P(y_i)$ if $b^q_i = \bot$.

§.§.§ Encoding the Head Position

The position of the head is encoded in the second part of the grid, that is, in
the interval $(3k+1, 3k+2)$ for the $(k+1)$-th configuration
(cf. Figure <ref>).  The grid on this interval is
$<$-isomorphic to $\mathbb{Z}$.  Each element of this subordering will
correspond to a position of the tape. When the predicate $P$ is true at
such a point, it means that the head points towards that cell. Since the Turing
machines that we consider here have a single read/write head, it must point
towards a unique cell for each configuration. Therefore $P$ must be true only
for a single element of that subordering.

§.§.§ Encoding the Tape Content

Similarly, the tape content is encoded in the third part of the grid, that is,
in the interval $(3k+2, 3k+3)$ for the $(k+1)$-th configuration
(cf. Figure <ref>).  Again, the grid on this interval is
$<$-isomorphic to $\mathbb{Z}$. And again, each element $x$ of this subordering
will correspond to a cell of the tape, matching the cell that corresponds to $x-1$
in the head position interval. Figure <ref> illustrates the
connections between the suborderings, within a single configuration and with the
next one. The idea of the encoding is to simply set the value of $P$ to true
on the elements of the subordering that correspond to cells containing a $1$,
and to false for cells containing a $0$.

[use as bounding box] (-1, -1.6) rectangle (13.5, .8);
(-1,0) – (13,0);
[dotted] (13,0) – (13.5,0);

(0,-.2) – (0,.2);
(2,-.2) – (2,.2);
(4,-.2) – (4,.2);
(6,-.2) – (6,.2);
(8,-.2) – (8,.2);
(10,-.2) – (10,.2);
(12,-.2) – (12,.2);

at (0,-.5) $0$;
at (2,-.5) $1$;
at (4,-.5) $2$;
at (6,-.5) $3$;
at (8,-.5) $4$;
at (10,-.5) $5$;
at (12,-.5) $6$;

[ultra thick] [decorate, decoration = calligraphic brace] (-0.06,.4) – (5.88,.4);
[] at (3,.73) $C_0$;
[ultra thick] [decorate, decoration = calligraphic brace] (5.96,.4) – (11.88,.4);
[] at (9,.73) $C_1$;

(0.2,0.15) – (0.2,-0.15);
(0.4,0.15) – (0.4,-0.15);
(0.6,0.15) – (0.6,-0.15);
(0.8,0.15) – (0.8,-0.15);
[dotted] (1, -.1) – (1.6, -.1);
(1.8,0.15) – (1.8,-0.15);

(6.2,0.15) – (6.2,-0.15);
(6.4,0.15) – (6.4,-0.15);
(6.6,0.15) – (6.6,-0.15);
(6.8,0.15) – (6.8,-0.15);
[dotted] (7, -.1) – (7.6, -.1);
(7.8,0.15) – (7.8,-0.15);

(3,0.2) – (3,-0.2);
(3.1,0.15) – (3.1,-0.15);
(2.9,0.15) – (2.9,-0.15);
(3.2,0.15) – (3.2,-0.15);
(2.8,0.15) – (2.8,-0.15);
(3.3,0.12) – (3.3,-0.12);
(2.7,0.12) – (2.7,-0.12);
(3.4,0.1) – (3.4,-0.1);
(2.6,0.1) – (2.6,-0.1);
(3.5,0.1) – (3.5,-0.1);
(2.5,0.1) – (2.5,-0.1);
(3.6,0.1) – (3.6,-0.1);
(2.4,0.1) – (2.4,-0.1);
(3.7,0.08) – (3.7,-0.08);
(2.3,0.08) – (2.3,-0.08);

(5,0.2) – (5,-0.2);
(5.1,0.15) – (5.1,-0.15);
(4.9,0.15) – (4.9,-0.15);
(5.2,0.15) – (5.2,-0.15);
(4.8,0.15) – (4.8,-0.15);
(5.3,0.12) – (5.3,-0.12);
(4.7,0.12) – (4.7,-0.12);
(5.4,0.1) – (5.4,-0.1);
(4.6,0.1) – (4.6,-0.1);
(5.5,0.1) – (5.5,-0.1);
(4.5,0.1) – (4.5,-0.1);
(5.6,0.1) – (5.6,-0.1);
(4.4,0.1) – (4.4,-0.1);
(5.7,0.08) – (5.7,-0.08);
(4.3,0.08) – (4.3,-0.08);

(9,0.2) – (9,-0.2);
(9.1,0.15) – (9.1,-0.15);
(8.9,0.15) – (8.9,-0.15);
(9.2,0.15) – (9.2,-0.15);
(8.8,0.15) – (8.8,-0.15);
(9.3,0.12) – (9.3,-0.12);
(8.7,0.12) – (8.7,-0.12);
(9.4,0.1) – (9.4,-0.1);
(8.6,0.1) – (8.6,-0.1);
(9.5,0.1) – (9.5,-0.1);
(8.5,0.1) – (8.5,-0.1);
(9.6,0.1) – (9.6,-0.1);
(8.4,0.1) – (8.4,-0.1);
(9.7,0.08) – (9.7,-0.08);
(8.3,0.08) – (8.3,-0.08);

(11,0.2) – (11,-0.2);
(11.1,0.15) – (11.1,-0.15);
(10.9,0.15) – (10.9,-0.15);
(11.2,0.15) – (11.2,-0.15);
(10.8,0.15) – (10.8,-0.15);
(11.3,0.12) – (11.3,-0.12);
(10.7,0.12) – (10.7,-0.12);
(11.4,0.1) – (11.4,-0.1);
(10.6,0.1) – (10.6,-0.1);
(11.5,0.1) – (11.5,-0.1);
(10.5,0.1) – (10.5,-0.1);
(11.6,0.1) – (11.6,-0.1);
(10.4,0.1) – (10.4,-0.1);
(11.7,0.08) – (11.7,-0.08);
(10.3,0.08) – (10.3,-0.08);

[-Stealth[length=2mm]] (3,-.3) to [bend right=75] node[below] $+1$ (5,-.3);
[-Stealth[length=2mm]] (3,-.3) to [bend right=100] node[above] $+3$ (9,-.3);

The first two consecutive configuration encodings.

§.§ Enforcing a Valid Run

Let us now define formally the formulas characterizing an accepting run of $\mathcal{M}$. We will decompose the global formula into three main parts: the initial conditions $\startformula$, the conditions on the transitions $\stepformula$ and the halting condition $\terminationformula$. For the sake of clarity, we use capital letters for these higher-level formulas.

The initial conditions of $\mathcal{M}$ are that the state encoded on $\mathbf{0}$ and its $N-1$ supporting successors is the initial state $q_0$, that the head points towards a unique initial unspecified cell of the tape, and finally that the tape is initially filled with $0$'s.
These conditions are expressed by the following formula:

\begin{align*}
\startformula = \state{q_0}(\mathbf{0})\ \land\ & \big[\exists y.\, \mathbf{1}<y<\mathbf{2} \land \rel(y) \land P(y) \\
& \quad \land \forall x.\, (\mathbf{1}<x<\mathbf{2} \land \rel(x) \land P(x)) \Rightarrow x=y\big] \\
\land\ & \big[\forall y.\, (\mathbf{2}<y<\mathbf{3} \land \rel(y)) \Rightarrow \lnot P(y)\big]
\end{align*}

The requirements on the transition are more complex.
Intuitively, if before reaching the step $i \in \mathbb{N}$, we have not yet encountered the halting state $q_F$, then we must ensure that the configuration at Step $i$ can be obtained from the configuration at the previous step $i-1$ by following a transition .
The overall formula for this condition is the following:

\begin{align*}
\stepformula = \forall y.\, (& y>0 \land \encodbeg(y) \land \textit{NotEnded}_\mathcal{M}(y)) \\
& \Rightarrow \exists x.\, y = x + 3 \land \textit{Transition}_\mathcal{M}(x, y)
\end{align*}

The subformula $\textit{NotEnded}_\mathcal{M}(y)$ expresses that no valid real value prior to $y$ (i.e., a positive multiple of $3$ strictly smaller than $y$) encodes the halting state. This formula is defined by:

\begin{align*}
\textit{NotEnded}_\mathcal{M}(y) = \forall x.\, (x<y \land \encodbeg(x)) \Rightarrow \lnot (\textit{State}_{q_F}(x))
\end{align*}

The subformula $\textit{Transition}_{\mathcal{M}}(x,y)$ expresses that there exists a transition $(q, \alpha, q', \alpha', \lambda) \in \Delta$ that allows to move in one step from the configuration encoded at $x$ (i.e., that the encoding of the configuration starts exactly on $x$), to the configuration corresponding to $y$.

To improve readability, we decompose the condition on the transition relation as follows:

\begin{align*}
&\textit{Transition}_\mathcal{M}(x, y) =\\
&\qquad \bigvee_{(q, \alpha, q', \alpha', \lambda) \in \Delta}  \Big[  \state{q}(x) \land \state{q'}(y) \land \textit{Tape}_{\alpha, \alpha'}(x, y) \land \textit{Head}_{\lambda}(x, y) \Big]
\end{align*}

For a given transition $(q, \alpha, q', \alpha', \lambda) \in \Delta$, the conditions on the states, tape and head are expressed as follows:

* The state $q$ must be encoded on the real value $x$, and the state $q'$ on $y$: $\state{q}(x) \land \state{q'}(y)$

* The tape must contain $\alpha \in \{0,1\}$ at the position of the head for the
step corresponding to $x$. Additionally, for the step corresponding to $y$, the tape must contain $\alpha'$ at
the previous position of the head, and remain unchanged at all other positions.

\begin{align*}
&\textit{Tape}_{\alpha, \alpha'}(x, y) = \big[\forall z.\, (x+1<z<x+2 \land \rel(z) \land P(z)) \\
&\mbox{\hspace{180pt}} \Rightarrow P(z+1) = \alpha \land P(z+4) = \alpha'\big] \\
&\land \! \big[\forall z.\, (x+1<z<x+2 \land \rel(z) \land \lnot P(z)) \Rightarrow (P(z+1) \Leftrightarrow P(z+4))\big]
\end{align*}

Where $P(z+k) = \alpha$ is a shorthand for $\exists u.\, u = z+k \land P(u)$ if $\alpha = 1$, and $\exists u.\, u = z+k \land \lnot P(u)$ if $\alpha = 0$. The $``+1"$ operator allows us to connect the encoding of the head position with the encoding of the tape content within the same configuration. The $``+4"$ operator does the same while jumping to the next configuration (cf. Figure 4).
Notice that this formula does not involve $y$; it assumes (rightfully, given the formula $\stepformula$) that the equality $y = x+3$ holds.

* The head is moved in the direction specified by $\lambda \in \{L, R\}$, i.e., left for $L$ and right for $R$. This can be expressed by exploiting the predecessor and successor relations defined for supporting real values.

\begin{align*}
\textit{Head}_{\lambda}(x, y) = \, \forall z.\, &(x+1<z<x+2 \land \rel(z) \land P(z)) \\
& \quad \Rightarrow \exists v.\, f_\lambda(v, z+3) \land P(v) \land \lnot P(z)
\end{align*}

where $f_R = \onesucc$ and $f_L = \onepred$.
Since in the initial configuration of the Turing machine the head points towards a single cell, the formula $\textit{Head}_{\lambda}$ ensures that this remains the case throughout every run of the Turing machine.

Finally, the existence of a halting run is expressed by the formula:

\begin{align*}
\textit{END}_{\mathcal{M}} = \exists x.\, \state{q_F}(x)
\end{align*}

The global formula that expresses that the Turing machine $\mathcal{M}$
halts on some run encoded by the value of the predicate $P$ is the following:

\begin{align*}
\textit{HALT}_{\mathcal{M}} = \textit{START}_{\mathcal{M}} \land \textit{STEP}_{\mathcal{M}} \land \textit{END}_{\mathcal{M}} \land \paxiom
\end{align*}

where $\paxiom$ is the axiomatization of the supporting points as described in Section <ref>.

By construction, satisfiability of the global formula $\haltformula$ is equivalent to the existence of a halting run for the Turing machine $\mathcal{M}$. It follows that the satisfiability problem for is undecidable, which proves Theorem <ref>.

§ CONCLUSION

This work provides a lower and an upper bound for the decidability of first-order
fragments with quantifiers mixing uninterpreted unary predicates and weak forms
of real arithmetic.  This draws a precise picture of the
frontier of decidability in fragments mixing real arithmetic and uninterpreted

We proved the decidability of the fragment , where uninterpreted unary
predicates, order constraints between real and integer variables, and
difference logic constraints between integer variables are allowed.  This result
is a consequence of the already established decidability of its restriction
, where only uninterpreted unary predicates and order constraints between
real values are allowed. To the best of our knowledge, there does not exist yet
a practical decision procedure for .

It would be interesting to investigate which arithmetic extensions of this decidable fragment preserve decidability. Note however that our proof of decidability relies on the translation of the fragment constraints into the first-order theory of order over $\mathbb{R}$, with unary predicates, which is not directly feasible for, e.g., constraints of the form $x+y \bowtie 0$, where $x$ and $y$ are variables, and $\bowtie \ \in \{<, \leq, =, \geq, >\}$.

In another result, we established the undecidability of the fragment , where
uninterpreted unary predicates and difference logic constraints between real
variables are allowed. It is worth mentioning that this result can be adapted straightforwardly to the same logic interpreted over the domain $\mathbb{Q}$.

Our long term goal is to design an effective decision procedure for the decidable fragment.  Complexity results have been established [12, 5, 13] for the temporal logic counterpart of the theory of order, to which we reduce the decidability of our fragment of interest. We are currently designing a decision procedure relying on the concept of automata on linear orderings introduced in [2].
We hope that the insight we obtained through this decision procedure will eventually guide the design of new powerful instantiation techniques for SMT in a more expressive context, and that these techniques will happen to be complete in particular for this decidable fragment.

Acknowledgments:  We are thankful to Tanja Schindler and the reviewers of
this paper and of our previous work-in-progress workshop paper for their comments.

[1]
Boigelot, B., Fontaine, P., Vergain, B.: Decidability of difference logics with
unary predicates. Proceedings, 7th International Workshop on Satisfiability
Checking and Symbolic Computation  (2022)

[2]
Bruyère, V., Carton, O.: Automata on linear orderings. Journal of Computer and
System Sciences  73(1),  1–24 (2007)

[3]
Büchi, J.R.: On a decision method in restricted second order arithmetic,
Logic, Methodology and Philosophy of Science (1962)

[4]
Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic.
Notre Dame Journal of Formal Logic  26(2),  115–128 (1985)

[5]
Cristau, J.: Automata and temporal logic over arbitrary linear time. In:
FSTTCS 2009. LIPIcs, vol. 4, pp. 133–144 (2009)

[6]
Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic
predicate letter. Tech. rep., Center for Research in Computer Technology,
Harvard University (1972)

[7]
Enderton, H.B.: A mathematical introduction to logic (2nd edition). Academic
Press, Boston (2001)

[8]
Gurevich, Y., Shelah, S.: Monadic theory of order and topology in ZFC.
Annals of Mathematical Logic  23(2-3),  179–198 (1982)

[9]
Haase, C.: A survival guide to Presburger arithmetic. ACM SIGLOG News
5(3),  67–82 (2018)

[10]
Halpern, J.Y.: Presburger arithmetic with unary predicates is $\Pi_1^1$
complete. The Journal of Symbolic Logic  56(2),  637–642 (Jun 1991)

[11]
Matiyasevich, Y.V.: Hilbert's Tenth Problem. MIT Press, Cambridge, MA, USA

[12]
Rabinovich, A.: Temporal logics over linear time domains are in
PSPACE. Information and Computation  210,  40–67 (2012)

[13]
Reynolds, M.: The complexity of temporal logic over the reals. Annals of Pure
and Applied Logic  161(8),  1063–1096 (2010)

[14]
Rosenstein, J.G.: Linear orderings. Academic press (1982)

[15]
Shannon, C.E.: A universal Turing machine with two internal states. Automata
studies  34,  157–165 (1956)

[16]
Shelah, S.: The monadic theory of order. Annals of Mathematics
102(3),  379–419 (1975)

[17]
Sierpiński, W.: Cardinal and ordinal numbers (2nd edition). PWN, Warszawa

[18]
Speranski, S.O.: A note on definability in fragments of arithmetic with free
unary predicates. Arch. Math. Log.  52(5-6),  507–516 (2013)

[19]
Tarski, A.: A Decision Method for Elementary Algebra and Geometry. Univ. of
California Press, 2nd edn. (1951)

§ APPENDIX

In order to formally prove Lemma <ref>, we provide a complete description of a model of the formula $\paxiom$.

In order to prove that the axiomatization is consistent, let us construct a model for $\paxiom$.
Let $S$ be a subset of $\mathbb{R}$ such that:

* All strictly negative numbers belong to $S$:	$(-\infty, 0) \subseteq S$.

* The interval $[0,1]$ is cut into $2N-2$ intervals of equal length, that are either included or disjoint from $S$:

* $(\frac{i}{N-1}, \frac{2i+1}{2(N-1)}) \subseteq \mathbb{R} \setminus S$ for all $i \in [0,N-2]$,

* $(\frac{2i+1}{2(N-1)}, \frac{i+1}{N-1}) \subseteq S$ for all $i \in [0,N-2]$.

This distribution ensures the existence of exactly $N-1$ supporting points ($0$ is the first one, and $1$ will be considered later). These $N-1$ supporting points are referred to as $s_1, s_2, \dots s_{N-1}$, and they are depicted in Figure <ref>. Recall that the supporting points are exactly those surrounded by an interval of $S$ (i.e., black on the figure) on the left, and an interval of the complement of $S$ (i.e., white) on the right.

* For the interval $[1,2]$, we first ensure that $1$ is also a supporting point by making the open interval $(1, 1+\frac{1}{4})$ on its right belong to $\mathbb{R} \setminus S$. We also make the interval $(2-\frac{1}{4},2)$ belong to $S$, to deal with the left part of the requirement of $2$ being a supporting point.

Furthermore, in order to generate the desired set of supporting points within $(1,2)$ (that must be  to $\mathbb{Z}$), we partition the interval  $(1 + \frac{1}{4}, 2 - \frac{1}{4})$ into a bi-infinite sequence of disjoint open subintervals that alternate between being included and disjoint from $S$, as depicted in Figure <ref>:

* $(1 , 1 + \frac{1}{4}) \subseteq \mathbb{R} \setminus S$, and $(2 - \frac{1}{4}, 2) \subseteq S$,

* $(1 + \frac{3}{8}, 1 + \frac{1}{2}) \subseteq S$ and $(1 + \frac{1}{2}, 1 + \frac{5}{8}) \subseteq \mathbb{R} \setminus S$,

* $(1 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i}, 1 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}) \subseteq S$ for all $j \geq 4$,

* $(1 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}, 1 + \frac{1}{2} - \sum\limits_{i=3}^{j-1}\frac{1}{2^i}) \subseteq \mathbb{R} \setminus S$ for all $j \geq 4$,

* $(1 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i}, 1 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}) \subseteq S$ for all $j \geq 3$,

* $(1 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}, 1 + \frac{1}{2} + \sum\limits_{i=3}^{j+1}\frac{1}{2^i}) \subseteq \mathbb{R} \setminus S$ for all $j \geq 3$.

Notice that the union of all the intervals for which we state their relation to $S$, covers the interval $(1,2)$ entirely apart from isolated points that are surrounded by an interval included in $S$, and an interval disjoint from $S$. Some of them are supporting points (when the interval included in $S$ is on the left, and the interval disjoint from $S$ is on the right), the others are completely irrelevant.

* The pattern described on the interval $(1,2)$ can be directly transposed onto the interval $(2,3)$, with an exact offset of $+1$:

* $(2 , 2 + \frac{1}{4}) \subseteq \mathbb{R} \setminus S$, and $(3 - \frac{1}{4}, 3) \subseteq S$,

* $(2 + \frac{3}{8}, 2 + \frac{1}{2}) \subseteq S$ and $(2 + \frac{1}{2}, 2 + \frac{5}{8}) \subseteq \mathbb{R} \setminus S$,

* $(2 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i}, 2 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}) \subseteq S$ for all $j \geq 4$,

* $(2 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}, 2 + \frac{1}{2} - \sum\limits_{i=3}^{j-1}\frac{1}{2^i}) \subseteq \mathbb{R} \setminus S$ for all $j \geq 4$,

* $(2 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i}, 2 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}) \subseteq S$ for all $j \geq 3$,

* $(2 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}, 2 + \frac{1}{2} + \sum\limits_{i=3}^{j+1}\frac{1}{2^i}) \subseteq \mathbb{R} \setminus S$ for all $j \geq 3$.

* Finally, the distribution of $S$ over the interval $(0,3)$ defined above can be transposed to every interval $(3k,3k+3)$ for $k > 0$:

* $(3k+\frac{i}{N-1}, 3k+\frac{2i+1}{2(N-1)}) \subseteq \mathbb{R} \setminus S$ for all $i \in [0,N-2]$,

* $(3k+\frac{2i+1}{2(N-1)}, 3k+\frac{i+1}{N-1}) \subseteq S$ for all $i \in [0,N-2]$.

* $(3k + 1 , 3k + \frac{1}{4}) \subseteq \mathbb{R} \setminus S$, and $(3k + 2 - \frac{1}{4}, 3k + 2) \subseteq S$,

* $(3k + 1 + \frac{3}{8}, 3k + 1 + \frac{1}{2}) \subseteq S$ and $(3k + 1 + \frac{1}{2}, 3k + 1 + \frac{5}{8}) \subseteq \mathbb{R} \setminus S$,

* $(3k + 1 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i}, 3k + 1 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}) \subseteq S$ for all $j \geq 4$,

* $(3k + 1 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}, 3k + 1 + \frac{1}{2} - \sum\limits_{i=3}^{j-1}\frac{1}{2^i}) \subseteq \mathbb{R} \setminus S$ for all $j \geq 4$,

* $(3k + 1 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i}, 3k + 1 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}) \subseteq S$ for all $j \geq 3$,

* $(3k + 1 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}, 3k + 1 + \frac{1}{2} + \sum\limits_{i=3}^{j+1}\frac{1}{2^i}) \subseteq \mathbb{R} \setminus S$ for all $j \geq 3$,

* $(3k + 2 , 3k + 2 + \frac{1}{4}) \subseteq \mathbb{R} \setminus S$, and $(3k+3  - \frac{1}{4}, 3k+3) \subseteq S$,

* $(3k + 2 + \frac{3}{8}, 3k + 2 + \frac{1}{2}) \subseteq S$ and $(3k + 2 + \frac{1}{2}, 3k + 2 + \frac{5}{8}) \subseteq \mathbb{R} \setminus S$,

* $(3k + 2 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i}, 3k + 2 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}) \subseteq S$ for all $j \geq 4$,

* $(3k + 2 + \frac{1}{2} - \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}, 3k + 2 + \frac{1}{2} - \sum\limits_{i=3}^{j-1}\frac{1}{2^i}) \subseteq \mathbb{R} \setminus S$ for all $j \geq 4$,

* $(3k + 2 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i}, 3k + 2 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}) \subseteq S$ for all $j \geq 3$,

* $(3k + 2 + \frac{1}{2} + \sum\limits_{i=3}^{j}\frac{1}{2^i} + \frac{1}{2^{j+2}}, 3k + 2 + \frac{1}{2} + \sum\limits_{i=3}^{j+1}\frac{1}{2^i}) \subseteq \mathbb{R} \setminus S$ for all $j \geq 3$.

The only real values for which we do not describe their relation with $S$, are isolated points (some of them constituting the support, some not). They never conflict with the axiomatization $\paxiom$ which only deals with non-empty open intervals.

By construction, $S$ satisfies each axiom of the formula $\paxiom$, and is therefore a model.