# Floquet prethermalization with lifetime exceeding 90s in a bulk
hyperpolarized solid

William Beatrez  Department of Chemistry, University of California, Berkeley,
Berkeley, CA 94720, USA.  Otto Janes  Department of Chemistry, University of
California, Berkeley, Berkeley, CA 94720, USA.  Amala Akkiraju  Department of
Chemistry, University of California, Berkeley, Berkeley, CA 94720, USA.  Arjun
Pillai  Department of Chemistry, University of California, Berkeley, Berkeley,
CA 94720, USA.  Alexander Oddo  Department of Chemistry, University of
California, Berkeley, Berkeley, CA 94720, USA.  Paul Reshetikhin  Department
of Chemistry, University of California, Berkeley, Berkeley, CA 94720, USA.
Emanuel Druga  Department of Chemistry, University of California, Berkeley,
Berkeley, CA 94720, USA.  Maxwell McAllister  Department of Chemistry,
University of California, Berkeley, Berkeley, CA 94720, USA.  Mark Elo  Tabor
Electronics Inc. Hatasia 9, Nesher, 3660301, Israel.  Benjamin Gilbert  Energy
Geoscience Division, Lawrence Berkeley National Laboratory, Berkeley, CA
94720, USA.  Dieter Suter  Fakultät Physik, Technische Universität Dortmund,
D-44221 Dortmund, Germany.  Ashok Ajoy<EMAIL_ADDRESS>Department of
Chemistry, University of California, Berkeley, Berkeley, CA 94720, USA.
Chemical Science Division, Lawrence Berkeley National Laboratory, University
of California, Berkeley, Berkeley, CA 94720, USA.

###### Abstract

We report the observation of long-lived Floquet prethermal states in a bulk
solid composed of dipolar-coupled ${}^{13}\textrm{C}$ nuclei in diamond at
room temperature. For precessing nuclear spins prepared in an initial
transverse state, we demonstrate pulsed spin-lock Floquet control that
prevents their decay over multiple-minute long periods. We observe Floquet
prethermal lifetimes $T_{2}^{\prime}{\approx}$90.9s, extended ${>}$60,000-fold
over the nuclear free induction decay times. The spins themselves are
continuously interrogated for ${\sim}$10min, corresponding to the application
of ${\approx}$5.8M control pulses. The ${}^{13}\textrm{C}$ nuclei are
optically hyperpolarized by lattice Nitrogen Vacancy (NV) centers; the
combination of hyperpolarization and continuous spin readout yields
significant signal-to-noise in the measurements. This allows probing the
Floquet thermalization dynamics with unprecedented clarity. We identify four
characteristic regimes of the thermalization process, discerning short-time
transient processes leading to the prethermal plateau, and long-time system
heating towards infinite temperature. This work points to new opportunities
possible via Floquet control in networks of dilute, randomly distributed, low-
sensitivity nuclei. In particular, the combination of minutes-long prethermal
lifetimes and continuous spin interrogation opens avenues for quantum sensors
constructed from hyperpolarized Floquet prethermal nuclei.

Fig. 1: System. (A) Dipolar lattice of ${}^{13}\textrm{C}$ nuclei in diamond.
Optically pumped NV centers are employed to hyperpolarize the
${}^{13}\textrm{C}$ nuclei (blue arrows). (B-C) Signal gains from
hyperpolarization, demonstrated by comparing single-shot ${}^{13}\textrm{C}$
NMR spectra to conventional 7T (thermal) NMR. Data is shown in (B) linear and
(C) log scales; line is a fit. Here, optical pumping was for 2min at 36mT, and
thermal measurement was taken after 4hrs in the magnet.  Fig. 2: Floquet
driving and lifetime extension. (A) Conventional ${}^{13}\textrm{C}$ free
induction decay with $T_{2}^{\ast}{\approx}$1.5ms. (B) Floquet drive consists
of a train of $\theta$-pulses applied spin-locked with the ${}^{13}\textrm{C}$
nuclei. Spins are interrogated in $t_{\textrm{acq}}$ windows between the
pulses (blue lines), the nuclear precession is sampled every 1ns. Pulse
repetition rate $\omega=\tau^{-1}$, and sequence not drawn to scale. (C)
Minutes-long lifetimes of the transverse state result from the Floquet
sequence ($\theta{\approx}\pi/2$). Data (blue points) shows single-shot
measurement of survival probability in the state $\rho_{I}$, and line is a fit
to a sum of five exponentials. Here $t_{\textrm{acq}}{=}2\mu$s,
$t_{p}{=}40\mu$s and $\tau{=}99.28\mu$s, and the 573s period corresponds to
${\approx}$5.8M pulses (upper axis). We neglect here the first 100ms for
clarity (see Fig. 3A). Inset (i): Raw data showing measurement of the
${}^{13}\textrm{C}$ spin precession, here at 1s into the decay. Inset (ii):
Data zoomed 200x in a 1s window. Using a 1/$e$-proxy yields
$T_{2}’{\approx}90.9$s. This corresponds to a ${>}$60,000-fold extension
compared to the FID.

Introduction – Systems pulled away from thermal equilibrium can exhibit
unusual phenomena non-existent or difficult to achieve at equilibrium [1]. For
instance, periodically driven quantum systems can display long-lived
prethermal lifetimes due to the emergence of approximately conserved
quantities under the effective time-independent Hamiltonian describing the
drive [2, 3, 4, 5, 6]. For sufficiently large driving frequencies $\omega$,
much higher than the intrinsic energy scales in the system Hamiltonian
(hereafter $J$), these prethermal lifetimes scale exponentially with $\omega$
[7, 8, 9, 10, 11]. Ultimately, however, the system absorbs energy and “heats
up” to a featureless infinite temperature state.

The long-lived prethermal plateau and its stability against perturbations in
the drive portends applications for the engineering of quantum states [3, 4,
12]. Fundamentally, the control afforded by periodically driven systems opens
avenues to study non-equilibrium phenomena and explore novel dynamic phases of
matter, some of which have no equilibrium counterparts [13, 14]. A flurry of
theoretical work has recognized Floquet prethermalization under random driving
[15], in driven linear chains [10], and even in the classical limit [16].
Experimentally, Floquet prethermalization has been observed recently in cold-
atom [17, 18, 19] and NMR systems [20, 21, 22]. They demonstrated a
characteristic exponential suppression of heating rates with Floquet driving.
Even before the current resurgence of interest, decades-old NMR experiments
had observed certain signatures of prethermalization, then referred to as
“quasi-equilibrium” [23, 24, 25, 26, 27, 28].

In this Letter, we report observation of Floquet prethermal states with
lifetimes exceeding 90s at room temperature in a dipolar-coupled ensemble of
${}^{13}\textrm{C}$ nuclei in diamond (see Fig. 1A). These nuclear spins,
randomly positioned at 1% concentration in the lattice, are optically
hyperpolarized by interactions with NV defect centers, which enhances their
polarization $\varepsilon{=}223$-fold with respect to the thermal limit (Fig.
1B). When placed in a Bloch transverse state $\hat{\textbf{x}}$ in the absence
of periodic driving, these precessing nuclei naturally dephase with free
induction decay lifetime $T_{2}^{*}{\approx}1.5$ms and measured observables
decay to zero. Under rapid pulsed spin-lock driving, however, we are able to
effect a significant improvement; the observed lifetimes
$T_{2}’{\approx}$90.9s constitute a ${>}$60,000-fold extension over
$T_{2}^{*}$. Moreover, with a drive consisting of ${\approx}$5.8M pulses, we
are able to continuously probe the thermalization process for up to 573s with
high fidelity. This corresponds to ${>}10^{10}$ precession cycles of the
nuclear spins. Both with respect to the number of pulses applied, and the
ultimate transverse spin lifetimes, these values are amongst the largest
reported in literature [29, 30]. Our work therefore suggests interesting
opportunities for Floquet control afforded in hyperpolarizable spin networks
consisting of dilute low-gyromagnetic ratio nuclei [31].

A primary contribution in this work is the ability to probe the system
thermalization dynamics with unprecedented signal-to-noise (SNR). Integrated
SNR (see Fig. 1B-C) exceeds $10^{9}$ per shot, arising from a combination of
hyperpolarization and continuous spin readout in our experiments. This permits
a view into the thermalization process with a high degree of clarity, in a
manner not directly accessible in previous experiments. We are able to
identify the four smoothly transitioning thermalization regimes that confirm
theoretical predictions [32] — an initial transient to the prethermal plateau,
the crossover to unconstrained thermalization and, ultimately, infinite
temperature. High measurement SNR also allows characterization of heating
rates over a wide range of drive frequencies. We observe system heating
scaling $\propto\exp(-t^{1/2})$ at high drive frequency $\omega$.
Simultaneously, the transient system response unveils interesting harmonic
behavior while establishing the prethermal plateau.

System – In a magnetic field $\textbf{B}_{0}$, the ${}^{13}\textrm{C}$ nuclei
interact by the dipolar Hamiltonian,
$\mathcal{H}_{dd}=\sum_{j<k}d_{jk}^{\textrm{CC}}(3I_{jz}I_{kz}-\vec{I_{j}}\cdot\vec{I_{k}})$,
with a coupling strength
$d_{jk}^{\textrm{CC}}=\frac{\mu_{0}}{4\pi}\hbar\gamma_{n}^{2}(3\cos^{2}\beta_{jk}-1)\frac{1}{r_{jk}^{3}}$
, where $I$ refer to spin-1/2 Pauli matrices, $\gamma_{n}$=10.7MHz/T is the
gyromagnetic ratio, and
$\beta_{jk}=\cos^{-1}\left(\frac{\textbf{r}_{jk}\cdot\textbf{B}_{0}}{r_{jk}B_{0}}\right)$
is the angle of the internuclear vector $\textbf{r}_{jk}$ to the magnetic
field. The sample is oriented with $\textbf{B}_{0}{||}[100]$, such that
nearest neighbor (NN) ${}^{13}\textrm{C}$ sites are decoupled. Ultimately, the
median dipolar coupling is $J=\left\langle
d_{jk}^{\textrm{CC}}\right\rangle{\approx}$0.66kHz (Fig. 2A). The random
${}^{13}\textrm{C}$ distribution leads to a long tailed distribution in the
coupling values, effectively rendering the interaction Hamiltonian disordered.
In addition, the nuclei are subject to on-site disorder, i.e. local dephasing
fields, $\mathcal{H}_{z}=\sum_{j}c_{j}I_{jz}$, arising from interactions with
paramagnetic impurities (e.g. P1 centers) [33]. At typical 20ppm P1
concentrations, $\left\langle c_{j}^{2}\right\rangle\approx$0.4[kHz]2 [34]. In
the rotating frame of the Floquet drive, the ${}^{13}\textrm{C}$ Hamiltonian
is therefore $\mathcal{H}=\mathcal{H}_{dd}+\mathcal{H}_{z}$.

Compared to previous NMR experiments, our work introduces some special
features leveraging nuclear hyperpolarization [25, 26]. The vast preponderance
of NMR experiments have been limited to high-$\gamma_{n}$ and dense (100%
abundant) nuclei such as 19F, 31P, and 1H [22, 20]. Instead, we focus
attention to dilute networks of insensitive nuclei (${}^{13}\textrm{C}$). This
provides a combination of factors critical to establishing Floquet control for
long periods — (i) a relatively low $\|\mathcal{H}_{\textrm{dd}}\|$ compared
to networks constructed from sensitive (high-$\gamma_{n}$) nuclei, scaling as
$\eta^{1/2}\gamma_{n}^{2}$, where $\eta$ is the nuclear enrichment, (ii) a
long tailed distribution in couplings, and (iii) long nuclear $T_{1}$ (here
${\approx}$25 min), significantly higher than many experimental systems, sets
a long memory time for the nuclear states.

Indeed, these very factors, while attractive for Floquet control [35], usually
make experiments challenging on account of poor sensitivity. Inductively
measured nuclear signals scale $\propto\gamma_{n}^{2}$, with a measurement
repetition rate set by $T_{1}^{-1}$, making obtaining reasonable SNR a
challenge [36]. We mitigate these difficulties by a combination of
hyperpolarization and instrumental advances (allowing continuous sampling).
Hyperpolarization is carried out at $B_{\textrm{pol}}{=}36$mT through a method
previously described [37, 38]. Measurement throughput is accelerated by
${\approx}\frac{1}{2}\varepsilon^{2}\left[T_{1}(B_{0})/T_{1}(B_{\textrm{pol}})\right]^{2}\frac{T_{2}’}{T_{2}^{*}}{\gtrsim}10^{10}$
over conventional high-field (FID-based) NMR readout.

Fig. 3: Floquet thermalization regimes (A) Log-scale visualization of the full
data in Fig. 2C. Points are experiment, there are ${\approx}5.8$M data points
here. Lines are carried out in two segments with solid and dashed lines
referring to a stretched exponential with $\alpha{=}0.55$ and $\alpha{=}0.5$
respectively. Upper axis denotes number of pulses applied, here
$J\tau\approx$0.066. Green points are the FID. We observe distinct, yet
smoothly transitioning (shaded), thermalization regimes (I-IV): a
${\approx}10$ms oscillatory approach (I) to the Floquet prethermal plateau
(II), followed by unconstrained thermalization (III). Infinite temperature
regime (IV) is not reached in these measurements up to 573s. (B) Semi-log plot
of the experimental data (red points) in regime II-III shows a dynamic change
of thermalization rate. Moving averaging is applied here every 0.1s. Blue line
is a fit to a sum of five exponentials. (C) Semi-log plot against $\sqrt{t}$
yields an approximately linear dependence (dashed line) for ${\sim}500$s. Cusp
(marked) at ${\approx}$9.2ms marks transition to the prethermal plateau
(regime II, see also Fig. 5).  Fig. 4: Exponential dependence of Floquet
prethermal lifetimes. (A) Variation with $J\tau$. Data (points) shows measured
signal probing thermalization dynamics in regime II-III for representative
$J\tau$ values (colorbar). Here $\theta{\approx}\pi/2$ and
$t_{\textrm{acq}}{=}32\mu$s and there are a high number
(${\sim}10^{3}$-$10^{6}$) points per line [39]. Data is normalized at the
transition points to the prethermal plateau (following Fig. 3C). The Floquet
prethermal decay rates reduce considerably with decreasing $J\tau$. See full
data at Ref. [40]. Inset: Zoom-in (on semilog scale). (B) Extracted decay
rates focusing on the region where decay follows ${\sim}\exp(-t^{1/2})$.
Plotted in a semi-log scale against $\omega/J$, the dashed line reveals an
approximately exponential scaling of the decay rates at low drive frequencies
$\omega$ (dashed line is a linear fit). At high $\omega$ we observe sharp
narrow features in the prethermal decay rates. (C) Plotted against $J\tau$,
showing exponential scaling at higher drive frequency (dashed line). Narrow
features in the decay rates superimposed on the exponential background are
more emphasized here. (D) Log-scale plot of the extracted $T_{2}’$ lifetimes
against $\omega$. Dashed line is a linear fit.

Floquet control and measurement — The driving protocol is described in Fig. 2B
[41, 42, 43]. Post polarization, the ${}^{13}\textrm{C}$ nuclei are rotated to
transverse axis $\hat{\textbf{x}}$ on the Bloch sphere, placing them in an
initial state $\rho_{I}{\sim}\varepsilon I_{x}$. The Floquet drive consists of
an equally spaced train of pulses of flip angle $\theta$. The center-to-center
pulse separation is $\tau\left[{=}(\omega/2\pi)^{-1}\right]$. After $N$
pulses, the unitary operator describing its action in the rotating frame can
be written as, $U(N\tau)=\left[\exp(i\theta
I_{x})\exp(i\mathcal{H}\tau)\right]^{N}$, where we have made a simplifying
assumption of $\delta$-pulses. The data is sampled after every pulse,
$t_{j}{=}j\tau$, and the evolution can be described by the operation
$U(t)=\prod_{j=1}^{N}\exp(i\mathcal{H}^{(j)}\tau)$, where we refer to the
toggling frame Hamiltonians after every pulse [44],
$\mathcal{H}^{(j)}=\exp(ij\theta I_{x})\mathcal{H}\exp(-ij\theta I_{x})$. This
evolution can be recast as, $U(t)=\exp(i\mathcal{H}_{F}N\tau)$, where $H_{F}$
is the Floquet Hamiltonian that captures the system dynamics under the drive.
$\mathcal{H}_{F}$ can be expanded in a Floquet-Magnus expansion [45, 46, 47]
to leading order in the parameter $\zeta{=}2\pi J/\omega$, and in the regime
$\zeta{\ll}1$, yields a time independent Hamiltonian,

${\mathcal{H}}^{(0)}_{F}=\sum_{j=1}^{N}\mathcal{H}^{(j)}\approx\sum_{j<k}d_{jk}^{\textrm{CC}}\left(\frac{3}{2}\mathcal{H}_{\textrm{ff}}-\vec{I_{j}}\cdot\vec{I_{k}}\right),$
(1)

with the flip-flop Hamiltonian,
$\mathcal{H}_{\textrm{ff}}=I_{jz}I_{kz}+I_{jy}I_{ky}$ [48]. The
$\mathcal{H}_{z}$ dephasing fields are filtered out in
${\mathcal{H}}^{(0)}_{F}$. For sufficiently small $\zeta$, Eq. (1) holds
irrespective of the flip-angle $\theta$, except for certain special values
($\theta\approx\pi,2\pi$). We note that this constitutes a key difference with
respect to conventional dynamical decoupling control (CPMG [49]), wherein the
interspin couplings are retained and result in rapid ${}^{13}\textrm{C}$ decay
[48]. The higher order terms in the Magnus expansion are progressively
smaller, but contribute to long time system dynamics [46, 50]. Importantly,
the initial transverse magnetized state $\rho_{I}$ is a conserved quantity
under ${\mathcal{H}}^{(0)}_{F}$, since
$[\rho_{I}{,}{\mathcal{H}}^{(0)}_{F}]{=}0$. This leads to prethermal lifetimes
that depend exponentially on the drive frequency $\omega$. Ultimately, the
divergence of the expansion manifests in the system heating to infinite
temperature.

Fig. 2C shows the measured survival probability $F(N\tau)$ of the state
$\rho_{I}$ under the applied Floquet drive. This can be expressed as,
$F(N\tau)=\frac{1}{2}\textrm{Tr}\left\\{{\rho_{I}U(N\tau)^{\dagger}\rho_{I}U(N\tau)}\right\\}$.
We have neglected the first 100ms here for clarity (see Fig. 3A for full
data). Data shows significant extension in the transverse state lifetimes.
Points in Fig. 2C are the experimental data while the line is a fit to a sum
of five exponentials (zoomed in Fig. 2C(ii)); the high measurement SNR is
evident in the zoomed data. The product $J\tau$ is a convenient metric to
label the Floquet regime of operation, and in these measurements
$J\tau$=0.066. The $\theta{\approx}\pi/2$ pulses here are applied every
$\tau{\approx}100\mu$s, and the 573s period encapsulates ${\approx}$5.8M
pulses. For comparison, the conventional ${}^{13}\textrm{C}$ free induction
decay [51] in the absence of Floquet driving is shown in Fig. 2A, where decay
occurs in $T_{2}^{\ast}{\approx}$1.5ms on account of internuclear couplings
and static field disorder. High SNR and continuous weak measurement readout
allows us to recognize (see Fig. 3B) a dynamic change in the decay rate
constant along the curve, making it difficult to quantify the decay rate by a
single number. The data especially past 100ms is found to fit well to the
stretched exponential ${\sim}\exp\left[-(t/T_{2}’)^{1/2}\right]$, from where
we extract $T_{2}’{\approx}$353s. Alternatively, using a 1/$e$\- intersection
(dashed line in Fig. 2C) as a convenient proxy yields, $T_{2}’{=}90.9$s. The
extension leads to substantial line-narrowing of the ${}^{13}\textrm{C}$ NMR
spectrum (${\sim}28$mHz in Fig. 1C).

The measurement procedure for Fig. 2C is detailed in the Supplementary
Information [39]. The signal is sampled every 1ns in $t_{\textrm{acq}}$
windows between the pulses (see Fig. 2B). Such continuous readout (akin to
weak measurement [52]) yields significant SNR advantages over point-by-point
stroboscopic measurements. Rapid data sampling throughput (at
$f_{s}{=}\tau^{-1}$) also allows further filtering to be applied when the
dynamics are slow compared to $f_{s}$. With this, we obtain a single-shot SNR
${>}10^{3}$ per measurement point, and ${\approx}4\times 10^{9}$ for the
integrated signal (see Fig. 1C).

Fig. 5: Transient approach to prethermal plateau. (A) Oscillations in the
approach to prethermal plateau seen for data zooming in on region I, in a 1s
long window (see Fig. 3A). Data (points) corresponds to
$\theta{\approx}\\{\pi/2,\pi/4\\}$ respectively. Solid line is data with
moving average filtering applied over the entire region (see Fig. 3B). (B)
Zoom in to region I shows the transient approach with high SNR. It is evident
that the oscillations are at higher frequency for $\theta{\approx}\pi/2$.
Solid line is a spline fit to guide the eye. (C) Fourier transforms of panels
in B allows identification of the frequency components constituting the
oscillations as a function of $\omega{=}\tau^{-1}$. Harmonics are represented
by numbers. It is clear that primary oscillation frequency is higher for
$\theta{\approx}\pi/2$, where we extract the primary harmonic position at
${\approx}0.26\tau^{-1}$. (D) Variation with flip angle $\theta$. Data shows
the position of the oscillation frequency for the primary and higher harmonics
(numbered). See full data at Ref. [53]. Solid lines are linear fits, while
dashed line is an extrapolation. Slopes are in the ratio expected.

Floquet Prethermalization – To better illustrate thermalization dynamics of
the spins, Fig. 3A shows the full data on a logarithmic time scale. The FID is
also shown, and lifetime extension is evident from the shift in the curves.
Points are experimental data with no moving average applied, and the solid and
dashed lines are stretched exponential fits. We identify distinct, albeit
smoothly transitioning, regimes in the thermalization process (shaded in Fig.
3A). Following Ref. [2], we refer to them as: (I) an initial regime of
constrained thermalization ($0{<}t{<}20$ms), where we observe oscillatory
behavior with a harmonic frequency response of the Floquet drive frequency
$\omega$, (II) the prethermal plateau, leading into (III) unconstrained
thermalization towards the (IV) infinite temperature state (not reached in
these experiments).

Let us first focus our attention to the dynamics in regimes II and III. Fig.
3B-C shows two complementary visualizations after moving average filter is
applied over the entire data. Fig. 3B, plotted on a semi-log scale, makes
evident that the decay rate constant changes over the entire thermalization
period. The high SNR and rapid sampling rate, however, allows us to unravel
the exact rate change behavior in a manner not accessible in previous
experiments. It is easiest seen when re-plotted against $\sqrt{t}$ in Fig. 3C,
where we obtain an approximately linear trend (dashed line) over a long period
(${\sim}$500s). The prethermal dynamics is therefore ${\sim}\exp(-t^{\alpha})$
with exponent $\alpha{\approx}1/2$. Decades-old NMR experiments had observed a
similar trend in paramagnetic impurity rich solids [54, 55]. We emphasize
however the high SNR of the data in Fig. 3, proffering insights into, and
deviations from, this behavior. At higher $J\tau$ values, for instance, we
observe a dynamic decrease in $\alpha$ away from 1/2 in regime III (movie
available at Ref. [40]). The turning point (cusp) in data in Fig. 3C, obtained
after moving average filtering over the oscillations in regime I, also allows
a convenient means to quantify the exact point of transition to prethermal
plateau. The length of this period ($\approx$10-20ms) closely mirrors the
period over which the FID completely decays (see Fig. 3A).

To study the scaling of the prethermal lifetimes with the frequency of the
Floquet drive $\omega$, Fig. 4A shows similar data at a range of $J\tau$
values. This is carried out by varying the inter-pulse spacing $\tau$ in Fig.
2B. The full dataset (shown in Supplementary Information) consists of
measurements at 57 such $J\tau$ values, but we show a restricted set here for
clarity. Again, there is a high density of data points in each experimental
line. To restrict attention to regions II-III, we normalize the data at the
transition points to the prethermal plateau, identified from the cusps as in
Fig. 3C. The data show thermalization proceeding more slowly for lower values
of $J\tau$. The dynamic change of rate coefficient makes plotting a single
graph that encapsulates the full long-time behavior difficult. Instead, we
extract the decay rates focusing on regime II, where decay (similar to Fig.
3C) follows an exponent $\alpha{\approx}1/2$.

This is presented in two complementary viewpoints in Fig. 4B-C. First, in Fig.
4B plotted on a semi-log scale with respect to the drive period $\tau$, we see
a linear trend in the decay rates, especially at high $\tau$ (dashed line).
This points to an approximately exponential scaling of the state preservation
lifetimes with drive frequency, one of the signatures of Floquet
prethermalization. At low $\tau$ however, we observe a flatter slope with
sharp features in the decay rates. Fig. 4C shows an alternate view instead in
terms of $\omega$. Extracting the transverse state lifetimes $T_{2}’$ on the
log-log plot, we find a slope of $2.1\pm 0.1$ at low-frequency suggesting a
Fermi’s Golden Rule scaling with drive frequency [56].

The sharp peaks in the decay rates in the high $\omega$ regime in Fig. 4B-C
are intriguing. We believe this is a manifestation of quantum sensing — the
${}^{13}\textrm{C}$ nuclei see an enhanced decay rate when subjected to
environmental magnetic fields at a fixed frequency $f_{\textrm{ac}}$ matched
in periodicity (resonant) with the pulse sequence, at
$f_{\textrm{ac}}{=}\theta/(2\pi\tau)$. The first two peaks are observed at
$f_{\textrm{ac}}{\approx}2.5$kHz and $f_{\textrm{ac}}{\approx}5.0$kHz. This is
possible because the pulsed spin-lock sequence exhibits dynamical decoupling
properties similar to quantum sensing protocols [31]. The exact origin of
these fields in Fig. 4B-C are unclear and beyond the scope of the current
manuscript. A more detailed exposition on exploiting Floquet prethermal states
for quantum sensing will be presented elsewhere.

Approach to prethermal plateau – Finally, let us elucidate how the nuclear
spins approach the Floquet prethermal plateau [57], focusing attention on
regime I of Fig. 3A. We observe transients in the survival probability leading
into the plateau; this is shown for two choices of the flip-angle $\theta$ in
Fig. 5A ($\theta{\approx}\pi/2$ and $\theta{\approx}\pi/4$) respectively. High
SNR allows us to track the oscillatory dynamics after every pulse, providing a
window into how the approximately time-independent Hamiltonian is established.
Moreover, the prethermal plateau level is itself dependent on $\theta$.

The transients last for $t{\approx}10$ms, which is approximately the total
lifetime for the original FID, and is of the order of magnitude of
$\|\mathcal{H}_{dd}\|^{-1}$ (see Fig. 3A). As Fig. 5B indicates, the
oscillation periodicity is closely related to the flip angle employed; for
$\theta{\approx}\pi/2$, for instance, the oscillations occur at a fourth of
the frequency of the Floquet drive $\omega$. To see this more clearly, Fig. 5C
shows the respective Fourier transforms in a 10ms region. Plotted against
$\omega$, we identify harmonics of the oscillatory dynamics (numbers). For
$\theta{\approx}\pi/4$ (lower panels in Fig. 5B-C), we recognize a primary
harmonic and higher harmonics at ${\approx}n\omega/8$, where $n$ is an
integer.

Intuitively, this characteristic periodicity can be thought of as arising from
the number of pulses $N_{k}$ required to return the Floquet unitary to a prior
configuration; i.e. such that the toggling frame Hamiltonian after $2N_{k}$
pulses is equivalent to that after $N_{k}$,
$\mathcal{H}^{(2N_{k})}{=}\mathcal{H}^{(N_{k})}$. This corresponds to
effectively completing a $2\pi$ rotation of the Hamiltonian in the toggling
frame. Four pulses are therefore needed for $\theta{=}\pi/2$ in Fig. 5A. In
general, the primary harmonic frequency is expected to be at frequency
$f{=}\theta/(2\pi\tau)$. Experiments confirm this picture; we extract the
oscillation frequencies in regime I as a function of $\theta$, and they fall
neatly onto three straight lines for the three harmonics (see Fig. 5D). We
hypothesize that the higher harmonics arise from bilinear and trilinear terms
in the density matrix produced by dipolar evolution. The experimentally
measured slopes are in the ratio $1{:}1.98{:}2.93$, close to the $1{:}2{:}3$
pattern expected.

In conclusion, we have observed Floquet prethermalization of dipolar-coupled
nuclear spins in a bulk solid at room temperature. The observed ${>}$90s-long
prethermal lifetimes in diamond ${}^{13}\textrm{C}$ nuclei are over four
orders of magnitude longer than free induction decay times, and significantly
longer than in other systems. Our measurements unveil regimes of
thermalization with a degree of clarity not accessible in previous NMR
studies. Apart from fundamental insights, our work points to attractive
opportunities possible via Floquet control in hyperpolarizable, dilute and
low-$\gamma_{n}$ nuclear networks. Protection and continuous interrogation of
spins along a Bloch transverse axis for ${\sim}$10min periods opens avenues
for high-sensitivity magnetometers, gyroscopes [58, 59], and spin sensors [60]
constructed out of hyperpolarized prethermal ${}^{13}\textrm{C}$ nuclei.

We gratefully acknowledge M. Markham (Element6) for the diamond sample used in
this work, and discussions with S. Bhave, M. Bukov, C. Fleckenstein, C.
Meriles, J. Reimer, D. Sakellariou, and A. Souza. This work was funded by ONR
under contract N00014-20-1-2806. BG was supported by DOE BES CSGB under
contract DE-AC02-05CH11231.

## References

  * Santos [2021] L. F. Santos, The quick drive to pseudo-equilibrium, Nature Physics , 1 (2021).
  * D’Alessio and Rigol [2014] L. D’Alessio and M. Rigol, Long-time behavior of isolated periodically driven interacting lattice systems, Physical Review X 4, 041048 (2014).
  * Goldman and Dalibard [2014] N. Goldman and J. Dalibard, Periodically driven quantum systems: effective hamiltonians and engineered gauge fields, Physical review X 4, 031027 (2014).
  * Bukov  _et al._ [2015a] M. Bukov, L. D’Alessio, and A. Polkovnikov, Universal high-frequency behavior of periodically driven systems: from dynamical stabilization to floquet engineering, Advances in Physics 64, 139 (2015a).
  * Abanin  _et al._ [2015] D. A. Abanin, W. De Roeck, and F. Huveneers, Exponentially slow heating in periodically driven many-body systems, Physical review letters 115, 256803 (2015).
  * Lazarides  _et al._ [2014] A. Lazarides, A. Das, and R. Moessner, Equilibrium states of generic quantum systems subject to periodic driving, Physical Review E 90, 012110 (2014).
  * Kuwahara  _et al._ [2016] T. Kuwahara, T. Mori, and K. Saito, Floquet–magnus theory and generic transient dynamics in periodically driven many-body quantum systems, Annals of Physics 367, 96 (2016).
  * Bukov  _et al._ [2015b] M. Bukov, S. Gopalakrishnan, M. Knap, and E. Demler, Prethermal floquet steady states and instabilities in the periodically driven, weakly interacting bose-hubbard model, Physical review letters 115, 205301 (2015b).
  * Abanin  _et al._ [2017] D. A. Abanin, W. De Roeck, W. W. Ho, and F. Huveneers, Effective hamiltonians, prethermalization, and slow energy absorption in periodically driven many-body systems, Physical Review B 95, 014112 (2017).
  * Weidinger and Knap [2017] S. A. Weidinger and M. Knap, Floquet prethermalization and regimes of heating in a periodically driven, interacting quantum system, Scientific reports 7, 1 (2017).
  * Luitz  _et al._ [2020] D. J. Luitz, R. Moessner, S. Sondhi, and V. Khemani, Prethermalization without temperature, Physical Review X 10, 021046 (2020).
  * Singh  _et al._ [2019] K. Singh, C. J. Fujiwara, Z. A. Geiger, E. Q. Simmons, M. Lipatov, A. Cao, P. Dotti, S. V. Rajagopal, R. Senaratne, T. Shimasaki, M. Heyl, A. Eckardt, and D. M. Weld, Quantifying and controlling prethermal nonergodicity in interacting floquet matter, Phys. Rev. X 9, 041021 (2019).
  * Else and Nayak [2016] D. V. Else and C. Nayak, Classification of topological phases in periodically driven interacting systems, Physical Review B 93, 201103 (2016).
  * Khemani  _et al._ [2016] V. Khemani, A. Lazarides, R. Moessner, and S. L. Sondhi, Phase structure of driven quantum systems, Physical review letters 116, 250401 (2016).
  * Zhao  _et al._ [2021] H. Zhao, F. Mintert, R. Moessner, and J. Knolle, Random multipolar driving: Tunably slow heating through spectral engineering, Phys. Rev. Lett. 126, 040601 (2021).
  * Howell  _et al._ [2019] O. Howell, P. Weinberg, D. Sels, A. Polkovnikov, and M. Bukov, Asymptotic prethermalization in periodically driven classical spin chains, Physical review letters 122, 010602 (2019).
  * Rubio-Abadal  _et al._ [2020] A. Rubio-Abadal, M. Ippoliti, S. Hollerith, D. Wei, J. Rui, S. Sondhi, V. Khemani, C. Gross, and I. Bloch, Floquet prethermalization in a bose-hubbard system, Physical Review X 10, 021044 (2020).
  * Viebahn  _et al._ [2021] K. Viebahn, J. Minguzzi, K. Sandholzer, A.-S. Walter, M. Sajnani, F. Görg, and T. Esslinger, Suppressing dissipation in a floquet-hubbard system, Physical Review X 11, 011057 (2021).
  * Ueda [2020] M. Ueda, Quantum equilibration, thermalization and prethermalization in ultracold atoms, Nature Reviews Physics , 1 (2020).
  * Peng  _et al._ [2021] P. Peng, C. Yin, X. Huang, C. Ramanathan, and P. Cappellaro, Floquet prethermalization in dipolar spin chains, Nature Physics , 1 (2021).
  * Yin  _et al._ [2021] C. Yin, P. Peng, X. Huang, C. Ramanathan, P. Cappellaro, _et al._ , Prethermal quasiconserved observables in floquet quantum systems, Physical Review B 103, 054305 (2021).
  * Rovny  _et al._ [2018] J. Rovny, R. L. Blum, and S. E. Barrett, Observation of discrete-time-crystal signatures in an ordered dipolar many-body system, Physical review letters 120, 180603 (2018).
  * Maricq [1987] M. M. Maricq, Spin thermodynamics of periodically time-dependent systems: The quasistationary state and its decay, Physical Review B 36, 516 (1987).
  * Maricq [1990] M. M. Maricq, Long-time limitations of the average hamiltonian theory: A dressed-states viewpoint, in  _Advances in Magnetic Resonance: The Waugh Symposium_ (Academic Press, 1990) pp. 151–182.
  * Sakellariou  _et al._ [1998] D. Sakellariou, P. Hodgkinson, and L. Emsley, Quasi equilibria in solid-state nmr, Chem. Phys. Lett. 293, 110 (1998).
  * Sakellariou  _et al._ [1999] D. Sakellariou, P. Hodgkinson, S. Hediger, and L. Emsley, Experimental observation of periodic quasi-equilibria in solid-state nmr, Chem. Phys. Lett. 308, 381 (1999).
  * Waugh [1998] J. b. Waugh, Equilibrium and ergodicity in small spin systems, Molecular Physics 95, 731 (1998).
  * Bruschweiler and Ernst [1997] R. Bruschweiler and R. Ernst, Non-ergodic quasi-equilibria in short linear spin 12 chains, Chem. Phys. Lett. 264, 393 (1997).
  * Ladd  _et al._ [2005] T. D. Ladd, D. Maryenko, Y. Yamamoto, E. Abe, and K. M. Itoh, Coherence time of decoupled nuclear spins in silicon, Phys. Rev. B 71, 014401 (2005).
  * Dong  _et al._ [2008a] Y. Dong, R. Ramos, D. Li, and S. Barrett, Controlling coherence using the internal structure of hard $\pi$ pulses, Phys. Rev. Lett. 100, 247601 (2008a).
  * Degen  _et al._ [2017] C. L. Degen, F. Reinhard, and P. Cappellaro, Quantum sensing, Reviews of modern physics 89, 035002 (2017).
  * Fleckenstein and Bukov [2021a] C. Fleckenstein and M. Bukov, Thermalization and prethermalization in periodically kicked quantum spin chains, Phys. Rev. B 103, 144307 (2021a).
  * Reynhardt and Terblanche [1997] E. Reynhardt and C. Terblanche, 13c relaxation in natural diamond, Chemical physics letters 269, 464 (1997).
  * Ajoy  _et al._ [2019] A. Ajoy, B. Safvati, R. Nazaryan, J. Oon, B. Han, P. Raghavan, R. Nirodi, A. Aguilar, K. Liu, X. Cai, _et al._ , Hyperpolarized relaxometry based nuclear t 1 noise spectroscopy in diamond, Nature communications 10, 1 (2019).
  * Dong  _et al._ [2008b] Y. Dong, R. Ramos, D. Li, and S. Barrett, Controlling coherence using the internal structure of hard $\pi$ pulses, Physical review letters 100, 247601 (2008b).
  * Hoult [1978] D. Hoult, The nmr receiver: a description and analysis of design, Progress in Nuclear Magnetic Resonance Spectroscopy 12, 41 (1978).
  * Ajoy  _et al._ [2018a] A. Ajoy, K. Liu, R. Nazaryan, X. Lv, P. R. Zangara, B. Safvati, G. Wang, D. Arnold, G. Li, A. Lin, _et al._ , Orientation-independent room temperature optical 13c hyperpolarization in powdered diamond, Sci. Adv. 4, eaar5492 (2018a).
  * Ajoy  _et al._ [2018b] A. Ajoy, R. Nazaryan, K. Liu, X. Lv, B. Safvati, G. Wang, E. Druga, J. Reimer, D. Suter, C. Ramanathan, _et al._ , Enhanced dynamic nuclear polarization via swept microwave frequency combs, Proceedings of the National Academy of Sciences 115, 10576 (2018b).
  * [39] See supplementary online material.
  * pre [2021a] Video showing full dataset of Fig. 4: https://www.youtube.com/watch?v=uLKIR_XM_FQ (2021a).
  * Ostroff and Waugh [1966] E. Ostroff and J. Waugh, Multiple spin echoes and spin locking in solids, Physical Review Letters 16, 1097 (1966).
  * Rhim  _et al._ [1976] W.-K. Rhim, D. Burum, and D. Elleman, Multiple-pulse spin locking in dipolar solids, Physical Review Letters 37, 1764 (1976).
  * Rhim  _et al._ [1978] W.-K. Rhim, D. Burum, and D. Elleman, Calculation of spin–lattice relaxation during pulsed spin locking in solids, The Journal of Chemical Physics 68, 692 (1978).
  * Haeberlen [1976] U. Haeberlen,  _High Resolution NMR in Solids: Selective Averaging_ (Academic Press Inc., New York, 1976).
  * Magnus [1954] W. Magnus, On the exponential solution of differential equations for a linear operator, Communications on Pure and Applied Mathematics 7, 649 (1954).
  * Wilcox [1967] R. M. Wilcox, Exponential operators and parameter differentiation in quantum physics, Journal of Mathematical Physics 8, 962 (1967).
  * Blanes  _et al._ [2009] S. Blanes, F. Casas, J. Oteo, and J. Ros, The magnus expansion and some of its applications, Physics Reports 470, 151 (2009).
  * Ajoy  _et al._ [2020] A. Ajoy, R. Nirodi, A. Sarkar, P. Reshetikhin, E. Druga, A. Akkiraju, M. McAllister, G. Maineri, S. Le, A. Lin, _et al._ , Dynamical decoupling in interacting systems: applications to signal-enhanced hyperpolarized readout, arXiv preprint arXiv:2008.08323 (2020).
  * Carr and Purcell [1954] H. Y. Carr and E. M. Purcell, Effects of diffusion on free precession in nuclear magnetic resonance experiments, Phys. Rev. 94, 630 (1954).
  * Ernst  _et al._ [1987] R. Ernst, G. Bodenhausen, and A. Wokaun,  _Principles of nuclear magnetic resonance in one and two dimensions_ (Clarendon Press Oxford, 1987).
  * Lowe [1959] I. Lowe, Free induction decays of rotating solids, Physical Review Letters 2, 285 (1959).
  * Pfender  _et al._ [2019] M. Pfender, P. Wang, H. Sumiya, S. Onoda, W. Yang, D. B. R. Dasari, P. Neumann, X.-Y. Pan, J. Isoya, R.-B. Liu, _et al._ , High-resolution spectroscopy of single nuclear spins via sequential weak measurements, Nature communications 10, 1 (2019).
  * pre [2021b] Video showing full dataset of Fig. 5: https://www.youtube.com/watch?v=8NI7Zzugi4o (2021b).
  * Tse and Hartmann [1968] D. Tse and S. Hartmann, Nuclear spin-lattice relaxation via paramagnetic centers without spin diffusion, Physical Review Letters 21, 511 (1968).
  * Lin and Hartmann [1973] N.-a. Lin and S. Hartmann, Nuclear spin-lattice relaxation in ca f 2 via paramagnetic centers for short correlation time when spin diffusion is inhibited, Physical Review B 8, 4079 (1973).
  * Fleckenstein and Bukov [2021b] C. Fleckenstein and M. Bukov, Prethermalization and thermalization in periodically driven many-body systems away from the high-frequency limit, Phys. Rev. B 103, L140302 (2021b).
  * Haldar  _et al._ [2018] A. Haldar, R. Moessner, and A. Das, Onset of floquet thermalization, Physical Review B 97, 245122 (2018).
  * Ajoy and Cappellaro [2012] A. Ajoy and P. Cappellaro, Stable three-axis nuclear-spin gyroscope in diamond, Phys. Rev. A 86, 062104 (2012).
  * Ledbetter  _et al._ [2012] M. Ledbetter, K. Jensen, R. Fischer, A. Jarmola, and D. Budker, Gyroscopes based on nitrogen-vacancy centers in diamond, Physical Review A 86, 052116 (2012).
  * Abobeih  _et al._ [2019] M. Abobeih, J. Randall, C. Bradley, H. Bartling, M. Bakker, M. Degen, M. Markham, D. Twitchen, and T. Taminiau, Atomic-scale imaging of a 27-nuclear-spin cluster using a quantum sensor, Nature 576, 411 (2019).

Supplementary Information
Floquet prethermalization with lifetime exceeding 90s in a bulk hyperpolarized
solid
William Beatrez,1 Otto Janes,1 Amala Akkiraju,1 Arjun Pillai,1 Alexander
Oddo,1 Paul Reshetikhin,1

Emanuel Druga,1 Maxwell McAllister,1 Mark Elo,2 Benjamin Gilbert,3 Dieter
Suter,4 and Ashok Ajoy,1,5,∗

_1 Department of Chemistry, University of California, Berkeley, Berkeley, CA
94720, USA._ _2 Tabor Electronics Inc. Hatasia 9, Nesher, 3660301, Israel._ _3
Energy Geoscience Division, Lawrence Berkeley National Laboratory, Berkeley,
CA 94720, USA._ _4 Fakultät Physik, Technische Universität Dortmund, D-44221
Dortmund, Germany._ _5 Chemical Science Division, Lawrence Berkeley National
Laboratory, University of California, Berkeley, Berkeley, CA 94720, USA._

Fig. S1: Data processing chain. (A) Raw data of ${}^{13}\textrm{C}$ nuclear
precession measured inductively, here heterodyned from 75MHz (Larmor
frequency) to 20MHz. The window shown is a 150ns part of the larger
acquisition window. (B) Raw data corresponding to one complete acquisition
period between the pulses, here $t_{\textrm{acq}}{=}32\mu$s. (C) Fourier
transformation reveals characteristic peaks at the heterodyning frequency
${\pm}20$MHz. This amplitude forms the primary data that is plotted in the
main paper. We therefore obtain one data point per acquisition window, and in
Fig. 2C a total of ${\approx}$5.8M data points.

##  I Data Processing

We now present details of the data processing employed in this manuscript.
Fig. S1 describes the chain of steps involved in obtaining decay curves such
as Fig. 2C of the main paper. We readout the NMR signal continuously in
$t_{\textrm{acq}}$ periods between the pulses, and the pulses are spaced apart
by $\tau{=}100\mu$s. A representative such acquisition window is shown in Fig.
S1B, in this case $t_{\textrm{acq}}{=}32\mu$s. The data here (taken 1s into
the decay) is sampled at 1Gs/s ($\Delta t$=1ns). A zoom in (Fig. S1A) reveals
high SNR oscillations corresponding to the precession of the hyperpolarized
nuclei; the frequency here is 20MHz (heterodyned from the 75MHz Larmor
frequency). For each such window, we take a Fourier transform (Fig. S1C), and
extract the 20MHz peak. This corresponds effectively to digital bandpass
filtering with a filter linewidth of ${\sim}t_{\textrm{acq}}^{-1}$. Each such
point is then plotted to create the decay curves in Fig. 2C, Fig. 3 and Fig.
4. Since the measurements are carried out after every pulse, we obtain a data
point in Fig. S1D every $\tau{=}100\mu$s. Over the 573s decay period, this
corresponds to ${\approx}5.8$ million measurement points. However, the data
itself is slowly varying (except in regime I), and can be thought of as being
effectively oversampled by the measurement points. Moving average filtering
thus increases SNR further, acting as a low-pass filter to suppress higher
frequency variations. We typically employ a moving average filter size of
0.1s.

Fig. S2: Signal dependence on flip angle $\theta$. Panel shows the net signal
obtained upon application of a train of ${\theta}$-pulses following the
initial $\pi/2$ pulse. We identify clear signal dips at
$\theta{\approx}\\{\pi,2\pi\\}$ corresponding to rapid decay due to evolution
under the dipolar Hamiltonian (see [48]). In these experiments
$t_{\textrm{acq}}{=}32\mu$s and pulse spacing $\tau{=}100\mu$s.  Fig. S3: Raw
data corresponding to Fig. 4 of the main paper. Movie (see at YouTube
here:[40]) shows signal plotted on a semi-log scale against$\sqrt{t}$. Data
are red points, while the blue line is a fit taken in the region where
$\alpha{\approx}1/2$. The extracted rates are plotted as points in the lower
panels of Fig. 4 of the main paper. Fig. S4: Raw data corresponding to Fig. 5
of the main paper. Movie (see at YouTube here:[53]) shows frames corresponding
to the transient approach to prethermal plateau for different flip angles
$\theta$. Panels show the transient approach and Fourier transform of the
oscillations showing characteristic frequencies.

##  II Materials and Methods

The sample used in these experiments consists of a CVD fabricated single
crystal of diamond with ${\sim}$1ppm of NV centers. The sample is placed flat,
i.e. with its [100] face pointing parallel to the hyperpolarization and
interrogation magnetic fields (36mT and 7T respectively). In this
configuration, the internuclear vector between ${}^{13}\textrm{C}$ nuclei at
NN sites on the lattice are positioned at the magic angle, and hence are
suppressed.

For hyperpolarization, we employ continuous optical pumping and swept
microwave irradiation for ${\sim}$40s through a technique described
previously. Hyperpolarization is carried out at low field, the sample is
shuttled to high field, and the Floquet sequence in Fig. 2B is then applied.
NV-${}^{13}\textrm{C}$ polarization transfer occurs via biased Landau-Zener
traversals in the rotating frame; spin diffusion serves to transfer
polarization to bulk ${}^{13}\textrm{C}$ nuclei in the diamond lattice.

Fig. S2 shows the variation of the integrated signal as a function of the flip
angle $\theta$ employed in the pulse sequence. We refer the reader to Ref.
[48] for a more detailed exposition of the observed trend. For experiments
Fig. 2 and Fig. 3 of this paper, we employ a pulse duty cycle of $\sim$50%,
where the measured SNR is highest.

The figure movie Fig. S3 (accessible in Ref. [40]) shows the full dataset
corresponding to Fig. 4 of the main paper. Similar to Fig. 4B, we plot the
data against $\sqrt{t}$ in a semi-log axis. Here the value $J\tau$ is varied
by altering the spacing between the pulses in Fig. 4B. The blue straight lines
in the movie show the fit to $\alpha{=}$1/2 region. These decay rates,
corresponding to the slope of the blue lines in Ref. [40], are plotted in the
lower panels of Fig. 4.

Similarly, the figure movie Fig. S4 (accessible in Ref. [53]) shows the full
dataset corresponding to Fig. 5 of the main paper, describing the approach to
the Floquet prethermal plateau for different values of the flip angle
$\theta$.


University of Florence, Italy and https://www.math.unifi.it/~maggesi/
marco.maggesi@unifi.ithttps://orcid.org/0000-0003-4380-7691Supported by the
Italian Ministry of University and Research and by INdAM-GNSAGA University of
Genoa, Italy and
https://logicosimo.gitlab.ioperinibrogi@dima.unige.ithttps://orcid.org/0000-0001-7883-5727
John Q. Public and Joan R. Public [500]Theory of computation Higher order
logic [500]Theory of computation Modal and temporal logics [300]Theory of
computation Automated reasoning The implementation described in this paper is
hosted in the subdirectory GL of the distribution of HOL Light theorem prover.
[swhid=swh:1:dir:288139a46b5250ca678d928a823173f4f69c8594]HOL Light source
code, Jenuary 2021 https://github.com/jrh13/hol-light/ John Q. Open and Joan
R. Access 2 42nd Conference on Very Important Topics (CVIT 2016) CVIT 2016
CVIT 2016 December 24–27, 2016 Little Whinging, United Kingdom 42 23

# A formal proof of modal completeness for provability logic

Marco Maggesi  Cosimo Perini Brogi

###### Abstract

This work presents a formalized proof of modal completeness for Gödel-Löb
provability logic (GL) in the HOL Light theorem prover. We describe the code
we developed, and discuss some details of our implementation, focusing on our
choices in structuring proofs which make essential use of the tools of HOL
Light and which differ in part from the standard strategies found in main
textbooks covering the topic in an informal setting. Moreover, we propose a
reflection on our own experience in using this specific theorem prover for
this formalization task, with an analysis of pros and cons of reasoning
_within_ and _about_ the formal system for GL we implemented in our code.

###### keywords:

Provability Logic, Higher-Order Logic, Mechanized Mathematics, HOL Light
Theorem Prover

## Introduction

In this paper we wish to report on our results and general experience in using
HOL Light theorem prover to formally verify some properties of Gödel-Löb
provability logic (GL).

Our work starts with a deep embedding of the syntax of propositional modal
logic together with the corresponding relational semantics. Next, we introduce
the traditional axiomatic calculus $\mathbb{GL}$ and prove the validity of the
system w.r.t. irreflexive transitive finite frames.

After doing that, the most interesting part of our work begins with the proof
of a number of lemmas _in_ $\mathbb{GL}$ that are necessary for our main goal,
namely the development of a formal proof of modal completeness for the system.

In order to achieve that, we had to formally verify a series of preliminary
lemmas and constructions involving the behaviour of syntactical objects used
in the standard proof of the completeness theorem. These unavoidable steps are
very often only proof-sketched in wide-adopted textbooks in logic, for they
mainly involve “standard” reasoning _within_ the proof system we are dealing
with. But when we are working in a formal setting like we did with HOL Light,
experience reveals that it is generally more convenient to adopt a different
line of reasoning and to make a smart use of our formal tools, so that we can
succeed in developing alternative (or simpler) proofs, still totally verified
by the computer.

In other terms: in order to give a formal proof of the completeness theorem
for $\mathbb{GL}$, that is

######  Theorem 0.1.

For any formula $A$, $\mathbb{GL}\vdash A$ iff $A$ is true in any irreflexive
transitive frame.

we needed to split down the main goal into several subgoals – dealing with
both the object- and the meta-level – which might seem trivial in informal
reasoning. However, when carefully checked, they revealed unexpected formal
subtleties, which guided us towards different proof-strategies where HOL Light
infrastructure played a more active role.

A more detailed account of these aspects is given in the main body of the
present work, but we can briefly summarise the present paper as follows:

  * •

In Section 1, we introduce the basic ingredients of our development, namely
the formal counterparts of the syntax and relational semantics for provability
logic, along with some lemmas and general definitions which are useful to
handle the implementation of these objects in a uniform way, i.e. without the
restriction to the modal system we are interested in. The formalization
constitutes large part of the file `modal.ml`;

  * •

In Section 2, we formally define the axiomatic calculus $\mathbb{GL}$, and
prove in a neat way the validity lemma for this system. Moreover, we give
formal proofs of several lemmas _in_ $\mathbb{GL}$ ($\mathbb{GL}$-lemmas, for
short), whose majority is in fact common to all normal modal logics, so that
our proofs might be re-used in subsequent implementations of different
systems. This corresponds to contents of our code in `gl.ml`;

  * •

Finally, in Section 3 we introduce all the necessary to give our formal proof
of modal completeness of $\mathbb{GL}$, starting with the definition of
maximal consistent _lists_ of formulae. In order to prove their syntactic
properties – and, in particular, the extension lemma for consistent lists of
formulae to maximal consistent lists – we use the $\mathbb{GL}$-lemmas we have
mentioned in the previous section, and, at the same time, we propose proof-
strategies which highlight the formal tools provided by HOL Light – or, more
informally, which apply more conveniently higher-order reasoning. Therefore,
the proof we are proposing in this section follows the standard lines
presented in e.g. [6] – from extension lemma to modal completeness via truth
lemma – but adopt tools, results, and techniques which are specific to the
theorem prover we used, in line with a clear philosophical attitude in
computer-aided proof development. These results, together with a simple
decision procedure for $\mathbb{GL}$, are gathered in the file
`completeness.ml`.

We care to stress that our formalization does not tweak any original HOL Light
tools, and it is therefore “foundationally safe”. Moreover, since we used just
that original formal infrastructure, our results can be easily translated into
another theorem prover belonging to the HOL family – or, more generally,
endowed with the same automation toolbox.

In any case, our code is integrated into the current HOL Light distribution,
and it is freely available from there.111See ”Supplementary Material” on the
first page of this paper.

Before presenting our results, in the forthcoming subsections of this
introduction we provide the reader with some background material both on
provability logic, and on formal theorem proving in HOL Light: further
information about modalities and HOL Light can be found in [11] and [13],
respectively.

### Developments of Provability Logic

The origins of provability logic date back to a short paper [10] of Gödel’s
where propositions about provability are formalized by means of a unary
operator $\mathtt{B}$ with the aim of giving a classical reading of
intuitionistic logic.

The resulting system corresponds to the logic $\mathbb{S}4$, and the
proposition $\mathtt{B}p$ has to be interpreted as ‘$p$ is _informally_
provable’ – as claimed by Gödel himself. This implies that $\mathbb{S}4$ can
be considered a provability logic lacking an appropriate semantics.

At the same time, that work opened the question of finding an adequate modal
calculus for the formal properties of the provability predicate used in
Gödel’s incompleteness theorems. That problem has been settled since 1970s for
many formal systems of arithmetic by means of Gödel-Löb logic GL.

The corresponding axiomatic calculus $\mathbb{GL}$ consists of the axiomatic
system for classical propositional logic, extended by

  * •

the axiom schema $\mathsf{K}:\Box(A\rightarrow B)\rightarrow\Box
A\rightarrow\Box B$;

  * •

the Löb schema $\mathsf{GL}$: $\Box(\Box A\rightarrow A)\rightarrow\Box A$

  * •

a necessitation rule  $A$ $\Box A$ .

The Löb schema is just a formal version of Löb’s theorem which holds for a
wide class of arithmetical theories satisfying the so-called Hilbert-Bernays-
Löb (HBL) provability conditions.222These properties of the formal predicate
for arithmetical provability were isolated first in [14].

On the semantic side, this calculus is the logic of irreflexive transitive
frames, and, moreover, it can be interpreted arithmetically in a sound and
complete way. In other terms, $\mathbb{GL}$ solves the problem raised by
Gödel’s paper by identifying a propositional formal system for provability in
all arithmetical theories that satisfy the previously mentioned HBL
conditions.

Published in 1976, Solovay’s arithmetical completeness theorem [19] is in this
sense a milestone result in the fields of proof theory and modal logic: for
being arithmetical complete, $\mathbb{GL}$ is capable of capturing and
identifying _all relevant properties of formal provability for arithmetic_ in
a very simple system, which is decidable and neatly characterised.

Such a deep result, however, uses in an essential way the _modal_ completeness
of $\mathbb{GL}$: Solovay’s technique basically consists of an arithmetization
of a relational countermodel for a given formula that is not a theorem of
$\mathbb{GL}$, from which it is possible to define an appropriate arithmetical
formula that is not a theorem of the mathematical system.

In contemporary research, this is still the main strategy to prove
arithmetical completeness for other modalities for provability and related
concepts, in particular for interpretability logic. In spite of this, for many
theories of arithmetic, including Heyting Arithmetic, this technique cannot be
applied, and no alternatives are known.

Therefore, on the one hand, completeness of formal systems w.r.t. the relevant
relational semantics is still an unavoidable step in achieving the more
substantial result of arithmetical completeness; on the other hand, however,
the area of provability logic keeps flourishing and suggesting old and new
open problems, closely related to the field of proof theory, but in fact
bounded also to seeking a uniform proof-strategy to establish adequate
semantics in formal theories of arithmetic having different strengths and
flavours.333The reader is referred to [2] for a survey of open problems in
provability logics. As an instance of relevant applications of this kind of
formal systems to traditional investigations in proof theory see e.g. [1].

### HOL Light Notation

The HOL Light proof assistant [12] is based on _classical_ higher-order logic
with polymorphic type variables and where equality is the only primitive
notion. From a logical viewpoint, the formal engine defined by the _term-
conversions_ and _inference rules_ underlying HOL Light is the same as that
described in [15], extended by an infinity axiom and the classical
characterization of Hilbert’s choice operator. From a practical perspective,
it is a theorem prover privileging a procedural proof style development – i.e.
when using it, we have to solve goals by applying _tactics_ that reduce it to
(eventually) simpler subgoals, so that the interactive aspect of proving is
highlighted. Proof-terms can then be constructed by means of declarations of
labels and of _tacticals_ that compact the proof into few lines of code
evaluated by the machine.

Logical operators – defined in terms of equality – and $\lambda$-abstraction
are denoted by specific symbols in ASCII: for the reader’s sake, we give a
partial glossary to summarise them in the next table. In the third column of
the table, we also report the notations used for the object logic GL
(introduced at the beginning of Section 1.1).

Informal notation | HOL notation | GL notation | Description
---|---|---|---
$\bot$ | `F` | `False` | Falsity
$\top$ | `T` | `True` | Truth
$\neg p$ | `~ p` | `Not p` | Negation
$p\wedge q$ | `/\` | `&&` | Conjunction
$p\vee q$ | `\/` | `||` | Disjunction
$p\Longrightarrow q$ | `==>` | `-->` | Implication
$p\Longleftrightarrow q$ | `<=>` | `<->` | Biconditional
$\Box p$ |  | `Box p` | Modal Operator
$\forall x.\,P(x)$ | `!x. P(x)` |  | Universal quantification
$\exists x.\,P(x)$ | `?x. P(x)` |  | Existential quantification
$\lambda x.\,M(x)$ | `\x. M(x)` |  | Lambda abstraction

In the following sections, we will directly state our results as theorems and
definitions in the HOL Light syntax. Note that theorems are prefixed by the
turnstile symbol, as in `|- 2 + 2 = 4`. We often report a theorem with its
associated name, that is, the name of its associated OCaml constant, e.g.

      ADD_SYM
        |- !m n. m + n = n + m

As expository style, we omit formal proofs at all, but meaning of definitions,
lemmas, and theorems in natural language is clear after the table we have just
given.

We warn the reader that the HOL Light printing mechanism omit type information
completely. However in this paper we manually add type annotations when it
might be useful, or even indispensable, to avoid ambiguity – including the
case of our main results `COMPLETENESS_THEOREM` and
`COMPLETENESS_THEOREM_GEN`.

As already told in the introduction, our contribution is now part of the HOL
Light distribution. The reader interested in performing these results in her
machine – and perhaps build further formalization on top of it – can run our
code with the command

      loadt "GL/make.ml";;

at the HOL Light prompt.

##  1 Basics of Modal Logic

As we stated previously, we deal with a logic that extends classical
propositional reasoning by means of a single modal operator which is intended
to capture the abstract properties of the provability predicate for
arithmetic.

To reason about and within this logic, we have to “teach” HOL Light – our
meta-language – how to identify it, starting with its syntax – the object-
language – and semantics – the interpretation of this very object-language.

We want to keep everything neat and clean from a foundational perspective,
therefore we will define _both_ the object-language and its interpretation
with no relation to the HOL Light environment. In other terms: our formulae
and operators are _real_ syntactic objects which we keep distinct from their
semantic counterpart – and from the logical operators of the theorem prover
too.

###  1.1 Language and Semantics Defined

Let us start by fixing the propositional modal language we will use throughout
the present work. We consider _all_ classical propositional operators –
conjunction, disjunction, implication, equivalence, negation, along with the
0-ary symbols $\top$ and $\bot$ – and we add a modal unary connective $\Box$.
The starting point is, as usual, a denumerable infinite set of propositional
atoms $a_{0},a_{1},\cdots$. Accordingly, formulae of this language will have
one of the following form

$a\;\,|\;\,A\wedge B\,\,|\;\,A\vee B\;\,|\;\,A\rightarrow
B\;\,|\;\,A\leftrightarrow B\;\,|\;\,\neg
A\;\,|\;\,\top\;\,|\;\,\bot\;\,|\;\,\Box A\;\,.$

The following code extends the HOL system with an the inductive type of
formulae up to the atoms – which we identify with the denumerable type of
strings – by using the above connectives:

      let form_INDUCT,form_RECURSION = define_type
        "form = False
              | True
              | Atom string
              | Not form
              | && form form
              | || form form
              | --> form form
              | <-> form form
              | Box form";;

Next, we turn to the semantics for our modal language. We use relational
models – aka Kripke models444See [7] for the historical development of this
notion. – which consist of directed graphs labelled with formulae. More
formally, a Kripke frame is made of a nonempty set ‘of possible worlds’ `W`,
together with a binary relation `R` on `W`. To this, we add a valuation
function `V` which assigns to each atom of our language and each world `w` in
`W` a boolean value. This is extended to a forcing relation holds, defined
recursively on the structure of the input formula `p`, that computes the
truth-value of `p` in a specific world `w`:

      let holds = new_recursive_definition form_RECURSION
        ‘(holds WR V False (w:W) <=> F) /\
       Ψ (holds WR V True w <=> T) /\
       Ψ (holds WR V (Atom s) w <=> V s w) /\
       Ψ (holds WR V (Not p) w <=> ~(holds WR V p w)) /\
       Ψ (holds WR V (p && q) w <=> holds WR V p w /\ holds WR V q w) /\
       Ψ (holds WR V (p || q) w <=> holds WR V p w \/ holds WR V q w) /\
       Ψ (holds WR V (p --> q) w <=> holds WR V p w ==> holds WR V q w) /\
       Ψ (holds WR V (p <-> q) w <=> holds WR V p w <=> holds WR V q w) /\
       Ψ (holds WR V (Box p) w <=> !u. u IN FST WR /\ SND WR w u ==> holds WR V p u)‘;;

Then, the validity of a formula `p` with respect to a frame `(W,R)`, and a
class of frames `L`, denoted respectively `holds_in (W,R) p` and `L |= p`, are

      let holds_in = new_definition
        ‘holds_in (W,R) p <=> !V w. w IN W ==> holds (W,R) V p w‘;;

      let valid = new_definition
        ‘L |= p <=> !f. L f ==> holds_in f p‘;;

The above definitions are already presented in Chapter 20 of Harrison’s HOL
Light Tutorial [13].

###  1.2 Frames for GL

For carrying out our formalization, we are interested in the logic of the
(nonempty) frames whose underlying relation $R$ is transitive and conversely
well-founded – aka Noetherian – on the corresponding set of possible worlds;
in other terms, we want to study the modal tautologies in models based on an
accessibility relation $R$ on $W$ such that

  * •

if $xRy$ and $yRz$, then $xRz$; and

  * •

for no $X\subseteq W$ which is nonempty, there are infinite $R$-chains
$x_{0}Rx_{1}Rx_{2}\cdots$.

In HOL Light, `WF R` states that `R` is a well-founded relation, so that we
express the latter condition as `WF(\x y. R y x)`. Here we see a recurrent
motif in logic: defining a system from the semantic perspective requires non-
trivial tools from the foundational point of view, for, to express the second
condition, a first-order language is not enough. However, that is not an issue
here, since our underlying system is natively higher order:

      let TRANSNT = new_definition
        ‘TRANSNT (W,R) <=>
         ~(W = {}) /\
         (!x y:W. R x y ==> x IN W /\ y IN W) /\
         (!x y z:W. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z) /\
         WF(\x y. R y x)‘;;

From a theoretical point of view, moreover, the question has no deep
consequences as we can characterize this class of frames by using a
_propositional_ language extended by a modal operator $\Box$ that satisfies
the following axiom – usually called _Gödel-Löb axiom schema_ :

$\mathsf{GL}:\quad\Box(\Box A\rightarrow A)\rightarrow\Box A.$

Here is the formal version of our claim:

      LOB_IMP_TRANSNT
        |- !W R. (!x y:W. R x y ==> x IN W /\ y IN W) /\
                 (!p. holds_in (W,R) (Box(Box p --> p) --> Box p))
                 ==> (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z) /\
                     WF (\x y. R y x)

      TRANSNT_IMP_LOB
        |- !W R. (!x y:W. R x y ==> x IN W /\ y IN W) /\
                 (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z) /\
                 WF (\x y. R y x)
                 ==> (!p. holds_in (W,R) (Box(Box p --> p) --> Box p))

      TRANSNT_EQ_LOB
        |- !W R. (!x y:W. R x y ==> x IN W /\ y IN W)
                 ==> ((!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z
                               ==> R x z) /\
                      WF (\x y. R y x) <=>
                      (!p. holds_in (W,R) (Box(Box p --> p) --> Box p)))

Note that the main claim is proven in both its directions by using both a
defined tactic introduced in [13], and the principle of well-founded induction
as implemented in HOL Light.

By using this preliminary result, we could say that the frame property of
being transitive and Noetherian can be captured by Gödel-Löb modal axiom,
without recurring to a higher-order language. Nevertheless, that class of
frames is not particularly informative from a logical point of view: in
particular, we have no information about the cardinality of $W$, so that it
might be possible to find very exotic models for which the axiom holds, with
no real interest yet.

We would like, in fact, to sharpen this result by identifying a smaller class
of frames which is eventually more informative and easier to reason about. To
this aim we note that by definition of Notherianness, our $R$ cannot be
reflexive – otherwise $xRxRx\cdots$ would give us an infinite $R$-chain. This
is not enough: the frames we want to investigate are precisely those whose $W$
is finite, and whose $R$ is both irreflexive and transitive:

      let ITF = new_definition
        ‘ITF (W:W->bool,R:W->W->bool) <=>
         ~(W = {}) /\
         (!x y:W. R x y ==> x IN W /\ y IN W) /\
         FINITE W /\
         (!x. x IN W ==> ~R x x) /\
         (!x y z. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z)‘;;

Now it is easy to see that ITF is a subclass of TRANSNT:

      ITF_NT
        |- !W R:W->W->bool. ITF(W,R) ==> TRANSNT(W,R)

That will be the class of frames whose logic we are now going to define
syntactically.

##  2 Axiomatizing GL

As stated before, we want to identify the logical system generating all the
modal tautologies for transitive Noetherian frames; more precisely, we want to
isolate the _generators_ of the modal tautologies in the subclass of
transitive Noetherian frames which are finite, transitive, and irreflexive.

When dealing with the very notion of tautology – or _theoremhood_ , discarding
the complexity or structural aspects of _derivability_ in a formal system – it
is convenient to focus on axiomatic calculi. The calculus we are dealing with
here is usually denoted by $\mathbb{GL}$.

It is clear from the definition of the forcing relation that for classical
operators any axiomatization of propositional classical logic will do the job.
Here, we adopt a basic system in which only $\rightarrow$ and $\bot$ are
primitive – from the axiomatic perspective – and all the remaining classical
connectives are defined by axiom schemas and by the inference rule of Modus
Ponens imposing their standard behaviour.555This is essentially the calculus
introduced by Wajsberg in 1939, and, independently by Church in 1956.

To this classical engine we add

  * •

the axiom schema $\mathsf{K}$: $\Box(A\rightarrow B)\rightarrow\Box
A\rightarrow\Box B$;

  * •

the axiom schema $\mathsf{GL}$: $\Box(\Box A\rightarrow A)\rightarrow\Box A$;

  * •

the necessitation rule $\mathsf{NR}$:  $A$ ${\mathsf{NR}}$ $\Box A$ ,

where $A,B$ are generic formulae (not simply atoms). Then, here is the
complete definition of the axiom system $\mathbb{GL}$. The set of axioms is
encoded via the inductive predicate `GLaxiom`:

      let GLaxiom_RULES,GLaxiom_INDUCT,GLaxiom_CASES = new_inductive_definition
        ‘(!p q. GLaxiom (p --> (q --> p))) /\
         (!p q r. GLaxiom ((p --> q --> r) --> (p --> q) --> (p --> r))) /\
         (!p. GLaxiom (((p --> False) --> False) --> p)) /\
         (!p q. GLaxiom ((p <-> q) --> p --> q)) /\
         (!p q. GLaxiom ((p <-> q) --> q --> p)) /\
         (!p q. GLaxiom ((p --> q) --> (q --> p) --> (p <-> q))) /\
         GLaxiom (True <-> False --> False) /\
         (!p. GLaxiom (Not p <-> p --> False)) /\
         (!p q. GLaxiom (p && q <-> (p --> q --> False) --> False)) /\
         (!p q. GLaxiom (p || q <-> Not(Not p && Not q))) /\
         (!p q. GLaxiom (Box (p --> q) --> Box p --> Box q)) /\
         (!p. GLaxiom (Box (Box p --> p) --> Box p))‘;;

The judgment $\mathbb{GL}\vdash A$, denoted `|-- A` in the machine code, is
also inductively defined in the expected way:

      let GLproves_RULES,GLproves_INDUCT,GLproves_CASES = new_inductive_definition
        ‘(!p. GLaxiom p ==> |-- p) /\
         (!p q. |-- (p --> q) /\ |-- p ==> |-- q) /\
         (!p. |-- p ==> |-- (Box p))‘;;

###  2.1 $\mathbb{GL}$-lemmas

As usual, $\mathbb{GL}\vdash A$ denotes the existence of a derivation of $A$
from the axioms of $\mathbb{GL}$; we could also define a notion of
derivability from a set of assumptions just by tweaking the previous
definitions in order to handle the specific limitations on $\mathsf{NR}$ – so
that the deduction theorem would hold [8] – but this would be inessential to
our intents.

What matters for the subsequent development is to derive further
$\mathbb{GL}$-lemmas with the help of the automation in HOL Light. In
accordance with this aim, we denoted the classical axioms and rules of the
system as the propositional schemas used by Harrison in the file
`Arithmetic/derived.ml` of the HOL Light standard distribution [12] – where,
in fact, many of our lemmas relying on the propositional calculus only are
already proven there w.r.t. an axiomatic system for first-order classical
logic; our further lemmas involving modal reasoning are denoted with names
that are commonly used in informal presentations.

The code in gl.ml mainly consists then of the formalized proofs of those
lemmas _in_ $\mathbb{GL}$ that are useful for the formalized results we
present in the next section. This file might be thought as a “kernel” for
further experiments in reasoning about axiomatic calculi by using HOL Light.
The lemmas we proved are, indeed, standard tautologies of classical
propositional logic, along with specific theorems of minimal modal logic and
its extension for transitive frames – i.e. of the systems $\mathbb{K}$ and
$\mathbb{K}4$ [17] –, so that by applying minor changes in basic definitions,
they are – so to speak – take-away proof-terms for extensions of that very
minimal system within the realm of normal modal logics.

More precisely, we have given, whenever it was useful, a “natural deduction”
characterization of classical operators both in terms of an implicit (or
internal) deduction – and in that case we named the lemma with the suffix
`_th` –, such as

      GL_modusponens_th
        |- !p q. |-- ((p --> q) && p --> q)

and as a derived rule of the axiomatic system mimicking the behaviour of the
connective in Gentzen’s formalism, e.g.,

      GL_and_elim
        |- !p q r. |-- (r --> p && q) ==> |-- (r --> q)  /\ |-- (r --> p)

We had to prove about 120 such results of varying degree of difficulty. We
believe that this file is well worth the effort of its development, for two
main reasons to be considered – along with the just mentioned fact that they
provide a (not so) minimal set of internal lemmas which can be moved to
different axiomatic calculi at, basically, no cost.

Indeed, on the one hand, these lemmas simplify the subsequent formal proofs
involving consistent lists of formulae since they let us work formally within
the scope of $\vdash$, so that we can rearrange subgoals according to their
most useful equivalent form by applying the appropriate
$\mathbb{GL}$-lemma(s).

On the other hand, the endeavour of giving formal proofs of these lemmas of
the calculus $\mathbb{GL}$ has been important for checking how much our proof-
assistant is “friendly” and efficient in performing this specific task.

As it is known, any axiomatic system fits very well an investigation involving
the notion of _theoremhood_ for a specific logic, but its lack of naturalness
w.r.t. the practice of developing informal proofs makes it an unsatisfactory
model for the notion of _deducibility_. In more practical terms: developing a
formal proof of a theorem in an axiomatic system _by pencil and paper_ can be
a dull and uninformative task.

After approaching this very same objective by using HOL Light, we feel like
expressing mixed opinions on the general experience. In most cases, relying on
the automation tools of this specific proof assistant did indeed save our time
and resources when trying to give a formal proof in $\mathbb{GL}$.
Nevertheless, there has been a number of $\mathbb{GL}$-lemmas for proving
which those automation tools did not revealed useful at all. In those cases,
actually, we had to perform a tentative search of the specific instances of
axioms from which deriving the lemmas,666The HOL Light tactics for first-order
reasoning MESON and METIS were unable, for instance, of instantiating
autonomously the obvious middle formula for the transitivity of an
implication, or even the specific formulae of a schema to apply to the goal in
order to rewrite it. so that interactive proving them had advantages as well
as traditional instruments of everyday mathematicians.

Just to stress the general point: it is clearly possible – and actually useful
in general – to rely on the resources of HOL Light to develop formal proofs
both _about_ and _within_ an axiomatic calculus for a specific logic, in
particular when the lemmas of the object system have relevance or practical
utility for mechanizing (meta-)results on it; however, these very resources –
and, as far as we can see, the tools of any other general proof assistant – do
not look peculiarly satisfactory for pursuing investigations on derivability
within axiomatic systems.

###  2.2 Soundness Lemma

At this point, we can prove that $\mathbb{GL}$ is sound – i.e. every formula
derivable in the calculus is a tautology in the class of irreflexive
transitive frames. This is obtained by simply unfolding the relevant
definitions and applying theorems `TRANSNT_EQ_LOB` and `ITF_NT` of Section
1.2:

      GL_TRANSNT_VALID
        |- !p. (|-- p) ==> TRANSNT:(W->bool)#(W->W->bool)->bool |= p

      GL_ITF_VALID
        |- !p. |-- p ==> ITF:(W->bool)#(W->W->bool)->bool |= p

From this, we get a model-theoretic proof of consistency for the calculus

      GL_consistent
        ~ |-- False

This having exhausted the contents of `gl.ml`, we would move to consider now
the most interesting part of our effort, namely the mechanized proof of
completeness for the calculus w.r.t. this very same class of frames. That
constitutes the remaining contents of our implementation, beside the auxiliary
code in `misc.ml` furnishing some general results about lists of items with
same type we needed to handle the subsequent constructions, but have more
general utility.

##  3 Completeness and Decidability

When dealing with normal modal logics, it is common to develop a proof of
completeness w.r.t. relational semantics by using the so-called ‘canonical
model method’. This can be summarized as a standard construction of
countermodels made of maximal consistent sets of formulae and an appropriate
accessibility relation [17].

For $\mathbb{GL}$, we cannot pursue this strategy, since the logic is not
compact: maximal consistent sets are (in general) infinite objects, though the
notion of derivability involves only a finite set of formulae. For being not
compact, we cannot therefore reduce the semantic notion of (in)coherent set of
formulae to the syntactic one of (in)consistent set of formulae: when
extending a consistent set of formulae to a maximal consistent one, we might
end up with a _syntactically_ consistent set that nevertheless cannot be
_semantically_ satisfied.

In spite of this, it is possible to achieve a completeness result by

  1. 1.

identifying the relevant properties of maximal consistent sets of formulae;
and

  2. 2.

tweaking the definitions so that those properties hold for specific consistent
sets of formulae related to the formula we want to find a countermodel to.

As a matter of fact, we can claim something more: it is possible to carry out
in a _very natural way_ a related tweaked Lindenbaum construction to extend
consistent _lists_ to maximal consistent ones, preserving the standard line of
reasoning in completeness proofs, and, at the same time, avoiding symbolic
subtleties that have no real relevance for the argument, but have the
unpleasant consequence of making the formalized proof unnecessarily long, so
that the implementation would sound rather pedantic – or even dull.

###  3.1 Maximal Consistent Lists

As just claimed, in order to make efficient use of our formal device, we will
work with _lists_ of formulae, instead of simple sets.777See Section 3.2 below
for the reasons of our choice. Accordingly, we define first, by recursion on
the list, the operation of finite conjunction of formulae in a list:

      let CONJLIST = new_recursive_definition list_RECURSION
        ‘CONJLIST [] = True /\
         (!p X. CONJLIST (CONS p X) = if X = [] then p else p && CONJLIST X)‘;;

Afterwards, we prove some properties of this operation on lists that
characterize it in terms of $\mathbb{GL}$-derivability, and which depends,
basically, on most of the $\mathbb{GL}$-lemmas defined above. In particular,
since $\mathbb{GL}$ is a normal modal logic – i.e. its modal operator
distributes over implication and preserves theoremhood – we have that our
modal operator distributes over the conjunction of $X$ so that we have
`CONJLIST_MAP_BOX`:

$\mathbb{GL}\vdash\Box\bigwedge X\leftrightarrow\bigwedge\Box X,$

where $\Box X$ is an abuse of notation for the list obtained by “boxing” each
formula in $X$.

We are now able to define the notion of consistent list of formulae and prove
the main properties of this kind of objects:

      let CONSISTENT = new_definition
        ‘CONSISTENT (l:form list) <=> ~ (|-- (Not (CONJLIST l)))‘;;

In particular, we prove that:

  * •

a consistent list cannot contain either both $A$ and $\neg A$ for any formula
$A$, nor $\bot$ (see theorems `CONSISTENT_LEMMA`, `CONSISTENT_NC`, and
`FALSE_IMP_NOT_CONSISTENT`, respectively);

  * •

for any consistent list $A$ and formula $A$, $X+A$ is consistent, or $X+\neg
A$ is consistent (`CONSISTENT_EM`), where $+$ denotes the usual operation of
appending an element to a list.

Our maximal consistent lists w.r.t. a given formula $A$ will be consistent
lists that do not contain repetitions and that contain, for any subformula of
$A$, that very subformula or its negation:888Here we define the set of
subformulae of $A$ as the reflexive transitive closure of the set of formulae
on which the main connective of $A$ operates: this way, the definition is
simplified and it is easier to establish standard properties of the set of
subformulae by means of general higher-order lemmas in HOL Light for the
closure of a given relation.

      let MAXIMAL_CONSISTENT = new_definition
        ‘MAXIMAL_CONSISTENT p X <=>
         CONSISTENT X /\ NOREPETITION X /\
         (!q. q SUBFORMULA p ==> MEM q X \/ MEM (Not q) X)‘;;

where `X` is a list of formulae and `MEM q X` is the membership relation for
lists. We then establish the main closure property of maximal consistent
lists:

      MAXIMAL_CONSISTENT_LEMMA
        |- !p X A b. MAXIMAL_CONSISTENT p X /\
                     (!q. MEM q A ==> MEM q X) /\
                     b SUBFORMULA p /\
                     |-- (CONJLIST A --> b)
                     ==> MEM b X

After proving some further lemmas with practical utility – in particular, the
fact that any maximal consistent list behaves like a restricted bivalent
evaluation for classical connectives (`MAXIMAL_CONSISTENT_MEM_NOT` and
`MAXIMAL_CONSISTENT_MEM_CASES`) – we can finally define the ideal (type of
counter)model we are interested in. The type `STANDARD_MODEL` consists, for a
given formula $A$, of:

  1. 1.

the set of maximal consistent lists w.r.t. $A$ made of subformulae of $A$ or
their negations, as possible worlds;

  2. 2.

an irreflexive transitive accessibility relation $R$ such that for any
subformula $\Box B$ of $A$ and any world $w$, $\Box B$ is in $w$ iff for any
$x$ $R$-accessible from $w$, $B$ is in $x$;

  3. 3.

an atomic valuation that gives value $1$ to $p$ in $w$ iff $p$ is a subformula
of $A$.

Here is the corresponding code:

      let GL_STANDARD_FRAME = new_definition
        ‘GL_STANDARD_FRAME p (W,R) <=>
         W = {w | MAXIMAL_CONSISTENT p w /\
                  (!q. MEM q w ==> q SUBFORMULA p \/
                                   (?q’. q = Not q’ /\ q’ SUBFORMULA p))} /\
         ITF (W,R) /\
         (!q w. Box q SUBFORMULA p /\ w IN W
                ==> (MEM (Box q) w <=> !x. R w x ==> MEM q x))‘;;

      let GL_STANDARD_MODEL = new_definition
        ‘GL_STANDARD_MODEL p (W,R) V <=>
         GL_STANDARD_FRAME p (W,R) /\
         (!a w. w IN W ==> (V a w <=> MEM (Atom a) w /\ Atom a SUBFORMULA p))‘;;

###  3.2 Maximal Extensions

What we have to do now is to show that the type `GL_STANDARD_MODEL` is
nonempty. We achieve this by constructing suitable maximal consistent lists of
formulae from specific consistent ones.

Our original strategy differs from the presentation given in e.g. [6] for
being closer to the standard Lindenbaum construction commonly used in proving
completeness results. By doing so, we have been able to circumvent both the
pure technicalities in formalizing the combinatorial argument sketched in [6,
p.79] _and_ the problem – apparently inherent to the Lindenbaum extension –
due to the non-compactness of the system, as we mentioned before.

Given a formula $A$, the key idea is to extend a consistent list of
subformulae of $A$ or their negations in a step-by-step construction, by
adding at each stage of the process a subformula of $A$ – if the resulting
list is consistent – or – otherwise – the negation of that very subformula,
after fixing an enumeration of the subformulae of $A$:

      EXTEND_MAXIMAL_CONSISTENT
        |- !p X.
             CONSISTENT X /\
             (!q. MEM q X ==> q SUBFORMULA p \/ (?q’. q = Not q’ /\ q’ SUBFORMULA p))
             ==> ?M. MAXIMAL_CONSISTENT p M /\
                     (!q. MEM q M
                          ==> q SUBFORMULA p \/
                              (?q’. q = Not q’ /\ q’ SUBFORMULA p)) /\
                     X SUBLIST M

This way, we are in the pleasant condition of carrying out the construction by
using the HOL Light device efficiently, and, at the same time, we do not have
to worry about the non-compactness of $\mathbb{GL}$ since we are working with
finite objects – the type list – by default.

Henceforth, we see that – under the assumption that $A$ is not a
$\mathbb{GL}$-lemma – the set of possible worlds in `STANDARD_FRAME` w.r.t.
$A$ is nonempty, as required by the definition of relational structures:

      NONEMPTY_MAXIMAL_CONSISTENT
        |- !p. ~ |-- p
               ==> ?M. MAXIMAL_CONSISTENT p M /\
                       MEM (Not p) M /\
                       (!q. MEM q M ==> q SUBFORMULA p \/
                                        (?q’. q = Not q’ /\ q’ SUBFORMULA p))

Next, we have to define an $R$ satisfying the condition 2 for a
`STANDARD_FRAME`; the following does the job:

      let GL_STANDARD_REL = new_definition
        ‘GL_STANDARD_REL p w x <=>
         MAXIMAL_CONSISTENT p w /\
         (!q. MEM q w ==> q SUBFORMULA p \/ ?q’. q = Not q’ /\ q’ SUBFORMULA p) /\
         MAXIMAL_CONSISTENT p x /\
         (!q. MEM q x ==> q SUBFORMULA p \/ ?q’. q = Not q’ /\ q’ SUBFORMULA p) /\
         (!B. MEM (Box B) w ==> MEM (Box B) x /\ MEM B x) /\
         (?E. MEM (Box E) x /\ MEM (Not (Box E)) w)‘;;

Such an accessibility relation, together with the set of the specific maximal
consistent lists we are dealing with, defines a structure in `ITF` with the
required properties:

      ITF_MAXIMAL_CONSISTENT
        |- !p. ~ |-- p
               ==> ITF ({M | MAXIMAL_CONSISTENT p M /\
                             (!q. MEM q M ==> q SUBFORMULA p \/
                                              ?q’. q = Not q’ /\ q’ SUBFORMULA p)},
                        GL_STANDARD_REL p),

      ACCESSIBILITY_LEMMA
        |- !p M w q.
             ~ |-- p /\
             MAXIMAL_CONSISTENT p M /\
             (!q. MEM q M ==> q SUBFORMULA p \/ (?q’. q = Not q’ /\ q’ SUBFORMULA p)) /\
             MAXIMAL_CONSISTENT p w /\
             (!q. MEM q w ==> q SUBFORMULA p \/ (?q’. q = Not q’ /\ q’ SUBFORMULA p)) /\
             MEM (Not p) M /\
             Box q SUBFORMULA p /\
             (!x. GL_STANDARD_REL p w x ==> MEM q x)
             ==> MEM (Box q) w,

###  3.3 Truth Lemma and Completeness

For our ideal model, it remains to reduce the semantic relation of forcing to
the more tractable one of membership to the specific world. More formally, we
prove – by induction on the complexity of the subformula $B$ of $A$ – that if
$\mathbb{GL}\not\vdash A$, then for any world $w$ of the standard model, $B$
holds in $w$ iff $B$ is member of $w$:

      GL_truth_lemma
        |- !W R p V q.
             ~ |-- p /\
             GL_STANDARD_MODEL p (W,R) V /\
             q SUBFORMULA p
             ==> !w. w IN W ==> (MEM q w <=> holds (W,R) V q w),

Finally, we are able to prove the main result: if $\mathbb{GL}\not\vdash A$,
then the list $[\neg A]$ is consistent, and by applying
`EXTEND_MAXIMAL_CONSISTENT`, we obtain a maximal consistent list $X$ w.r.t.
$A$ that extends it, so that, by applying `GL_truth_lemma`, we have that
$X\not\vDash A$ in our standard model. The corresponding formal proof reduces
to the application of those previous results and the appropriate
instantiations:

      COMPLETENESS_THEOREM
        |- !p. ITF:(form list->bool)#(form list->form list->bool)->bool |= p
               ==> |-- p,

Notice that the family of frames `ITF` is polymorphic, but, at this stage, our
result holds only for frames on the domain `form list`, as indicated by the
type annotation. This is not an intrinsic limitation: the next section is
devoted indeed to generalize this theorem to frames on an arbitrary domain.

As an immediate corollary, we have that the system $\mathbb{GL}$ is decidable
and, in principle, we could implement a decision procedure for it in OCaml.
However, this is a difficult task – especially if one seeks efficiency and
completeness – and it is out of the scope of the present work. Nevertheless,
we feel like offering a very rough approximation.

We define the tactic `GL_TAC` and its associated rule `GL_RULE` that perform
the following steps: (1) apply the completeness theorem, (2) unfold some
definitions, and (3) try to solve the resulting _semantic_ problem using
first-order reasoning.

      let GL_TAC : tactic =
        MATCH_MP_TAC COMPLETENESS_THEOREM THEN
        REWRITE_TAC[valid; FORALL_PAIR_THM; holds_in; holds;
                    ITF; GSYM MEMBER_NOT_EMPTY] THEN
        MESON_TAC[];;

      let GL_RULE tm = prove(tm, REPEAT GEN_TAC THEN GL_TAC);;

The above naive strategy is able to prove automatically some lemmas which are
common to normal modal logic, but require some effort when derived in an
axiomatic system. As an example consider the following $\mathbb{GL}$-lemma:

      GL_box_iff_th
        |- !p q. |-- (Box (p <-> q) --> (Box p <-> Box q))

When developing a proof of it within the axiomatic calculus, we need to “help”
HOL Light with by instantiating several further $\mathbb{GL}$-lemmas, so that
the resulting proof-term consists of ten lines of code. On the contrary, our
rule is able to check it in few steps:

      # GL_RULE ‘!p q. |-- (Box (p <-> q) --> (Box p <-> Box q))‘;;
        0..0..1..6..11..19..32..solved at 39
        0..0..1..6..11..19..32..solved at 39
      val it : thm = |- !p q. |-- (Box (p <-> q) --> (Box p <-> Box q))

In spite of this, the automation offered by `MESON` tactic is not enough when
the generated semantic problem involves in an essential way the fact that our
frames are finite (or Noetherian). So, for instance, our procedure is not able
to prove the Löb axiom

$\mathbb{GL}\vdash\Box(\Box A\longrightarrow A)\longrightarrow\Box A\,.$

This suggests the need for improving `GL_TAC` to handle more general contexts:
in the long run, it is a likely-looking outcome of what we reached so far.

###  3.4 Generalizing via Bisimulation

As we stated before, our theorem `COMPLETENESS_THEOREM` provides the modal
completeness for $\mathbb{GL}$ with respect to a semantics defined using
models built on the type `:form list`. It is obvious that the same result must
hold whenever we consider models built on any infinite type. To obtain a
formal proof of this fact, we need to establish a _correspondence_ between
models built on different types. It is well-known that a good way to make
rigorous such correspondence is through the notion of _bisimulation_ [4].

In our context, given two models `(W1,R1)` and `(W2,R2)` sitting respectively
on types `:A` and `:B`, each with a valuation function `V1` and `V2`, a
bisimulation is a binary relation `Z:A->B->bool` that relates two worlds
`w1:A` and `w2:B` when they can _simulate_ each other. The formal definition
is as follows:

      BISIMIMULATION
        |- BISIMIMULATION (W1,R1,V1) (W2,R2,V2) Z <=>
           (!w1:A w2:B.
              Z w1 w2
              ==> w1 IN W1 /\ w2 IN W2 /\
                  (!a:string. V1 a w1 <=> V2 a w2) /\
                  (!w1’. R1 w1 w1’  ==> ?w2’. w2’ IN W2 /\ Z w1’ w2’ /\ R2 w2 w2’) /\
                  (!w2’. R2 w2 w2’ ==> ?w1’. w1’ IN W1 /\ Z w1’ w2’ /\ R1 w1 w1’))

Then, we say that two worlds are _bisimilar_ if there exists a bisimulation
between them:

      let BISIMILAR = new_definition
        ‘BISIMILAR (W1,R1,V1) (W2,R2,V2) (w1:A) (w2:B) <=>
         ?Z. BISIMIMULATION (W1,R1,V1) (W2,R2,V2) Z /\ Z w1 w2‘;;

The key fact is that the semantic predicate `holds` respects bisimilarity:

      BISIMILAR_HOLDS
        |- !W1 R1 V1 W2 R2 V2 w1:A w2:B.
             BISIMILAR (W1,R1,V1) (W2,R2,V2) w1 w2
             ==> (!p. holds (W1,R1) V1 p w1 <=> holds (W2,R2) V2 p w2)

From this, we can proof that validity is preserved by bisimilarity. The
precise statements are the following:

      BISIMILAR_HOLDS_IN
        |- !W1 R1 W2 R2.
             (!V1 w1:A. ?V2 w2:B. BISIMILAR (W1,R1,V1) (W2,R2,V2) w1 w2)
             ==> (!p. holds_in (W2,R2) p ==> holds_in (W1,R1) p)

      BISIMILAR_VALID
        |- !L1 L2.
             (!W1 R1 V1 w1:A.
                L1 (W1,R1) /\ w1 IN W1
                ==> ?W2 R2 V2 w2:B. L2 (W2,R2) /\
                                    BISIMILAR (W1,R1,V1) (W2,R2,V2) w1 w2)
             ==> (!p. L2 |= p ==> L1 |= p)

Finally, we can explicitly define a bisimulation between `ITF`-models on the
type `:form list` and on any infinite type `:A`. From this, it follows at once
the desired generalization of completeness for $\mathbb{GL}$:

      COMPLETENESS_THEOREM_GEN
        |- !p. INFINITE (:A) /\ ITF:(A->bool)#(A->A->bool)->bool |= p ==> |-- p

## Related Works

Our formalization gives a mechanical proof of completeness for $\mathbb{GL}$
in HOL Light which sticks to the original Henkin’s method for classical logic.
In its standard version, its nature is synthetic and intrinsically semantic
[9], and, as we stated before, it is the core of the canonical model
construction for most of normal modal logic.

That very approach does not work for $\mathbb{GL}$. Nevertheless, the modified
extension lemma we proved in our mechanization introduces an analytic flavour
to the strategy – for building maximal consistent lists in terms of components
of the given formula non-proven in the calculus – and shows that Henkin’s idea
can be applied to $\mathbb{GL}$ too modulo appropriate changes.

As far as we know, _no other mechanized proof of modal completeness for_
$\mathbb{GL}$ has been given before, despite there exist formalizations of
similar results for several other logics, manly propositional and first-order
classical and intuitionistic logic.

Formalizations of completeness for _classical logic_ define an established
trend in interactive theorem proving since [18], where a Hintikka-style
strategy is used to define a theoremhood checker for formulas built up by
negation and disjunction only.

In fact, a very general treatment of systems for classical propositional logic
is given in [16]. There, axiomatic calculus is investigated along with natural
deduction, sequent calculus, and resolution system in Isabelle/HOL, and
completeness is proven by Hintikka-style method for sequent calculus first, to
be lifted then to the other formalisms by means of translations of each system
into the others. Their formalization is more ambitious than ours, but, at the
same time, it is focused on a very different aim.

Finally, a recent overview of meta-theoretical results for several calculi and
theorem provers formalized in HOL/Isabelle is given in [5], where, in any
case, a different proof assistant is used towards a more general investigation
unrelated to modal logics.

An objective more similar to ours is obtained in [3], where the Henkin-style
completeness for the system $\mathbb{S}5$ is formalized within the Lean
theorem prover – therefore, it uses a different meta-theory and works on the
classical method of canonical model for normal modal logic.

## References

  * [1] Juan Aguilera and David Fernández-Duque.  Strong completeness of provability logic for ordinal spaces.  The Journal of Symbolic Logic, 82:608–628, 11 2017.  doi:10.1017/jsl.2017.3.
  * [2] Lev Beklemishev and Albert Visser.  Problems in the logic of provability.  In Mathematical Problems from Applied Logic I, pages 77–136. Springer, 2006.
  * [3] Bruno Bentzen.  A henkin-style completeness proof for the modal logic S5.  CoRR, abs/1910.01697, 2019.  URL: http://arxiv.org/abs/1910.01697, arXiv:1910.01697.
  * [4] Patrick Blackburn and Johan Van Benthem.  Modal logic: a semantic perspective.  In Handbook of modal logic, volume 3, pages 1–84. Elsevier, 2007\.
  * [5] Jasmin Christian Blanchette.  Formalizing the metatheory of logical calculi and automatic provers in isabelle/hol (invited talk).  In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, page 1–13, New York, NY, USA, 2019\. Association for Computing Machinery.  doi:10.1145/3293880.3294087.
  * [6] George Boolos.  The logic of provability.  Cambridge university press, 1995.
  * [7] B. Jack Copeland.  The genesis of possible worlds semantics.  Journal of Philosophical logic, 31(2):99–137, 2002.
  * [8] Melvin Fitting.  Modal proof theory.  In Handbook of modal logic, pages 85–138. Elsevier, 2007.
  * [9] Melvin Fitting and Richard L Mendelsohn.  First-order modal logic, volume 277.  Springer Science & Business Media, 2012.
  * [10] Kurt Gödel.  Eine interpretation des intuitionistischen aussagenkalküls. ergebnisse eines mathematischen kolloquiums, 4: 39–40, 1933. english translation, with an introductory note by as troelstra.  Kurt Gödel, Collected Works, 1:296–303, 1986.
  * [11] Robert Goldblatt.  Mathematical modal logic: A view of its evolution.  In Handbook of the History of Logic, volume 7, pages 1–98. Elsevier, 2006.
  * [12] John Harrison.  The HOL Light Theorem Prover.  Web site: https://github.com/jrh13/hol-light.
  * [13] John Harrison.  HOL Light tutorial.  http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf, 2017.
  * [14] David Hilbert and Paul Bernays.  Grundlagen der Mathematik, Vol. I (1934), Vol II (1939).  Berlin: Springer, 1939.
  * [15] Joachim Lambek and Philip J Scott.  Introduction to higher-order categorical logic, volume 7.  Cambridge University Press, 1988.
  * [16] Julius Michaelis and Tobias Nipkow.  Formalized proof systems for propositional logic.  In A. Abel, F. Nordvall Forsberg, and A. Kaposi, editors, 23rd Int. Conf. Types for Proofs and Programs (TYPES 2017), volume 104 of LIPIcs, pages 6:1–6:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018\.
  * [17] Sally Popkorn.  First steps in modal logic.  Cambridge University Press, 1994.
  * [18] Natarajan Shankar.  Towards mechanical metamathematics.  Journal of Automated Reasoning, 1(4):407–434, 1985.
  * [19] Robert M Solovay.  Provability interpretations of modal logic.  Israel journal of mathematics, 25(3-4):287–304, 1976.