# Cut elimination for propositional cyclic proof systems with fixed-point
operators

Hiromasa Hori Graduate School of Informatics, Nagoya University,
<EMAIL_ADDRESS>Koji Nakazawa Graduate School of Informatics, Nagoya
University<EMAIL_ADDRESS>Makoto Tatsuta National Institute of
Informatics/Sokendai<EMAIL_ADDRESS>
###### Abstract

Infinitary and cyclic proof systems are proof systems for logical formulas
with fixed-point operators or inductive definitions. A cyclic proof system is
a restriction of the corresponding infinitary proof system. Hence, these proof
systems are generally not the same, as in the cyclic system may be weaker than
the infinitary system. For several logics, the infinitary proof systems are
shown to be cut-free complete. However, cyclic proof systems are characterized
with many unknown problems on the (cut-free) completeness or the cut-
elimination property. In this study, we show that the provability of
infinitary and cyclic proof systems are the same for some propositional logics
with fixed-point operators or inductive definitions and that the cyclic proof
systems are cut-free complete.

##  1 Introduction

Infinitary and cyclic (or regular) proof systems are proof systems for logical
formulas containing fixed-point operators or inductively defined predicates.
Infinitary proof systems allow infinite branches in proof trees that satisfy a
soundness condition, corresponding to the principle of infinite descent.
Cyclic proofs are regular infinite proofs and can be represented by finite
proof tree with some cycles. A proof search in cyclic proof systems is not
necessary to decide induction hypotheses beforehand. Therefore, compared to
proof systems with an explicit induction rule, cyclic proof systems are more
suitable for automatic reasoning of inductive properties [4]. For this reason,
cyclic proof systems have been widely studied for several logics, such as the
linear logic [8, 6] and the separation logic [2, 3, 14, 10] for the software
verification as well as first-order logic [1, 5].

Some theoretical properties for infinitary and cyclic proof systems have been
studied. For instance, several completeness results have been reported for
infinitary cut-free proof systems of logics, such as the modal $\mu$-calculus
[13], the linear-time $\mu$-calculus [7], and the first-order logic with
inductive definitions [1]. Furthermore, Doumane [8] proved the cut-elimination
property for the infinitary proof system of the multiplicative and additive
linear logic with fixed-point operators. Also, several negative results were
also reported on cut elimination for cyclic proof systems of logics, such as
the symbolic heaps of separation logic [10], the logic of bunched implications
[12], and the first-order logic with inductive definitions [11]. In [6], Das
et al. proved that the infinitary and cyclic cut-free proof systems are
equivalent in additive linear logic with fixed-point operators; hence cut
elimination holds for the cyclic system.

In this study, we show that every infinite proof can be transformed into a
cyclic proof by only changing structures of proof trees and without adding
rule applications if each infinite branch in the infinite proof contains only
finitely many sequents. It can be easily seen that infinite proofs in several
propositional logics, such as the modal $\mu$-calculus, the linear time
$\mu$-calculus, and the classical propositional logic, always satisfy the
condition. This indicates that cut-free cyclic proof systems of these logics
are equivalent to cut-free infinitary systems. Therefore, these cyclic proof
systems are also cut-free complete.

Das et al. [6] have provided a similar result for the additive linear logic
with fixed point operators. They developed a proof sketch which shows that if
an infinitary proof contains only finitely many formulas, a regular proof of
the same conclusion using Rabin’s basis theorem can be found, since the set of
infinite proof of the conclusion constitutes an $\omega$-regular tree
language. Our result differs from theirs in two points. (1) We assume only
that each infinite branch contains only finitely many sequents, and the whole
proof may contain infinitely many sequents. Hence, our assumption is weaker
than theirs. (2) Our proof is simple and does not depend on the complex theory
of tree languages and Rabin’s theorem.

This paper is organized as follows. In Chapter 2, we recall the infinitary
proof system $\mu LK^{\infty}$ and the cyclic proof system $\mu LK^{\omega}$
for the propositional logic with fixed point operators. In Chapter 3, we prove
the main theorem of this study and show the equivalence between $\mu
LK^{\infty}$ and $\mu LK^{\omega}$. In Chapter 4, we adapt our proof to some
propositional modal logics with fixed-point operators, such as the linear-time
$\mu$-calculus and the modal $\mu$-calculus. In Chapter 5, our proof is
adapted to the infinitary proof system and the cyclic proof system for the
classical sequent calculi with inductively defined propositions, which are the
propositional fragments of $\rm{LKID}^{\omega}$ and $\rm{CLKID}^{\omega}$
proposed by Brotherston et al [1, 5]. In Chapter 6, we conclude this paper and
discuss future work.

##  2 Infinite and cyclic proofs with fixed-point operators

In this chapter, we recall the infinitary and cyclic proof system for
propositional logic with fixed-point operators [8]. In Section 2.1, we define
the syntax of those systems. In sections 2.2 and 2.3, we define the infinite
system $\mu LK^{\infty}$ and the cyclic system $\mu LK^{\omega}$,
respectively. As [8], these systems are given in the one-sided sequent-
calculus style.

###  2.1 Propositional logic with fixed-point operators

Below we define the language of the propositional logic with fixed-point
operators and the Fischer-Ladner subformula relation that extends the ordinary
subformula relation.

######  Definition 2.1 (Formulas).

We use $p$ for a metavariable for atomic proposition symbols and $X,Y,\ldots$
for propositional variables. The _formulas_ $F,G,\ldots$ are defined as
follows.

$F:=p\ |\ p^{\bot}\ |\ \bot\ |\ \top\ |\ F\lor G\ |\ F\land G\ |\ X\ |\ \mu
X.F\ |\ \nu X.F$

Here, $\mu$ and $\nu$ denote the least and greatest fixed points,
respectively.

######  Definition 2.2 (Negation).

We define the _negation_ $F^{\bot}$ of $F$ as follows.

$\displaystyle\top^{\bot}=$ $\displaystyle\bot$ $\displaystyle\bot^{\bot}=$
$\displaystyle\top$ $\displaystyle(p)^{\bot}=$ $\displaystyle p^{\bot}$
$\displaystyle(p^{\bot})^{\bot}=$ $\displaystyle p$ $\displaystyle(F\land
G)^{\bot}=$ $\displaystyle F^{\bot}\lor G^{\bot}$ $\displaystyle(F\lor
G)^{\bot}=$ $\displaystyle F^{\bot}\land G^{\bot}$ $\displaystyle(X)^{\bot}=$
$\displaystyle X^{\bot}$ $\displaystyle(\mu X.F)^{\bot}=$ $\displaystyle\nu
X.F^{\bot}$ $\displaystyle(\nu X.F)^{\bot}=$ $\displaystyle\mu X.F^{\bot}$

######  Definition 2.3 (Subformulas).

We define the relation $\rightharpoonup$ on formulas as follows.

$\displaystyle F\star G$ $\displaystyle\rightharpoonup F$
$\displaystyle\star\in\\{\land,\lor\\}$ $\displaystyle F\star G$
$\displaystyle\rightharpoonup G$ $\displaystyle\star\in\\{\land,\lor\\}$
$\displaystyle\sigma X.F$ $\displaystyle\rightharpoonup F$
$\displaystyle\sigma\in\\{\mu,\nu\\}$

Let $\rightharpoonup^{*}$ be the reflexive transitive closure of
$\rightharpoonup$ and if $F\rightharpoonup^{*}G$, $G$ is called a _subformula_
of $F$.

######  Definition 2.4 (Fischer-Ladner subformulas).

We define the relation $\rightarrow$ on formulas as follows.

$\displaystyle F\star G$ $\displaystyle\rightarrow F$
$\displaystyle\star\in\\{\land,\lor\\}$ $\displaystyle F\star G$
$\displaystyle\rightarrow G$ $\displaystyle\star\in\\{\land,\lor\\}$
$\displaystyle\sigma X.F$ $\displaystyle\rightarrow F[\sigma X.F/X]$
$\displaystyle\sigma\in\\{\mu,\nu\\}$

Here, $F[G/X]$ is the ordinary capture-avoiding substitution of formulas. Let
$\rightarrow^{*}$ be the reflexive transitive closure of $\rightarrow$ and if
$F\rightarrow^{*}G$, $G$ is called a _Fischer-Ladner subformula_ of $F$.
$FL(F)$ is defined as the set of Fischer-Ladner subformulas of $F$ and called
the _Fischer-Ladner closure_.

######  Example 2.5.

Let $F=\mu X.X\land p\ \text{and}\ G=(\mu X.X\land p)\land p$. $F\to G$ holds
but $F\rightharpoonup G$ does not hold. Both $G\to F$ and $G\rightharpoonup F$
hold. We have $FL(F)=\\{F,G,p\\}$.

######  Lemma 2.6 ([9]).

For any formula $F$, $FL(F)$ is finite.

###  2.2 Infinitary proof system $\mu LK^{\infty}$

In this subsection, we define the infinitary proof system $\mu LK^{\infty}$.

######  Definition 2.7 (Sequents).

A _sequent_ is an expression of the form $\vdash\Gamma$ in which $\Gamma$ is a
finite set of formulas.

######  Definition 2.8 (Inference rules of $\mu LK^{\infty}$).

The inference rules of $\mu LK$ are given in Figure 1. For each rule except
for (Cut), the distinguished formula in the conclusion is called the
_principal formula_ of the rule and the distinguished formulas in the premises
are called _auxiliary formulas_ of the rule.

Structural rules:
(Axiom) $\vdash F,F^{\bot}$ $\vdash F^{\bot},\Delta_{1}$ $\vdash F,\Delta_{2}$
(Cut) $\vdash\Delta_{1},\Delta_{2}$ $\vdash\Delta$ (Weak) $\vdash F,\Delta$

Logical rules:
$\vdash F,G,\Delta$ $(\lor)$ $\vdash F\lor G,\Delta$ $\vdash F,\Delta_{1}$
$\vdash G,\Delta_{2}$ $(\land)$ $\vdash F\land G,\Delta_{1},\Delta_{2}$
$\vdash A[X:=\mu X.A],\Delta$ $(\mu)$ $\vdash\mu X.A,\Delta$ $\vdash A[X:=\nu
X.A],\Delta$ $(\nu)$ $\vdash\nu X.A,\Delta$ $(\top)$ $\vdash\top$

Figure 1: Inference rules for $\mu LK^{\infty}$

######  Definition 2.9 ($\mu LK^{\infty}$ pre-proofs).

A _pre-proof_ of $\mu LK^{\infty}$ is a possibly infinite tree that is
coinductively generated by the rules of Figure 1.

######  Definition 2.10 (Branches).

For a pre-proof $\pi$, a _branch_ in $\pi$ is a sequence of sequents
$(\vdash\Gamma_{i})_{i\in o}$ for $o\in\omega+1$ such that, for any $i\in o$,
$\vdash\Gamma_{i+1}$ is an assumption of a rule instance in $\pi$ whose
conclusion is $\vdash\Gamma_{i}$.

Note that a branch $(\vdash\Gamma_{i})_{i\in o}$ may be either finite
($o\in\omega$) or infinite ($o=\omega$).

######  Definition 2.11 (Threads).

For a branch $(\vdash\Gamma_{i})_{i\in o}$ in a pre-proof $\pi$, a _thread_
following the branch is a sequence of formulas $(F_{i})_{i\in o}$ that
satisfies the following for any $i\in o$.

(1)

$F_{i}\in\Gamma_{i}$.

(2)

If $\Gamma_{i}$ is the conclusion of a rule instance in $\pi$ and $F_{i}$ is
not its principal formula, then $F_{i}=F_{i+1}$.

(3)

If $\Gamma_{i}$ is the conclusion of a rule instance and $F_{i}$ is its
principal formula, then $F_{i+1}$ is an auxiliary formula of the rule
instance.

Note that, for any thread $(F_{i})_{i\in o}$, $F_{i}\to F_{i+1}$ holds for any
$i\in o$.

######  Definition 2.12 (Valid threads).

For an infinite thread $t$, ${\rm Inf}(t)$ is defined as the set of the
elements of $t$ that appears infinitely often in $t$ and $\min({\rm Inf}(t))$
is defined as the minimum element in ${\rm Inf}(t)$ w.r.t. the subformula
relation $\rightharpoonup^{*}$.

An infinite thread $t=(F_{i})_{i\in\omega}$ is said to be _valid_ if $t$ is
not stationary (i.e., $\forall i\in\omega.\exists j>i.F_{j}\neq F_{j+1}$) and
$\min({\rm Inf}(t))$ is a $\nu$-formula.

An infinite branch $B=(\vdash\Gamma_{i})_{i\in o}$ in a $\mu LK^{\infty}$ pre-
proof is said to be _valid_ if there is a valid thread $(F_{i})_{i>j}$
following a tail $(\vdash\Gamma_{i})_{i>j}$ of $B$.

Note that the set ${\rm Inf}(t)$ always contains the minimum element w.r.t.
the subformula relation ([8], Proposition 2.7).

######  Definition 2.13 ($\mu LK^{\infty}$ proof).

A _proof_ of $\mu LK^{\infty}$ is a pre-proof in which every infinite branch
is valid.

######  Example 2.14.

Let $F=\mu X.X\land p$ and $G=\nu X.X\land p$. Both of the following are
examples of the pre-proofs.

$\vdash F,p^{\bot}\vdash F\land p,p^{\bot}\lx@proof@logical@and\vdash
F,p^{\bot}\vdash F\land p,p^{\bot}\vdash p,p^{\bot}\qquad\vdash
G,p^{\bot}\vdash G\land p,p^{\bot}\lx@proof@logical@and\vdash G,p^{\bot}\vdash
G\land p,p^{\bot}\vdash p,p^{\bot}$

The left pre-proof is not a proof since the unique infinite branch contains no
valid thread. On the other hand, the right one is a proof since the infinite
branch contains the thread $t=(G,G\land p,G,G\land p,\ldots)$ such that
$\min({\rm Inf}(t))=G$ is a $\nu$-formula.

###  2.3 Cyclic proof system $\mu LK^{\omega}$

In this subsection, we define the cyclic proofs in $\mu LK^{\omega}$ with the
bud-companion functions [1, 5]. This definition is equivalent to the
regularity of proofs in $\mu LK^{\infty}$.

######  Definition 2.15 ($\mu LK^{\omega}$ pre-proof).

A pre-proof of $\mu LK^{\omega}$ is a pair $(\mathcal{D},\mathcal{C})$ such
that:

(1)

$\mathcal{D}$ is a finite derivation tree in which non-axiom leaves are
allowed. Let the set of non-axiom leaves in $\mathcal{D}$ be ${\rm
Bud}(\mathcal{D})$, and an element of ${\rm Bud}(\mathcal{D})$ is called a
_bud_.

(2)

$\mathcal{C}$ is a function from ${\rm Bud}(\mathcal{D})$ to the nodes in $D$
such that the sequent associated with $\mathcal{C}(\vdash\Gamma)$ is identical
to $\vdash\Gamma$ for each bud $\vdash\Gamma$. The node
$\mathcal{C}(\vdash\Gamma)$ is called the _companion_ of the bud
$\vdash\Gamma$.

Every $\mu LK^{\omega}$ pre-proof can be unfolded to a $\mu LK^{\infty}$ pre-
proof. The infinite branches and the infinite threads in $\mu LK^{\omega}$
pre-proofs are defined as those in the unfolded infinite pre-proofs in $\mu
LK^{\infty}$.

######  Definition 2.16 ($\mu LK^{\omega}$ proof).

A _proof_ of $\mu LK^{\omega}$ is a $\mu LK^{\omega}$ pre-proof such that
every infinite branch are valid.

######  Example 2.17.

For $G=\nu X.X\land p$, the following is an example of pre-proof in $\mu
LK^{\omega}$:

$\langle c\rangle\vdash G,p^{\bot}\vdash G\land
p,p^{\bot}\lx@proof@logical@and\langle b\rangle\vdash G,p^{\bot}\vdash
p,p^{\bot},$

which is accompanied by the bud-companion function ${\mathcal{C}}$ that maps
the sequent labeled with $\langle b\rangle$ to the sequent labeled with
$\langle c\rangle$. This is a proof in $\mu LK^{\omega}$ since we obtain the
proof of $\mu LK^{\infty}$ that is the right one in Example 2.14 by unfolding
this cyclic pre-proof.

##  3 Equivalence of $\mu LK^{\infty}$ and $\mu LK^{\omega}$

In this section, we prove the main theorem (Theorem 3.2) of this paper.

######  Definition 3.1.

For a branch $B$ in a proof, ${\rm Seq}(B)$ is defined as the set of sequents
that appear in $B$. For a proof $\pi$, ${\rm Rule}(\pi)$ is defined as the set
of the inference rules that appear in $\pi$.

######  Theorem 3.2.

For an infinite proof $\pi$ of $\vdash\Gamma$, if ${\rm Seq}(B)$ is finite for
every infinite branch $B$ in $\pi$, then there exists a cyclic proof
$\pi^{\prime}$ of $\vdash\Gamma$ such that ${\rm
Rule}(\pi^{\prime})\subseteq{\rm Rule}(\pi)$. In particular, if the infinite
proof $\pi$ of $\vdash\Gamma$ is cut free, then there exists a cut-free cyclic
proof $\pi^{\prime}$ of $\vdash\Gamma$.

###  3.1 Construction of a cycle for each infinite branch

First, for any infinite branch in a proof and a node on the branch, we can
find a pair of a bud and a companion above the node that yields a valid
branch.

######  Lemma 3.3.

Let $\pi$ be an infinite proof, $B=(\vdash\Gamma_{i})_{i\in\omega}$ be an
infinite branch in $\pi$, and $\vdash\Gamma_{j}$ be a node on $B$. If ${\rm
Seq}(B)$ is finite, there exist $b,c\in\omega$ that satisfies the following.

(1)

$j\leq c<b$.

(2)

$\Gamma_{b}=\Gamma_{c}$.

(3)

The infinite branch
$\vdash\Gamma_{0},\ldots,\vdash\Gamma_{c},\vdash\Gamma_{c+1},\ldots,\Gamma_{b}=\Gamma_{c},\Gamma_{c+1},\ldots$
is valid.

###### Proof.

Since $B$ is valid, there exists a valid thread $t=(F_{i})_{i>j^{\prime}}$
following a tail $B^{\prime}=(\vdash\Gamma_{i})_{i>j^{\prime}}$ of $B$.
W.l.o.g. we assume $j^{\prime}\geq j$, because, for the case $j>j^{\prime}$,
the thread $(F_{i})_{i>j}$ is also valid, so we can take $j$ as $j^{\prime}$.
By the condition of the validity, $t$ is not stationary and $\min({\rm
Inf}(t))$ is a $\nu$-formula.

For each $i>j^{\prime}$, mark $F_{i}\in\Gamma_{i}$ as $\overline{F_{i}}$. Let
$\vdash\overline{\Gamma_{i}}$ be the sequent obtained from $\vdash\Gamma_{i}$
by the marking and $\overline{B^{\prime}}$ be
$(\vdash\overline{\Gamma}_{i})_{i>j^{\prime}}$. Since ${\rm Seq}(B)$ is
finite, ${\rm Seq}(\overline{B^{\prime}})$ is finite, and hence there exists
$\vdash\overline{\Gamma}$ that appears infinitely many times in
$\overline{B^{\prime}}$. Then, we can find $b,c>j^{\prime}$ such that

  * •

$c<b$,

  * •

there exists $d$ between $b$ and $c$ such that $F_{d}\neq F_{d+1}$,

  * •

$\overline{\Gamma_{b}}=\overline{\Gamma_{c}}=\overline{\Gamma}$, and

  * •

there exists $e$ between $b$ and $c$ such that $F_{e}$ is the $\nu$-formula
$\min({\rm Inf}(t))$.

For these $b$ and $c$, the sequence
$F_{c},F_{c+1},\ldots,F_{b}=F_{c},F_{c+1},\ldots$ is a thread following the
branch
$\vdash\Gamma_{c},\vdash\Gamma_{c+1},\ldots,\vdash\Gamma_{b}=\vdash\Gamma_{c},\vdash\Gamma_{c+1},\ldots$.
Furthermore, for this thread $t^{\prime}$, $t^{\prime}$ is not stationary and
$\min({\rm Inf}(t))=F_{e}$ is a $\nu$-formula, and hence $t^{\prime}$ is
valid. ∎

###  3.2 Constructing cyclic proof

We will prove the main theorem by Lemma 3.3. However, if we naively use Lemma
3.3 for each infinite branch, some unexpected infinite branches may occur. For
example, for the infinite branches $B_{i}$ and $B_{i+1}$ in Figure 2, we may
find the pairs $(b_{i},c_{i})$ and $(b_{i+1},c_{i+1})$ by Lemma 3.3,
respectively. These bud-companion pairs designated by the dotted arrow yield a
pre-proof in the cyclic proof system, but it contains an infinite branch
designated by the solid arrow. This infinite branch does not exist in the
original infinite proof and its validity is not guaranteed.

Figure 2: Infinite branch through alternating multiple cycles

Therefore, we construct a cyclic proof by taking the bud-companion pairs while
avoiding unexpected infinite branch as shown in Figure 2.

Before we do that, we prove a basic lemma for trees.

######  Definition 3.4.

For a tree $T$, ${\rm Br}(T)$ is defined as the set of all finite or infinite
branches of $T$. For a branch $B=(n_{i})_{i\in o}\in{\rm Br}(T)$ and a node
$n_{j}$ on $B$, the _pruned branch_ $B|_{n_{j}}$ is defined as the finite
branch $(n_{i})_{0\leq i\leq n_{j}}$. For a set $\mathcal{B}$ of branches or
pruned branches of $T$, ${\rm Tr}(\mathcal{B})$ is defined as the tree
consisting of the branches and the pruned branches in $\mathcal{B}$, i.e., the
union of $\mathcal{B}$ as the set of the nodes.

######  Lemma 3.5.

Let $T$ be an infinite tree and $n_{B}$ be a node on $B$ for each $B\in
Br(T)$. If every $B\in Br(T)$ contains at most one element of
$\\{n_{B^{\prime}}\ |\ B^{\prime}\in Br(T)\\}$, then $Tr(\\{B|_{n_{B}}\ |\
B\in Br(T)\\})$ is a finite tree.

###### Proof.

Assuming that $Tr(\\{B|_{n_{B}}\ |\ B\in Br(T)\\})$ is an infinite tree, and
we show the contradiction. By König’s Lemma, there exists an infinite branch,
and it is an element $B\in Br(T)$. However, in $Tr(\\{B|_{n_{B}}\ |\ B\in
Br(T)\\})$, $B$ is pruned at $n_{B}$, and hence it cannot be included in
$Tr(\\{B|_{n_{B}}\ |\ B\in Br(T)\\})$. ∎

By this lemma, we prove the main theorem.

###### Proof of Theorem 3.2.

For an infinite proof $\pi$, let $\\{B_{\beta}\mid\beta<\alpha\\}={\rm
Br}(\pi)$ for some ordinal $\alpha$. Define the bud-companion pairs
$(b_{\beta},c_{\beta})$ on $B_{\beta}$ for each $\beta<\alpha$ as follows.

  * •

For 0:

    * –

If $B_{0}$ is finite, then both $b_{0}$ and $c_{0}$ are defined as the leaf of
$B_{0}$.

    * –

If $B_{0}$ is infinite, let $(b_{0},c_{0})$ as the bud-companion pair obtained
by Lemma 3.3 to $B_{0}$.

  * •

For $0<\beta<\alpha$:

    * –

If $B_{\beta}$ is finite, then both $b_{0}$ and $c_{0}$ are defined as the
leaf of $B_{0}$.

    * –

If $B_{\beta}$ is infinite and $b_{\gamma}$ for some $\gamma<\beta$ exists on
$B_{\beta}$, define $(b_{\beta},c_{\beta}):=(b_{\gamma},c_{\gamma})$.

    * –

Otherwise, consider the tree $T={\rm
Tr}(\\{B_{\gamma}|_{b_{\gamma}}\mid\gamma<\beta\\})$, and then $T$ is finite
by Lemma 3.5. By Lemma 3.3, we can find $(b_{\beta},c_{\beta})$ above $T$.

Then, let $\mathcal{D^{\prime}}$ be the tree $Tr(\\{B_{\beta}|_{b_{\beta}}\ |\
B\in Br(\mathcal{D})\\})$ and define
$\mathcal{C^{\prime}}(b_{\beta})=c_{\beta}$ for $\beta$ such that $B_{\beta}$
is infinite. By Lemma 3.5, $\mathcal{D^{\prime}}$ is finite, and
$(\mathcal{D^{\prime}},\mathcal{C^{\prime}})$ is a pre-proof of the cyclic-
proof system.

Let $B^{\prime}$ be an infinite branch in
$(\mathcal{D^{\prime}},\mathcal{C^{\prime}})$. By the construction,
$B^{\prime}$ has a tail consisting of the loop between $c_{\beta}$ and
$b_{\beta}$ for some $\beta$. By Lemma 3.3, the tail of $B^{\prime}$ contains
a valid thread, and hence $B^{\prime}$ is valid.

From the above, $(\mathcal{D^{\prime}},\mathcal{C^{\prime}})$ is a cyclic
proof. ∎

###  3.3 Equivalence of $\mu LK^{\infty}$ and $\mu LK^{\omega}$

By Theorem 3.2, we show the equivalence of provability between the infinite
proof system $\mu LK^{\infty}$ and the cyclic proof system $\mu LK^{\omega}$.

######  Lemma 3.6 (Subformula property for $\mu LK^{\infty}$).

Every formula that appears in a cut-free $\mu LK^{\infty}$ proof that
concludes $\vdash\Gamma$ is a Fischer-Ladner subformula of a formula contained
in $\Gamma$.

###### Proof.

For the inference rules of $\mu LK$ in Figure 1 except for (Cut), every
formula in the premises of the rule is a Fischer-Ladner subformula of a
formula in the conclusion. ∎

######  Theorem 3.7 (Equivalence between cut-free $\mu\rm{LK}^{\infty}$ and
cut-free $\mu\rm{LK}^{\omega}$.).

For any cut-free $\mu\rm{LK}^{\infty}$ proof, there exists a cut-free
$\mu\rm{LK}^{\omega}$ proof of the same conclusion.

###### Proof.

Let $\mathcal{D}$ be a cut-free $\mu\rm{LK}^{\infty}$ proof of $\vdash\Gamma$.
From Lemma 3.6, every formula in $\mathcal{D}$ is a Fischer-Ladner subformula
of a formula in conclusion sequent. From this and Lemma 2.6, ${\rm Seq}(B)$ is
finite for any infinite branch $B$ in $\mathcal{D}$. Therefore, by Theorem
3.2, there exists a cut-free $\mu\rm{LK}^{\omega}$ proof of $\vdash\Gamma$. ∎

Studer has proved that the infinitary proof system for the modal
$\mu$-calculus is cut-free complete [13] and the cut-elimination property of
$\mu LK^{\infty}$ follows from it, and hence we obtain the cut-elimination
property of the cyclic proof system $\mu LK^{\omega}$ as a corollary of
Theorem 3.7.

######  Corollary 3.8 (Cut elimination of $\mu LK^{\omega}$).

For any $\mu LK^{\omega}$ proof, there exists a cut-free $\mu LK^{\omega}$
proof of the same conclusion.

##  4 Infinite proofs and cyclic proofs with modal operators

In this chapter, we recall proof systems of propositional logic with fixed-
point operators and modal operators. We follow the definition in [8]. Then, we
show that Theorem 3.2 is applicable to these systems as well, and show the
equivalence of the provability between infinitary proof systems and cyclic
proof systems.

###  4.1 $\mu LK\bigcirc$: linear temporal logic with fixed-point operators

First, we recall infinite and cyclic proof systems of propositional logic with
fixed-point operators and the linear temporal operator $\bigcirc$. Then, we
prove that equivalence of provability of those systems.

######  Definition 4.1 ($\mu LK\bigcirc$).

Formulas of $\mu LK\bigcirc$ are defined as follows.

$F:=p\ |\ p^{\bot}\ |\ \bot\ |\ \top\ |\ F\lor G\ |\ F\land G\ |\ X\ |\ \mu
X.F\ |\ \nu X.F\ |\ \bigcirc F$

The negation is extended by $(\bigcirc A)^{\bot}=\bigcirc A^{\bot}$. The
Fischer-Ladner subformula relation is extended by $\bigcirc F\to F$.

######  Definition 4.2 (Rules for $\mu LK\bigcirc$).

The inference rules for $\mu LK\bigcirc$ are the rules in Figure 1 extended by
the following.

$\vdash\Gamma$ $(\bigcirc)$ $\vdash\bigcirc\Gamma$

Here, for a finite set $\Gamma=\\{F_{1},\ldots,F_{n}\\}$ of formulas, we
define $\bigcirc\Gamma$ as $\\{\bigcirc F_{1},\ldots,\bigcirc F_{n}\\}$.

As in the case of $\mu LK^{\infty}$ and $\mu LK^{\omega}$, the infinite proof
system $\mu LK\bigcirc^{\infty}$ and the cyclic proof system $\mu
LK\bigcirc^{\omega}$ are defined.

The proof of Theorem 3.2 can be adapted to $\mu LK\bigcirc$ in a
straightforward way. Furthermore, the finiteness of $FL(F)$ and the subformula
property holds also for $\mu LK\bigcirc$, and hence the equivalence between
the cut-free $\mu LK\bigcirc^{\infty}$ and the cut-free $\mu
LK\bigcirc^{\omega}$ follows.

######  Lemma 4.3.

The Fischer-Ladner closure is a finite set for any
$\mu\rm{LK\bigcirc}^{\infty}$ formula.

######  Lemma 4.4 (Subformula property for $\mu LK\bigcirc^{\infty}$).

Every formula that appears in a cut-free $\mu LK\bigcirc^{\infty}$ proof that
concludes $\vdash\Gamma$ is a Fischer-Ladner subformula of a formula contained
in $\Gamma$.

######  Theorem 4.5 (Equivalence between cut-free
$\mu\rm{LK}\bigcirc^{\infty}$ and cut-free $\mu\rm{LK}\bigcirc^{\omega}$).

For any $\mu\rm{LK}\bigcirc^{\infty}$-proof, there exists a
$\mu\rm{LK}\bigcirc^{\omega}$ proof of the same conclusion.

Dax et al. [7] have proved the cut-free completeness of the infinitary proof
system for $\mu LK\bigcirc$, and hence the cut elimination of $\mu
LK\bigcirc^{\omega}$ follows as a corollary.

######  Corollary 4.6 (Cut-elimination of $\mu LK\bigcirc^{\omega}$).

For any $\mu LK\bigcirc^{\omega}$ proof, there exists a cut-free $\mu
LK\bigcirc^{\omega}$ proof of the same conclusion.

###  4.2 $\mu LK\Box$: modal $\mu$-calculus

Secondly, we recall the infinite and the cyclic proof systems of the modal
$\mu$-calculus. Then, we prove that equivalence of those systems.

######  Definition 4.7 (Language for $\mu LK\Box$).

The formulas of $\mu LK\Box$ are defined as follows.

$F:=p\ |\ p^{\bot}\ |\ \bot\ |\ \top\ |\ F\lor G\ |\ F\land G\ |\ X\ |\ \mu
X.F\ |\ \nu X.F\ |\ \Box F\ |\ \Diamond F$

The negation is expanded by $(\Box F)^{\bot}=\Diamond F^{\bot}$ and $(\Diamond
F)^{\bot}=\Box F^{\bot}$. The Fischer-Ladner subformula relation is expanded
by $\Box F\to F$ and $\Diamond F\to F$.

######  Definition 4.8 (Rules for $\mu LK\Box$).

The inference rules for $\mu LK\Box$ are the rules in Figure 1 extended by the
following.

$\vdash F,\Gamma$ $(\Box)$ $\vdash\Box F,\Diamond\Gamma$

Here, for a finite set $\Gamma=\\{F_{1},\ldots,F_{n}\\}$ of formulas, we
define $\Diamond\Gamma$ as $\\{\Diamond F_{1},\ldots,\Diamond F_{n}\\}$.

As in the case of $\mu LK^{\infty},\mu LK^{\omega}$, we define the infinite
proof system $\mu LK\Box^{\infty}$ and the cyclic proof system $\mu
LK\Box^{\omega}$.

The proof of Theorem 3.2 can be adapted to $\mu LK\Box$ in a straightforward
way.

######  Lemma 4.9.

The Fischer-Ladner closure in $\mu\rm{LK\Box}^{\infty}$ is a finite set.

######  Lemma 4.10 (Subformula property for $\mu LK\Box^{\infty}$).

Every formula that appears in a cut-free $\mu LK\Box^{\infty}$ proof that
concludes $\vdash\Gamma$ is a Fischer-Ladner subformula of a formula contained
in $\Gamma$.

######  Theorem 4.11 (Equivalence between cut-free $\mu\rm{LK}\Box^{\infty}$
and cut-free $\mu\rm{LK}\Box^{\omega}$).

For any $\mu\rm{LK}\Box^{\infty}$-proof, there exists a
$\mu\rm{LK}\Box^{\omega}$ proof of the same conclusion.

Studer [13] has proved the cut-free completeness of the infinitary proof
system for $\mu LK\Box$, and hence the cut-elimination of $\mu
LK\Box^{\omega}$ follows as a corollary.

######  Corollary 4.12 (Cut-elimination of $\mu LK\Box^{\omega}$).

For any $\mu LK\Box^{\omega}$ proof, there exists a cut-free $\mu
LK\Box^{\omega}$ proof of the same conclusion.

##  5 Propositional logic with inductive definitions

In this chapter, we recall the proof systems of propositional logic with
inductive definitions introduced by Brotherston et al. [1, 5]. Then, we show
that Theorem 3.2 is applicable to these systems as well, and show the
equivalence of the provability between infinite proof systems and cyclic proof
systems.

###  5.1 Inference rules

In this section, we recall $\rm{LKID}^{\omega}_{prop}$ and
$\rm{CLKID}^{\omega}_{prop}$, which are the two-sided proof systems of the
propositional logic with inductive predicates. These are propositional
restrictions of $\rm{LKID}^{\omega}$ and $\rm{CLKID}^{\omega}$ [1, 5].

######  Definition 5.1 (Formulas).

We use metavariables $P,P_{1},\ldots$ for inductively defined proposition
symbols. The _formulas_ are defined as follows.

$F:=p\mid P\mid\neg F\mid F\land G\mid F\lor G\mid F\to G$

######  Definition 5.2 (Inductive definition set).

A _production_ $\phi$ of $P_{i}$ is of the following form.

$p_{1}\cdots p_{h}\ \ P_{j_{1}}\cdots P_{j_{m}}$ $P_{i}$

The _inductive definition set_ $\Phi$ is the finite set of productions.

In the following, we suppose a fixed inductive definition set $\Phi$. The
Fischer-Ladner subformula relation is extended by $P\to F$ for each $F$ that
appears as a premise in a production of $P$ in $\Phi$.

######  Lemma 5.3.

For a fixed inductive definition set, $FL(F)$ is finite for any formula $F$.

A sequent is an expression of the form $\Gamma\vdash\Delta$, where $\Gamma$
and $\Delta$ are finite sets of formulas. The inference rules for
$\rm{LKID}^{\omega}_{prop}$ and $\rm{CLKID}^{\omega}_{prop}$ are given in the
following.

Figure 3 shows the inference rules other than those for inductive definitions
in $\rm{LKID}^{\omega}_{prop}$ and $\rm{CLKID}^{\omega}_{prop}$.

Structural rules:
(Axiom)($\Gamma\cap\Delta\neq\emptyset$) $\Gamma\vdash\Delta$
$\Gamma^{\prime}\vdash\Delta^{\prime}$
(Weak)($\Gamma^{\prime}\subseteq\Gamma,\Delta^{\prime}\subseteq\Delta$)
$\Gamma\vdash\Delta$ $\Gamma\vdash F,\Delta$ $\Gamma,F\vdash\Delta$ (Cut)
$\Gamma\vdash\Delta$

Logical rules:
$\Gamma\vdash F,\Delta$ $(\neg\ \rm{L})$ $\Gamma,\neg F\vdash\Delta$
$\Gamma,F\vdash\Delta$ $(\neg\ \rm{R})$ $\Gamma\vdash\neg F,\Delta$
$\Gamma,F\vdash\Delta$ $\Gamma,G\vdash\Delta$ $(\lor\ \rm{L})$ $\Gamma,F\lor
G\vdash\Delta$ $\Gamma\vdash F,G,\Delta$ $(\lor\ \rm{R})$ $\Gamma\vdash F\lor
G\Delta$ $\Gamma,F,G\vdash\Delta$ $(\land\ \rm{L})$ $\Gamma,F\land
G\vdash\Delta$ $\Gamma\vdash F,\Delta$ $\Gamma\vdash G,\Delta$ $(\land\
\rm{R})$ $\Gamma\vdash F\land G,\Delta$ $\Gamma\vdash F,\Delta$
$\Gamma,G\vdash\Delta$ $(\to\rm{L})$ $\Gamma,F\to G\vdash\Delta$
$\Gamma,F\vdash G,\Delta$ $(\to\rm{R})$ $\Gamma\vdash F\to G,\Delta$

Figure 3: Inference rules except those for inductive definitions

Below are two rules regarding inductive definitions. First, for each
production

$p_{1}\cdots p_{h}\ \ P_{j_{1}}\cdots P_{j_{m}}$ $P_{i}$

in $\Phi$, there exists the rule

$\Gamma\vdash p_{1},\Delta\ \cdots\ \Gamma\vdash p_{h},\Delta\ \ \Gamma\vdash
P_{j_{1}},\Delta\ \cdots\ \Gamma\vdash P_{j_{m}},\Delta$ $(P_{i}\ \rm{R})$
$\Gamma\vdash P_{i},\Delta$

Next, we define a left rule for inductive definitions. The case distinction of
a sequent $\Gamma,P_{i}\vdash\Delta$ for the above production are defined as
the sequent

$\displaystyle\Gamma,p_{1},\cdots,p_{h},P_{j_{1}},\cdots,P_{j_{m}}\vdash\Delta$

The rule (Case $P_{i}$) is defined as

All case distinctions of $\Gamma,P_{i}\vdash\Delta$ for each production of
$P_{i}$ (Case $P_{i}$) $\Gamma,P_{i}\vdash\Delta$

###  5.2 ${\rm LKID}^{\omega}_{prop}$ and ${\rm CLKID}^{\omega}_{prop}$

We recall the infinitary proof system ${\rm LKID}^{\omega}_{prop}$ and the
cyclic proof system ${\rm CLKID}^{\omega}_{prop}$ [1].

######  Definition 5.4 ($\rm{LKID}^{\omega}_{prop}$ pre-proofs).

A $LKID^{\omega}_{prop}$ pre-proof is a possibly infinite tree, coinductively
generated by the rules in Figure 3, ($P_{i}$ R), and (Case $P_{i}$).

######  Definition 5.5 (Threads).

For a branch $B=(\Gamma_{i}\vdash\Delta_{i})_{i\in o}$ in a pre-proof
$\mathcal{D}$, define a _thread_ following $B$ as a sequence of inductively
defined propositional symbols $(F_{i})_{i\in o}$ that satisfies the following.

(1)

$F_{i}\in\Gamma_{i}$.

(2)

If $\Gamma_{i}\vdash\Delta_{i}$ is the conclusion of (Case $P_{i}$) and
$F_{i}=P_{i}$ is its principal formula, then $P_{i+1}$ is a premise of a
production of $P_{i}$. In this case, $P_{i}$ is called a _progress point_ in
the thread.

(3)

Otherwise, $F_{i}=F_{i+1}$.

######  Definition 5.6 (Validity condition).

We say that an infinite branch $B$ in a pre-proof is _valid_ if there exists a
thread following a tail of $B$ containing infinitely many progressing points.
A pre-proof satisfies the _validity condition_ if every infinite branch in the
pre-proof is valid.

Note that this condition is the same as the _global trace condition_ in [1,
5].

######  Definition 5.7 ($\rm{LKID}^{\omega}_{prop}$-proofs).

A $\rm{LKID}^{\omega}_{prop}$-proof is a pre-proof of
$\rm{LKID}^{\omega}_{prop}$ satisfying the validity condition.

The cyclic proof system $\rm{CLKID}^{\omega}_{prop}$ is defined in a similar
way to $\mu LK^{\omega}$.

######  Definition 5.8 ($\rm{CLKID}^{\omega}_{prop}$ pre-proof).

Define a $\rm{CLKID}^{\omega}_{prop}$ pre-proof as a pair
$(\mathcal{D},\mathcal{C})$ that satisfies the following.

(1)

$\mathcal{D}$ is a finite derivation tree in which non-axiom leaves, called
_buds_ , are allowed.

(2)

$\mathcal{C}$ is a function from each bud to its _companion_ such that the
sequents associated with the bud and the companion are the same.

######  Definition 5.9 ($\rm{CLKID}^{\omega}_{prop}$ proof).

We define the $\rm{CLKID}^{\omega}$ proof of the sequent $\Gamma\vdash\Delta$
as a $\rm{CLKID}^{\omega}$ pre-proof such that all infinite branches of those
graph are valid.

###  5.3 Equivalence between cut-free ${\rm LKID}^{\omega}_{prop}$ and cut-
free ${\rm CLKID}^{\omega}_{prop}$

Lemma 3.3 also holds for ${\rm LKID}^{\omega}_{prop}$.

######  Lemma 5.10.

Let $\pi$ be an infinite proof, $B=(\Gamma_{i}\vdash\Delta_{i})_{i\in\omega}$
be an infinite branch in $\pi$, and $\Gamma_{j}\vdash\Delta_{j}$ be a node on
$B$. If ${\rm Seq}(B)$ is finite, there exist $b,c\in\omega$ that satisfies
the following.

(1)

$j\leq c<b$.

(2)

$\Gamma_{b}=\Gamma_{c}$.

(3)

The infinite branch
$\vdash\Gamma_{0},\ldots,\vdash\Gamma_{c},\vdash\Gamma_{c+1},\ldots,\Gamma_{b}=\Gamma_{c},\Gamma_{c+1},\ldots$
is valid.

###### Proof.

It is proved similarly to Lemma 3.3. We can find $b$ and $c$ such that there
exists a progress point on the thread, and then the branch with the loop
between $c$ and $b$ is valid. ∎

The subformula property holds for cut-free ${\rm LKID}^{\omega}$-proofs.

######  Lemma 5.11 (Subformula property for ${\rm LKID}^{\omega}$).

Every formula that appears in a cut-free ${\rm LKID}^{\omega}$ proof of
$\Gamma\vdash\Delta$ is a Fischer-Ladner subformula of a formula contained in
$\Gamma$ or $\Delta$.

By Lemma 5.3, Lemma 5.10, and Lemma 5.11, the equivalence of ${\rm
LKID}^{\omega}_{prop}$ and ${\rm CLKID}^{\omega}_{prop}$ is proved.

######  Theorem 5.12 (Equivalence between cut-free ${\rm
LKID}_{prop}^{\omega}$ and cut-free ${\rm CLKID}_{prop}^{\omega}$).

For any cut-free ${\rm LKID}_{prop}^{\omega}$ proof, there exists a cut-free
${\rm CLKID}_{prop}^{\omega}$ proof of the same conclusion.

By the cut-free completeness of ${\rm LKID}^{\omega}$ [1, 5], the cut-
elimination property of ${\rm CLKID}^{\omega}$ follows.

######  Corollary 5.13 (Cut-elimination of ${\rm CLKID}^{\omega}$).

For any ${\rm CLKID}_{prop}^{\omega}$ proof, there exists a cut-free
$CLKID_{prop}^{\omega}$ proof of the same conclusion.

##  6 Conclusion

In this study, we have proved that every infinite proof can be translated to a
cyclic proof if any infinite branch of the infinite proof contains only
finitely many sequents. We have also proved the equivalence between the cut-
free infinite proof systems and corresponding cyclic proof systems for some
propositional logics, including the propositional logic with fixed-point
operators, the linear temporal logic with fixed-point operators, the modal
$\mu$-calculus, and the propositional logic with inductive definitions.

One interesting future direction is to adapt our proof to the first-order
logic with restricted languages. It has been proved [11] that the cut
elimination does not hold for ${\rm CLKID}^{\omega}$. The counterexample
contains a function symbol, which easily violates the finiteness condition of
Lemma 3.3. We guess that if the language is restricted to only 1-ary
predicates and there are no function symbols, the finiteness condition always
holds for the infinite proofs, and the cut-free ${\rm LKID}^{\omega}$ and the
cut-free ${\rm CLKID}^{\omega}$ are equivalent.

## References

  * [1] J. Brotherston.  Sequent calculus proof systems for inductive definitions.  PhD thesis, University of Edinburg, 2006.
  * [2] J. Brotherston, R. Bornat, and C. Calcagno.  Cyclic proofs of program termination in separation logic.  ACM SIGPLAN Notices, 43(1):101–112, 2008.
  * [3] J. Brotherston, D. Distefano, and R. L. Petersen.  Automated cyclic entailment proofs in separation logic.  In 23rd international conference on automated deduction (CADE-23), volume 6803 of Lecture Notes in Artificial Intelligence (LNAI), pages 131–146, 2011.
  * [4] J. Brotherston, N. Gorogiannis, and R. L. Petersen.  A generic cyclic theorem prover.  In 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), volume 7705 of Lecture Notes in Computer Science (LNCS), pages 350–367, 2012.
  * [5] J. Brotherston and A. Simpson.  Sequent calculi for induction and infinite descent.  Journal of Logic and Computation, 21(6):1177–1216, 2011.
  * [6] A. Das, A. De, and A. Saurin.  Decision problems for linear logic with least and greatest fixed points.  In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1–20:20, 2022.
  * [7] C. Dax, M. Hofmann, and M. Lange.  A proof system for the linear time $\mu$-calculus.  In 26th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2006), volume 4337 of Lecture Notes in Computer Science (LNCS), pages 274–285, 2006.
  * [8] A. Doumane.  On the infinitary proof theory of logics with fixed points.  PhD thesis, Paris 7, 2017.
  * [9] M.J. Fischer and R.E. Ladner.  Propositional dynamic logic of regular programs.  Journal of Computing and System Science, 18(2):194–211, 1979.
  * [10] D. Kimura, K. Nakazawa, T. Terauchi, and H. Unno.  Failure of cut-elimination in cyclic proofs of separation logic.  Comupter Software, 37(1):39–52, 2020.
  * [11] Y. Masuoka and M. Tatsuta.  Counterexample to cut-elimination in cyclic proof system for first-order logic with inductive definitions.  Available at `https://arxiv.org/abs/2106.11798`, 2021.
  * [12] K. Saotome, K. Nakazawa, and D. Kimura.  Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions.  In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), volume 195 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1–11:14, 2021.
  * [13] T. Studer.  On the proof theory of the modal mu-calculus.  Studia Logica, 89(3):343–363, 2008.
  * [14] M. Tatsuta, K. Nakazawa, and D. Kimura.  Completeness of cyclic proofs for symbolic heaps with inductive definitions.  In The 17th Asian Symposium on Programming Languages and Systems (APLAS 2019), volume 11893 of Lecture Notes in Computer Science (LNCS), pages 367–387, 2019.


# Background resilient quantitative phase microscopy using entangled photons

Yingwen Zhang<EMAIL_ADDRESS>Nexus for Quantum Technologies, University
of Ottawa, Ottawa ON Canada, K1N6N5  National Research Council of Canada, 100
Sussex Drive, Ottawa ON Canada, K1A0R6  Joint Centre for Extreme Photonics,
National Research Council and University of Ottawa, Ottawa, Ontario, Canada
Paul-Antoine Moreau<EMAIL_ADDRESS>Department of Physics, National
Cheng Kung University, Tainan, 70101, Taiwan  Center for Quantum Frontiers of
Research and Technology, NCKU, Tainan, 70101, Taiwan  Duncan England  National
Research Council of Canada, 100 Sussex Drive, Ottawa ON Canada, K1A0R6
Ebrahim Karimi  Nexus for Quantum Technologies, University of Ottawa, Ottawa
ON Canada, K1N6N5  National Research Council of Canada, 100 Sussex Drive,
Ottawa ON Canada, K1A0R6  Joint Centre for Extreme Photonics, National
Research Council and University of Ottawa, Ottawa, Ontario, Canada  Benjamin
Sussman  National Research Council of Canada, 100 Sussex Drive, Ottawa ON
Canada, K1A0R6  Nexus for Quantum Technologies, University of Ottawa, Ottawa
ON Canada, K1N6N5  Joint Centre for Extreme Photonics, National Research
Council and University of Ottawa, Ottawa, Ontario, Canada

###### Abstract

In this work, we introduce a quantum-based quantitative phase microscopy
technique using a phase gradient approach that is inherently background
resistant and does not rely on interferometry or scanning. Here, a transparent
sample is illuminated by both photons of a position-momentum entangled pair
with one photon setup for position measurement in the near-field (NF) of the
sample and its partner for momentum measurement in the far-field (FF). By
virtue of the spatial correlation property inherent to the entanglement, both
the position and momentum information of the photons can thus be obtained
simultaneously. The phase profile of the sample is then deduced through a
phase gradient measurement obtained by measuring the centroid shift of the
photons’ in the FF momentum plane for each NF position. We show that the
technique, while achieving an imaging resolution of 2.76 $\mu$m, is phase
accurate to at least $\lambda/30$ and phase sensitive to $\lambda/100$ at a
wavelength of 810 nm. In addition, through the temporal correlation between
the photon pairs, our technique shows resilience to strong dynamic background
lights, which can prove difficult to account for in classical phase imaging
techniques. We believe this work marks a significant advancement in the
capabilities of quantum phase microscopy and quantum imaging in general, it
showcases imaging and phase resolutions approaching those attainable with
classical phase microscopes. This advancement brings quantum imaging closer to
practical real-world applications, heralding new possibilities in the field.

##  I Introduction

Utilizing the properties of quantum entangled photons for sensing and imaging
applications has been an active area of research in recent decades Genovese
(2016); Berchera and Degiovanni (2019); Moreau  _et al._ (2019); Degen  _et
al._ (2017); Pirandola  _et al._ (2018). Quantum light offers a range of
potential advantages over its classical counterpart in these applications,
this includes super-resolution Tsang (2009); Shin  _et al._ (2011); Rozema
_et al._ (2014); Unternährer  _et al._ (2018); Tenne  _et al._ (2019),
robustness against noise Brida  _et al._ (2010); Samantaray  _et al._ (2017);
Zhang  _et al._ (2020); Defienne  _et al._ (2021a); Zhao  _et al._ (2022), and
additional functionalities such as immunity to dispersion Nasr  _et al._
(2003); Yepiz-Graciano  _et al._ (2022), hyperspectral imaging Zhang  _et al._
(2023) and 3D imaging Ndagano  _et al._ (2022); Zhang  _et al._ (2022, 2024).

The use of entangled photons has also been extended to phase imaging. Phase
imaging plays a pivotal role in revealing with enhanced clarity, the subtle
variations in the optical path length of light passing through a transparent
sample and has found widespread usage in biomedical science Park  _et al._
(2018); Micó  _et al._ (2019); Nguyen  _et al._ (2022). Interferometry based
quantum phase retrieval techniques includes the use of photonic N00N states
Ono  _et al._ (2013); Israel  _et al._ (2014) and the interference between
successive laser passes of spontaneous parametric down-conversion (SPDC)
events Black  _et al._ (2023). Phase imaging has also been demonstrated
through holography with entangled photons Defienne  _et al._ (2021b);
Thekkadath  _et al._ (2023). Non-interference methods includes ghost imaging
approaches Abouraddy  _et al._ (2004), the use of transport of intensity
equation between intensity images obtained from different image planes Lu  _et
al._ (2015); Ortolano  _et al._ (2023) and through the simultaneous
measurement of the position and momentum information of photons through a
Fourier Ptychography approach Aidukas  _et al._ (2019) and differential phase
gradient approach Hodgson  _et al._ (2023). These techniques offers various
advantages such as sub-shot-noise sensitivity Ono  _et al._ (2013); Israel
_et al._ (2014); Ortolano  _et al._ (2023); Lu  _et al._ (2015), strong
background-noise tolerance Aidukas  _et al._ (2019); Defienne  _et al._
(2021b) and ease of use, such as phase stability Thekkadath  _et al._ (2023)
or allowing scanning-free measurement compared to the classical counterpart
Hodgson  _et al._ (2023).

In this study, we introduce a proof-of-concept demonstration showcasing a
quantum-based quantitative phase microscopy technique using a phase gradient
approach utilizing position-momentum entangled photons. The technique is shown
to be resilient to the influence of background light and it does not rely on
interferometry or scanning making it phase stable and requires no moving
parts. As a property of position-momentum entanglement, a photon pair is
correlated in position and anti-correlated in momentum, thus by measuring the
position/momentum of one photon, one can deduce the position/momentum of the
partner photon through the correlation property. By having both photons
jointly illuminate a phase target then capturing one photon in the near-field
(NF) plane of the target, which contains the photon’s position information,
and capturing the partner in the far-field (FF) plane, which contains the
photon’s momentum information, both the position and momentum of the photon
pairs can be acquired simultaneously. Next, using the relationship linking the
phase gradient at a NF position with a corresponding centroid shift of the
photons’ location in the FF, we can quantitatively recover the phase profile
of the target. This initial demonstration showcases an imaging resolution of
2.76 $\mu$m or 362 line pairs per mm while being phase accurate to at least
$\lambda$/30 and phase sensitive to $\lambda/100$ at a wavelength of 810 nm.
In addition, through utilizing the temporal correlation between the entangled
photons, we also demonstrate the technique’s resilience against a strong
dynamic background that fluctuates with space and time. This type of
background can be especially challenging to correct for in classical phase
imaging techniques.

Compared to earlier works exploiting position-momentum entangled photon pairs
for phase measurement Aidukas  _et al._ (2019); Hodgson  _et al._ (2023),
here, a different technique is used to extract the phase with significant
improvements in both sensitivity and accuracy. This has allowed us to achieve
imaging and phase resolutions close to that of classical phase microscopes
demonstrating that our technique could readily be used for real world
microscopy applications that requires low light levels or working under
complex background lighting conditions. This is exemplified by the acquisition
of the phase and amplitude images of biological cells.

##  II Experimental Setup

Figure 1: Experimental setup of quantum phase microscope (a) Spatially
entangled photon pairs with orthogonal polarization are generated through a
Type II ppKTP crystal. After illuminating the target, the photon pairs are
separated with a PBS such that the NF and FF of the target can be imaged
separately by the signal and idler photons respectively. PBS: polarizing
beamsplitter, LP filter: longpass filter, BP filter: bandpass filter, ppKTP:
periodically-poled potassium titanyl phosphate crystal. (b) Brightfield image
of a phase target with 200 nm feature height captured by the time-tagging
camera. A time correlation measurement to identify photon pairs is then
performed between all photons captured within the two highlighted circular
regions. For viewing clarity, the idler beam shown here is scaled to be 50
times dimmer than measured to allow the signal beam to be visible in the same
image. (c) Image formed by all idler photons in the FF that are detected in
coincidence with signal photons that passed through the indicated NF pixel.
(d) A reference idler photon image captured for the same NF pixel with no
phase target in place. A centroid measurement is performed on each FF image
for all NF pixels. Here the centroid for (c), indicated by the yellow
crosshair, is shown relative to the centroid of the reference (d), indicated
by the red crosshair.

The setup of our quantum phase microscope is depicted in Fig. 1. A 20 mW, 405
nm continuous-wave (CW) laser, with a 1 mm beam diameter, is used to pump a 1
mm thick Type II periodically-poled potassium titanyl phosphate (ppKTP)
crystal to generate, through the process of spontaneous parametric down-
conversion (SPDC), orthogonally polarized photon pairs at 810 nm that are
correlated in time and entangled in the position-momentum degrees of freedom.
The photon pairs are directed through a 4f-imaging system to illuminate a
phase target placed in the NF plane of the nonlinear crystal. The photons are
then separated using a polarizing beamsplitter. The NF of the phase target is
imaged onto a time-tagging camera (TPX3CAM Nomerotski (2019); ASI ) through
the signal photons, while the FF of the target is projected onto a corner of
the camera through a separate path using the idler photons. To identify photon
pairs, time correlation measurement is conducted with a coincidence window of
20 ns. Because the photons are position-momentum entangled, we can infer the
momentum of each signal photon detected at a NF position from the partnered
idler photon, whose momentum is measured in the FF. Thus, 5-dimensional
information, in time, position and momentum, is obtained for each photon.

To extract the phase information from a target that introduces a phase
$\phi(x,y)$ to the photons, we determine the photons’ mean propagation
direction, given by the phase gradient
$\vec{\theta}(x,y)=\vec{\nabla}[\phi(x,y)+\phi_{0}(x,y)]$, where
$\phi_{0}(x,y)$ represents the photons’ initial phase profile. Through a lens,
this directional angle $\vec{\theta}(x,y)$ is directly measured as a position
$\vec{k}(x,y)\approx f\vec{\theta}(x,y)$ in the FF (under the paraxial
approximation), with $f$ representing the lens focal length.

After detecting numerous photon pairs, we calculate the centroid position in
each direction of $\vec{k}=u\hat{u}+v\hat{v}$ for all idler photons detected
in the FF that are time-correlated with signal photons detected at position
$(x,y)$ in the NF. That is

$\displaystyle\mathscr{U}(x,y)$
$\displaystyle=\frac{1}{N(x,y)}\sum_{n=1}^{N(x,y)}u_{n}(x,y)$
$\displaystyle\mathscr{V}(x,y)$
$\displaystyle=\frac{1}{N(x,y)}\sum_{n=1}^{N(x,y)}v_{n}(x,y),$ (1)

where $\mathscr{U}(x,y)$ and $\mathscr{V}(x,y)$ represent the centroid
positions in the $\hat{u}$ and $\hat{v}$ directions for all idler photons
temporally correlated with signal photons at position $(x,y)$ in the NF, and
$N(x,y)$ is the number of photon pairs detected at position $(x,y)$ in the NF.

The expectation value of the phase gradient $\vec{\nabla}\phi(x,y)$ is then

$\begin{pmatrix}\langle\frac{\partial\phi(x,y)}{\partial x}\rangle\\\
\langle\frac{\partial\phi(x,y)}{\partial
y}\rangle\end{pmatrix}=\frac{1}{f}\begin{pmatrix}\mathscr{U}(x,y)-\mathscr{U}_{0}(x,y)\\\
\mathscr{V}(x,y)-\mathscr{V}_{0}(x,y)\end{pmatrix},$ (2)

with $\mathscr{U}_{0}(x,y)$ and $\mathscr{V}_{0}(x,y)$ representing the
reference centroid positions obtained without the phase target.

Finally, the phase $\phi(x,y)$ is reconstructed by solving the two-dimensional
partial differential equations $\frac{\partial\phi(x,y)}{\partial x}$ and
$\frac{\partial\phi(x,y)}{\partial y}$. For this we use the Frankot and
Chellappa method Frankot and Chellappa (1988); Gong  _et al._ (2017)

$\phi(x,y)=\mathscr{F}^{-1}\left[\frac{u\mathscr{F}\left[\frac{\partial\phi(x,y)}{\partial
x}\right]+v\mathscr{F}\left[\frac{\partial\phi(x,y)}{\partial
y}\right]}{i(u^{2}+v^{2})}\right],$ (3)

where $\mathscr{F}[\cdot]$ and $\mathscr{F}^{-1}[\cdot]$ represent the Fourier
and inverse Fourier transform, respectively. A derivation of this relation can
be found in the Supplementary.

Before conducting these measurements with the phase target, a one-time
reference measurement without the phase target in place is performed to
determine $\phi_{0}(x,y)$. Note that background contributions has not been
taken into account in eq. 1, see the Supplementary on the modifications
required for background correction.

##  III Experimental Results

###  III.1 Quantitative phase measurement

Figure 2: Results from imaging resolution phase targets (a, b) Recovered phase
images for a Star (a) and 1951 USAF (b) resolution phase target with 200 nm
feature height. The corresponding measured phase gradient in the horizontal
and vertical direction used to recover the phase image are shown in (a1, b1)
and (a2, b2) respectively. (c) Cross-section from, 0 to 100 degrees, of the
yellow highlighted regions of (a) compared to an ideal phase measurement of
this target. (d) Measured phase (blue square) and NRMSE (red circle) as a
function of the target thickness for the Star target. The phase is measured as
the mean difference between the maxima and minima in the cross-section of the
yellow highlighted regions as indicated in (a) and NRMSE compares the
similarity between the measured phase profile to that of the ideal profile as
shown in (c). The bright field image of the Star phase target can be seen in
Fig. 4 and the full cross-sections can be found in the Supplementary. The
measured phase of the USAF target can also be found in the Supplementary. Data
acquisition time for all images shown in this and subsequent figures is 500 s.
Background contributions has been corrected for in all results shown.

To calibrate the accuracy of the phase recovery process we used quantitative
phase targets (from Benchmark technologies Ben ) with feature heights ranging
from 50 nm to 350 nm, with two different patterns, the star and 1951 USAF.
Measuring the average peak-to-peak phase difference in the patterns, we find
the method is accurate from a target thickness of 50 nm, or $\sim\lambda$/30
at 810 nm (the phase difference between 50 nm of glass and air) up to 200 nm,
or $\lambda$/8. The smallest spatial feature observed in the microscope is
group 8-4 of the 1951 USAF target, which corresponds to resolving line pairs
separated by 2.76 $\mu$m. The results for this are shown in Fig. 2. Based on
the uncertainties in the phase measurement of approximately 0.06 rad, we would
expect the technique to still be phase sensitive at approximately
$\lambda$/100. The uncertainties in the phase measurement can be reduced with
a longer data acquisition time or with a higher efficiency camera which will
allow for even better phase accuracy and sensitivity, a more detailed
discussion on this is given in the Discussions section. Note that we are not
yet imaging at the diffraction limit of the imaging system, which given the
numerical aperture of the lens arrangement is expected to be $\sim 1$ $\mu$m.
This is a result of the large pixel size of the camera ($55$ $\mu$m) limiting
the achievable resolution.

As a measure of the similarity between the recovered phase profile and that of
an ideal phase profile, which has a constant phase across the target features,
we determine the normalized root mean squared error (NRMSE) between the two
phase profiles which is defined as

$\text{NRMSE}=\frac{\sqrt{\frac{1}{N}\sum_{i=1}^{N}(O_{i}-E_{i})^{2}}}{\bar{E}},$
(4)

where $O_{i}$ and $E_{i}$ are the observed and expected values, respectively.
$\bar{E}$ is the mean of the expected values. For better statistics we
determined the NRMSE only for the cross-section of the star target. The NRMSE
for the Star targets of different heights are shown as red circles in Fig.
2(d).

From the results, we see that the NRMSE deteriorates for both smaller and
larger feature heights. This outcome aligns with expectations. Smaller feature
heights amplify the influence of background noise in relation to the subtle
phase profile. For larger feature heights, the discrepancies between the
measured and ideal phase profile can be due to a number of reasons. One is
that the large phase jump will cause a very large phase gradient that
diffracts photons to outside the numerical aperture of the FF imaging system,
resulting in measuring a smaller centroid shift. The other being the linear
relationship between the phase gradient and the FF centroid shift no longer
holds for larger diffraction angles, due to the paraxial approximation being
no longer valid. Therefore, the method is most accurate for targets that does
not contain phase jumps of over 250 nm. It should be noted here that our
analysis did not account for manufacturing irregularities in the quantitative
phase targets which may exhibit deviations of up to 10% from the specified
values, as stipulated by the manufacturer.

Lastly, in Fig. 3 we show the phase imaging of cheek epithelial cells where a
refractive index of 1.35 Gul  _et al._ (2021) was assumed for the cells for
estimating the thickness. We note that the Lapacian of the phase image, Fig.
3(d), can also be used to display features in the cells with a much better
contrast as compared to the brightfield image as seen in Fig. 3(e).

Figure 3: Results of imaging cheek epithelial cells (a) Phase image of cheek
epithelial cells. (b, c) The measured phase gradient in the horizontal and
vertical direction for recovering the phase image (a). (d) The Laplacian of
the phase. (e) Image of the cells captured directly by the camera as if
through a conventional bright-field microscope.

###  III.2 Background mitigation

Figure 4: Results demonstrating background mitigation (a1, b1, c1) NF and FF
images obtained through direct imaging of the phase target with 200 nm feature
heights when (a1) no background light is applied, (b1) a dynamic background
light with approximately half the number of photons as compared to SPDC is
added and (c1) when the dynamic background has approximately equal amount of
photons as SPDC. (a2, b2, c2) NF and FF images after a time correlation
measurement has been made to identify the photon pairs. It can be seen that a
substantial amount of background light has been removed. (a3, b3, c3)
Recovered phase image without applying background correction. (a4, b4, c4)
Recovered phase images after background correction. The cross-section for all
phase images can be found in the supplementary materials.

Quantitative phase imaging techniques are highly susceptible to the influence
of background light. Addressing the background typically involves either
separately measuring the background light or applying Fourier filtering
techniques, which require some prior knowledge of the background
characteristics. These methods are often limited in their effectiveness,
especially against a dynamic backgrounds which fluctuates with space and time.

Here, we simulate the effect of a dynamic background by introducing
numerically generated photon detection events from a Gaussian shaped beam
profile into the raw camera data, both in the NF and FF. The properties of
this background, including its intensity, width, and position, were all
randomized over time. Refer to the Supplementary for more details on the
background generation.

We demonstrate that, regardless of the background type, our approach of
utilizing SPDC photons offers a robust two-stage process to mitigate the
impact of background light. The first stage relies on the coincident detection
of photon pairs, this intrinsically provides background suppression as only
photons arriving in the correct temporal window are included in the
coincidence image. This type of background suppression, common to many imaging
schemes based on entangled pairs England  _et al._ (2019); Zhao  _et al._
(2022), is visually apparent when comparing Fig. 4(b1,c1) and (b2,c2).

However, even after coincidence detection, an uncorrelated background remains
due to photons that accidentally arrive within the coincidence window despite
not being generated in the same SPDC event. These are due to accidental
coincidences between a SPDC photon and a background photon, two background
photons, or two SPDC photons belonging to different pair events. In the second
stage, the rate of accidental coincidences are measured by selecting a
coincidence window that is outside of the true coincidence window, in this
case, 50 ns before it. The contribution of background coincidences can then be
subtracted from the the centroid shift to mitigate the effect of a dynamic
background on the recovered phase profile. Refer to the Supplementary for more
details on the detection and subtraction of background light.

For weak background light, the dominant contribution in the background
coincidences originates from the coincidences between different SPDC pairs
generated within the coincidence window in which no spatial entanglement
exists. Thus, the resultant background idler images will show no centroid
shift. Consequently, the phase image in cases where this term is not
subtracted will closely resemble the background-corrected phase image, albeit
with a slightly smaller measured phase, as shown in Fig. 4(a). In Fig. 4(a3),
for the star pattern having 200 nm feature heights and an expected phase of
0.81, the average measured phase without background-correction is $0.56\pm
0.04$, whereas in the background-corrected image, as seen in Fig. 4(a4), the
measured phase is $0.74\pm 0.06$. The NRMSE is 0.62 for the background-
corrected image and 0.69 for the uncorrected image. The difference can be seen
more clearly in the cross-section of the phase target shown in the
Supplementary.

In contrast, for strong backgrounds, a centroid shift will be introduced in
the background idler image whenever the background light does not fall in the
center of the detection area of the FF. This can be observed in Fig. 4(b3, c3)
where strong distortions are seen in the recovered phase image. After
background correction, our technique is able to recover the phase image with
relatively good accuracy with a measured phase of $0.73\pm 0.08$ and a NRMSE
of 0.77 for (b4), where the total background photons is approximately half the
number of SPDC photons. For Fig. 4(c4), where the total background photons is
approximately equal to the number of SPDC photons, a phase of $0.68\pm 0.12$
and a NRMSE of 2.0 is obtained.

###  III.3 Reduced far-field resolution

Since the phase recovery method is based on FF centroid shift, in principle, a
high-resolution camera is not necessarily needed to perform the FF
measurement. The centroid measurement can be performed with a resolution of
just 2$\times$2 pixels in the FF. Practically, this can be implemented by
using a quandrant avalanche photodiode detector.

Here we demonstrate this in Fig. 5 by applying a 30$\times$30 binning to the
idler photon positions detected on the camera. i.e. $\lceil(u,v)/30\rceil$
where $(u,v)$ are the pixel position of the detected idler photon and
$\lceil\cdot\rceil$ is the ceiling operation. The phase images obtained
through 30$\times$30 binning are quantitatively similar to those obtained at
full resolution as seen in Fig. 2. However the reduced FF spatial resolution
results in a larger uncertainty (by between 20$\%$ to 70$\%$ depending on the
size of the phase jump), and increased NRMSE (by approximately 10% on
average). With 2$\times$2 pixel FF resolution, though less accurate in the
phase measurement, as a result, becomes more tolerant to background
influences. In Fig. 5(b), when a 30$\times$30 binning is applied to the FF
detector on the same dataset used in Fig.4(c), a much better background
tolerance is observed. A NRSME of 1.0 is obtained in Fig. 5(b) compared to 2.0
for Fig.4(c4).

This demonstrates another versatility of our technique, in that it can be
switched, all in post-processing, from having better phase accuracy to better
background tolerance, depending on the requirement.

Figure 5: Results from 2$\times$2 pixels FF resolution (a) Recovered phase
images for a Star and 1951 USAF resolution phase target with 200 nm feature
heights using 2$\times$2 pixels FF resolution. (b) Recovered phase images for
a Star resolution phase target with 200 nm feature heights before and after
background correction using 2$\times$2 pixels FF resolution. The background to
SPDC photon ratio is $\sim$1:1. A full comparison with the results of Fig. 2
and 4 can be found in the Supplementary.

##  IV Discussion

In summary, by utilizing the inherent correlations of position-momentum
entangled photons, we demonstrated a scaning-free, non-interferometric
quantitative phase microscopy technique which is inherently resilient to the
influence of background light. This approach allows for the simultaneous
measurement of the position and momentum of photons diffracted from a phase
target, facilitating the reconstruction of the target’s phase profile via a
phase gradient method. This initial demonstration achieved an imaging
resolution of 2.76 $\mu$m or 362 line pairs per mm with the phase measurement
tested to be accurate at $\lambda/30$ at a wavelength of 810 nm and is phase
sensitive to $\lambda/100$. Additionally, through taking advantage of the
temporal correlation between the photon pairs, we show that the phase image of
a target can still be recovered with good accuracy under a strong, dynamic
background. Lastly, our technique has the versatility to be switched, all in
post-processing, from having better phase accuracy to better background
tolerance by changing the effective FF resolution for momentum measurements.
Though we demonstrated phase microscopy using this technique, it can also be
used as a wavefront sensor for adaptive optics.

Our technique bears the closest classical resemblance to the Shack-Hartmann
(SH) wavefront sensor Shack (1971). The SH sensor employs a microlens array to
capture both the position and momentum attributes of incident light rays,
subsequently utilizing this data to deduce the phase information via phase
gradient measurements. Though more commonly used in the field of adaptive
optics Tyson and Frazier (2022), the SH sensor has also been demonstrated for
use in quantitative phase microscopy Gong  _et al._ (2017). Nevertheless, our
quantum method offers numerous advantages beyond its robustness against
background light. Most notably it obviates the need for microlens arrays,
thereby mitigating several challenges inherent to SH sensors. Firstly, a SH
sensor requires a total of $N_{n}\times N_{f}$ pixels, with $N_{n}$ and
$N_{f}$ being the NF and FF pixel resolution respectively, while our quantum
technique only requires $N_{n}+N_{f}$ pixels. Secondly, we circumvent the
issue of cross-talk between pixels situated behind neighboring microlenses, a
common problem encountered in SH sensors when encountering large phase
gradient, leading to overlapping FF beams beneath adjacent microlenses.
Lastly, our technique employs standard 1- and 2-inch diameter lenses, which
can be constructed with much higher quality compared to the less-ideal shape
of microlens arrays and is less prone to misalignment, thus reducing the
occurrence of aberrations Pfund  _et al._ (1998); Chernyshov  _et al._ (2005).

Other similar classical non-interferometric phase imaging techniques that
involve imaging both the NF and FF includes Ptychography Rodenburg and Maiden
(2019) and the Gerchberg-Saxton (GS) algorithm Gerchberg (1972). However,
Ptychography requires scanning of the NF and the GS algorithm is not always
convergent, our quantum technique does not have either of these two short
comings.

The data acquisition speed of our technique is currently limited by the
available camera technology. Our camera system exhibits a quantum efficiency
of approximately 7%, an 8 ns time-resolution, and a maximum photon detection
rate of approximately $10^{7}$ photons per second, as detailed in Vidyapin
_et al._ (2023). A seven-fold improvement in each of the three camera
parameters mentioned above could potentially reduce the required data
acquisition time to a second. Such enhancements would not only expedite data
collection but also significantly enhance the phase sensitivity and accuracy
of the technique due to an increased coincidence rate. Considering the rapid
advancements in single-photon detection technology witnessed in recent years,
the prospect of developing time-tagging single-photon cameras meeting these
specifications appears to be within reach in the near future.

During the submission of this work, we are made aware of a work using a
similar phase gradient approach but using a SH sensor instead of a time-
tagging camera for the measurement of biphoton spatial wave function Zheng
_et al._ (2024).

## References

  * Genovese (2016) M. Genovese, Journal of Optics 18, 073002 (2016).
  * Berchera and Degiovanni (2019) I. R. Berchera and I. P. Degiovanni, Metrologia 56, 024001 (2019).
  * Moreau  _et al._ (2019) P.-A. Moreau, E. Toninelli, T. Gregory, and M. J. Padgett, Nature Reviews Physics 1, 367 (2019).
  * Degen  _et al._ (2017) C. L. Degen, F. Reinhard, and P. Cappellaro, Rev. Mod. Phys. 89, 035002 (2017).
  * Pirandola  _et al._ (2018) S. Pirandola, B. R. Bardhan, T. Gehring, C. Weedbrook, and S. Lloyd, Nature Photonics 12, 724 (2018).
  * Tsang (2009) M. Tsang, Phys. Rev. Lett. 102, 253601 (2009).
  * Shin  _et al._ (2011) H. Shin, K. W. C. Chan, H. J. Chang, and R. W. Boyd, Phys. Rev. Lett. 107, 083603 (2011).
  * Rozema  _et al._ (2014) L. A. Rozema, J. D. Bateman, D. H. Mahler, R. Okamoto, A. Feizpour, A. Hayat, and A. M. Steinberg, Phys. Rev. Lett. 112, 223602 (2014).
  * Unternährer  _et al._ (2018) M. Unternährer, B. Bessire, L. Gasparini, M. Perenzoni, and A. Stefanov, Optica 5, 1150 (2018).
  * Tenne  _et al._ (2019) R. Tenne, U. Rossman, B. Rephael, Y. Israel, A. Krupinski-Ptaszek, R. Lapkiewicz, Y. Silberberg, and D. Oron, Nature Photonics 13, 116 (2019).
  * Brida  _et al._ (2010) G. Brida, M. Genovese, and I. Ruo Berchera, Nature Photonics 4, 227 (2010).
  * Samantaray  _et al._ (2017) N. Samantaray, I. Ruo-Berchera, A. Meda, and M. Genovese, Light: Science & Applications 6, e17005 (2017).
  * Zhang  _et al._ (2020) Y. Zhang, D. England, A. Nomerotski, P. Svihra, S. Ferrante, P. Hockett, and B. Sussman, Phys. Rev. A 101, 053808 (2020).
  * Defienne  _et al._ (2021a) H. Defienne, J. Zhao, E. Charbon, and D. Faccio, Phys. Rev. A 103, 042608 (2021a).
  * Zhao  _et al._ (2022) J. Zhao, A. Lyons, A. C. Ulku, H. Defienne, D. Faccio, and E. Charbon, Opt. Express 30, 3675 (2022).
  * Nasr  _et al._ (2003) M. B. Nasr, B. E. A. Saleh, A. V. Sergienko, and M. C. Teich, Phys. Rev. Lett. 91, 083601 (2003).
  * Yepiz-Graciano  _et al._ (2022) P. Yepiz-Graciano, Z. Ibarra-Borja, R. Ramírez Alarcón, G. Gutiérrez-Torres, H. Cruz-Ramírez, D. Lopez-Mago, and A. B. U’Ren, Phys. Rev. Applied 18, 034060 (2022).
  * Zhang  _et al._ (2023) Y. Zhang, D. England, and B. Sussman, Opt. Express 31, 2282 (2023).
  * Ndagano  _et al._ (2022) B. Ndagano, H. Defienne, D. Branford, Y. D. Shah, A. Lyons, N. Westerberg, E. M. Gauger, and D. Faccio, Nature Photonics 16, 384 (2022).
  * Zhang  _et al._ (2022) Y. Zhang, A. Orth, D. England, and B. Sussman, Phys. Rev. A 105, L011701 (2022).
  * Zhang  _et al._ (2024) Y. Zhang, D. England, A. Orth, E. Karimi, and B. Sussman, Phys. Rev. Appl. 21, 024029 (2024).
  * Park  _et al._ (2018) Y. Park, C. Depeursinge, and G. Popescu, Nature Photonics 12, 578 (2018).
  * Micó  _et al._ (2019) V. Micó, J. Zheng, J. Garcia, Z. Zalevsky, and P. Gao, Adv. Opt. Photon. 11, 135 (2019).
  * Nguyen  _et al._ (2022) T. L. Nguyen, S. Pradeep, R. L. Judson-Torres, J. Reed, M. A. Teitell, and T. A. Zangle, ACS Nano 16, 11516 (2022), pMID: 35916417, https://doi.org/10.1021/acsnano.1c11507 .
  * Ono  _et al._ (2013) T. Ono, R. Okamoto, and S. Takeuchi, Nature Communications 4, 2426 (2013).
  * Israel  _et al._ (2014) Y. Israel, S. Rosen, and Y. Silberberg, Phys. Rev. Lett. 112, 103604 (2014).
  * Black  _et al._ (2023) A. N. Black, L. D. Nguyen, B. Braverman, K. T. Crampton, J. E. Evans, and R. W. Boyd, Optica 10, 952 (2023).
  * Defienne  _et al._ (2021b) H. Defienne, B. Ndagano, A. Lyons, and D. Faccio, Nature Physics 17, 591 (2021b).
  * Thekkadath  _et al._ (2023) G. Thekkadath, D. England, F. Bouchard, Y. Zhang, M. Kim, and B. Sussman, Science Advances 9, eadh1439 (2023), https://www.science.org/doi/pdf/10.1126/sciadv.adh1439 .
  * Abouraddy  _et al._ (2004) A. F. Abouraddy, P. R. Stone, A. V. Sergienko, B. E. A. Saleh, and M. C. Teich, Phys. Rev. Lett. 93, 213903 (2004).
  * Lu  _et al._ (2015) C.-H. Lu, M. Reichert, X. Sun, and J. W. Fleischer, “Quantum phase imaging using spatial entanglement,” (2015), arXiv:1509.01227 [physics.optics] .
  * Ortolano  _et al._ (2023) G. Ortolano, A. Paniate, P. Boucher, C. Napoli, S. Soman, S. F. Pereira, I. Ruo-Berchera, and M. Genovese, Light: Science & Applications 12, 171 (2023).
  * Aidukas  _et al._ (2019) T. Aidukas, P. C. Konda, A. R. Harvey, M. J. Padgett, and P.-A. Moreau, Scientific Reports 9, 10445 (2019).
  * Hodgson  _et al._ (2023) H. Hodgson, Y. Zhang, D. England, and B. Sussman, Applied Physics Letters 122, 034001 (2023), https://doi.org/10.1063/5.0133980 .
  * Nomerotski (2019) A. Nomerotski, Nuclear Instruments and Methods in Physics Research Section A: Accelerators, Spectrometers, Detectors and Associated Equipment 937, 26 (2019).
  * (36) “https://kt.cern/technologies/timepix3,” .
  * Frankot and Chellappa (1988) R. Frankot and R. Chellappa, IEEE Transactions on Pattern Analysis and Machine Intelligence 10, 439 (1988).
  * Gong  _et al._ (2017) H. Gong, T. E. Agbana, P. Pozzi, O. Soloviev, M. Verhaegen, and G. Vdovin, Opt. Lett. 42, 2122 (2017).
  * (39) “https://benchmarktech.com/quantitativephasemicroscop/,” .
  * Gul  _et al._ (2021) B. Gul, S. Ashraf, S. Khan, H. Nisar, and I. Ahmad, Photodiagnosis and Photodynamic Therapy 33, 102096 (2021).
  * England  _et al._ (2019) D. G. England, B. Balaji, and B. J. Sussman, Phys. Rev. A 99, 023828 (2019).
  * Shack (1971) R. V. Shack, Spring Meeting of Optical Society of America, 1971 656 (1971).
  * Tyson and Frazier (2022) R. Tyson and B. Frazier,  _Principles of Adaptive Optics_ (CRC Press, 2022).
  * Pfund  _et al._ (1998) J. Pfund, N. Lindlein, and J. Schwider, Appl. Opt. 37, 22 (1998).
  * Chernyshov  _et al._ (2005) A. Chernyshov, U. Sterr, F. Riehle, J. Helmcke, and J. Pfund, Appl. Opt. 44, 6419 (2005).
  * Rodenburg and Maiden (2019) J. Rodenburg and A. Maiden, “Ptychography,” in  _Springer Handbook of Microscopy_, edited by P. W. Hawkes and J. C. H. Spence (Springer International Publishing, Cham, 2019) pp. 819–904.
  * Gerchberg (1972) R. W. Gerchberg, Optik 35, 237 (1972).
  * Vidyapin  _et al._ (2023) V. Vidyapin, Y. Zhang, D. England, and B. Sussman, Scientific Reports 13, 1009 (2023).
  * Zheng  _et al._ (2024) Y. Zheng, Z.-D. Liu, R.-H. Miao, J.-M. Cui, M. Yang, X.-Y. Xu, J.-S. Xu, C.-F. Li, and G.-C. Guo, “Characterizing biphoton spatial wave function dynamics with quantum wavefront sensing,” (2024), arXiv:2406.04973 [quant-ph] .

## The Frankot and Chellappa method

Letting $p(x,y)=\frac{\partial\phi(x,y)}{\partial x}$ and
$q(x,y)=\frac{\partial\phi(x,y)}{\partial y}$ be the measured phase gradients,
the Laplacian for the phase $\phi(x,y)$ can be written as

$\nabla^{2}\phi(x,y)=\frac{\partial^{2}\phi(x,y)}{\partial
x^{2}}+\frac{\partial^{2}\phi(x,y)}{\partial y^{2}}=\frac{\partial
p(x,y)}{\partial x}+\frac{\partial q(x,y)}{\partial y}.$ (5)

Given the Fourier transform and inverse Fourier transform defined as

$\displaystyle\mathscr{F}\Bigl{[}f(x,y)\Bigr{]}=\hat{f}(u,v)=\int\int
f(x,y)e^{-i(ux+vy)}dxdy$
$\displaystyle\mathscr{F}^{-1}\left[\hat{f}(u,v)\right]=f(x,y)=\frac{1}{2\pi}\int\int\hat{f}(u,v)e^{i(ux+vy)}dudv,$
(6)

and using the differentiation property of the Fourier transform

$\mathscr{F}\left[\frac{d^{n}}{dx^{n}}f(x)\right]=(iu)^{n}\hat{f}(u),$ (7)

we can write the Fourier transform of Eq. 5 as

$\displaystyle\mathscr{F}\left[\frac{\partial^{2}\phi(x,y)}{\partial
x^{2}}+\frac{\partial^{2}\phi(x,y)}{\partial y^{2}}\right]$
$\displaystyle=\mathscr{F}\left[\frac{\partial p(x,y)}{\partial
x}+\frac{\partial q(x,y)}{\partial y}\right]$
$\displaystyle-(u^{2}+v^{2})\hat{\phi}(u,v)$
$\displaystyle=iu\hat{p}(u,v)+iv\hat{q}(u,v).$ (8)

Thus, knowing the phase gradients $p(x,y)$ and $q(x,y)$ and computing their
Fourier transforms $\hat{p}(u,v)$ and $\hat{q}(u,v)$, the phase $\phi(x,y)$
can be recovered through the inverse Fourier transform of Eq. 8

$\phi(x,y)=\mathscr{F}^{-1}\left[\frac{u\hat{p}(u,v)+v\hat{q}(u,v)}{i(u^{2}+v^{2})}\right].$
(9)

## Background generation, detection and subtraction

Background photon events are numerically generated and inserted into the raw
camera data. A random number generator is used to generate the detected
position and time for each photon from a background light with Gaussian beam
profile exhibiting Poissonian photon number statistics. This background is
applied to both the NF and FF. Parameters for the intensity, width, and
location of the Gaussian shaped background is randomized every 25 s to
simulate a dynamic background. The background is chosen to be randomized every
25 s and not at a much faster rate so as not to create an overall background
that is uniform in intensity after the 500 s data acquisition time. For the
data in Fig. 4(b) of the main text, the background intensity in each image
plane is on average $\sim 0.5\times 10^{6}$ photons per second, and for Fig.
4(c) of the main text this is $\sim 1\times 10^{6}$ photons per second. In
comparison, the number of detected SPDC photons in each image plane is $\sim
1.1\times 10^{6}$ photons per second. For better comparison, the same seed is
used in the random number generation of the width and location for the
background light at the two different intensity levels. An illustration on how
the background is added to the NF and FF with time is shown in Fig. 6(a).

Figure 6: Background generation and detection (a) Shows the numerically added
background light to the NF and FF whose parameters are randomized every 25 s.
(b) A typical coincidence histogram taken showing the number of events
detected as a function of the difference in arrival time between the photons
detected on the two regions of the camera. The location and width of the
coincidence window for identifying all photons detected in coincidence and
only that of background coincidences are highlighted in orange. (c) Verifying
the validity of the background identification approach illustrated in (b)
through subtracting the obtained background image from the image containing
all coincidences.

Figure 6(b) is a typical histogram showing the difference in arrival time
between two photons detected in the two regions of the camera. The central
peak is the result of time-correlated SPDC photon pairs being detected at the
same time. On the other hand a constant background is also visible in the
histogram, this is from the detection of coincidence between uncorrelated
photons. It is not possible to determine which of the photon pairs detected
are from background light, however, one can determine the resultant
contribution of the background. To obtain the background contribution, the
coincidence window is shifted away from the central peak. All photon pair
events detected within this window will be from only uncorrelated photons.
Since the background coincidence rate is uniform in time on the nanosecond
timescale, this measurement is representative of the accidental coincidence
rate in the central window. It can be verified that the resultant image formed
by the uncorrelated photon pairs is indeed the background by subtracting it
directly from the coincidence image to obtain a background free image, as
shown in Fig. 6(c).

Due to the timing resolution of the camera, a 50 ns shift in the coincidence
window is used in this experiment. For a detector with better timing
resolution, which will result in a narrower central peak for SPDC, a smaller
shift can be used. Note that this method of background identification is only
valid when the background fluctuation is slower than the applied shift to the
coincidence window.

Now with the position information on each detected photon pair from the
background correlation measurement, the background contribution is subtracted
from the centroid shift by modifying eq. 1 as follows:

$\displaystyle\mathscr{U}(x,y)$
$\displaystyle=\frac{1}{N(x,y)-N_{b}(x,y)}\left(\sum_{n=1}^{N(x,y)}u_{n}(x,y)-\sum_{m=1}^{N_{b}(x,y)}u^{b}_{m}(x,y)\right)$
$\displaystyle\mathscr{V}(x,y)$
$\displaystyle=\frac{1}{N(x,y)-N_{b}(x,y)}\left(\sum_{n=1}^{N(x,y)}v_{n}(x,y)-\sum_{m=1}^{N_{b}(x,y)}v^{b}_{m}(x,y)\right),$
(10)

where $N_{b}(x,y)$ is the number of background coincidences detected at
position $(x,y)$ in the NF and $u^{b}(x,y)$ and $v^{b}(x,y)$ are the positions
of the background photons detected in the FF, in coincidence with those
detected at position $(x,y)$ in the NF.

## Images of full data set

Figure 7 shows the recovered phase images and cross-sections for all Star
resolution phase targets with full far-field (FF) resolution and 2$\times$2
pixels FF resolution. Figure 8 shows the recovered phase and NRMSE as a
function of the target thickness for the Star target as determined from Fig.
7. Figure 9 shows the recovered phase images and cross-sections for all 1951
USAF resolution phase targets with full FF resolution and 2$\times$2 pixels FF
resolution. Figure 10 shows the recovered phase as a function of the target
thickness for the 1951 USAF target as determined from Fig. 9. Figure 11 shows
the recovered phase images and cross-sections of the Star resolution phase
targets used to illustrate background subtraction.

Figure 7: Recovered phase image and cross-section of all Star resolution phase
targets. Figure 8: Recovered phase and NRMSE as a function of the target
thickness for the Star target. Red are the results for after a 30$\times$30
binning is applied to the idler photons’ position, whereas blue are when no
binning is applied. Figure 9: Recovered phase image and cross-section of the
highlighted region for all 1951 USAF resolution phase targets. Figure 10:
Recovered phase as a function of the target thickness for the 1951 USAF
target. Red triangles are the results for after a 30$\times$30 binning is
applied to the idler photons’ position, whereas blue circles are when no
binning is applied. Figure 11: Recovered phase image and cross-section of Star
resolution phase targets to illustrate the background subtraction.