#  On black hole supertranslations and hydrodynamic enstrophy

Raja Marjieh<EMAIL_ADDRESS>Department of Psychology, Princeton
University, Princeton, NJ 08544, USA  Natalia Pinzani-Fokeeva<EMAIL_ADDRESS>Center for Theoretical Physics, Massachusetts Institute of Technology,
Cambridge, MA 02139, USA, and
Department of Physics, University of Florence, Via G. Sansone 1, I-50019,
Sesto Fiorentino, Firenze, Italy  Bar Tavor<EMAIL_ADDRESS>Amos
Yarom<EMAIL_ADDRESS>Department of Physics, Technion, Haifa
32000, Israel

###### Abstract

We study the relation between approximate horizon symmetries of AdS black
branes and approximately conserved currents in their dual hydrodynamic
description. We argue that the existence of an approximately conserved
enstrophy current unique to $2+1$ dimensional fluid flow implies that AdS4
black branes possess a special class of approximate supertranslations (which
we identify).

††preprint: MIT-CTP/5340

##  I Introduction

Enstrophy is a scalar quantity associated with non relativistic,
incompressible, fluid flow. In two spatial dimensions it can not increase in
time, and in the absence of dissipation it is conserved. Its properties are
key ingredients in generating the unique features of turbulent flows in two
spatial dimensions.

The study of enstrophy in relativistic fluids is lagging behind that of its
Galilean cousin. It is possible to identify a relativistic enstrophy current
which is conserved for an ideal fluid in $2+1$ dimensions [1, 2, 3]. Since
dissipative effects spoil this property, we will refer to such a current as
being approximately conserved.

The existence of a relativistic enstrophy current suggests, via the gauge-
gravity duality [4], that AdS4 black branes possess an approximate symmetry
associated with approximate enstrophy conservation. Since the enstrophy
current exists only in the hydrodynamic limit, one might expect that an
associated approximate black hole symmetry will exist on the event horizon.

Indeed, it has recently been established that stationary black hole geometries
are endowed with horizon symmetries, classified as supertranslations and
superrotations [5, 6] (see [7, 8, 9, 10] for older work on this topic).
Generic fluid flows which possess enstrophy are not stationary and imply non
stationary dual black hole configurations. While the definition of
supertranslations and superrotations may be extended to non stationary black
holes, they are generally not associated with conserved currents [11].

In this work we will relate a subset of supertranslation transformations of
AdS4 black branes to approximate enstrophy current conservation in the dual
hydrodynamic description of the field theory. Further, we clarify the role of
the remaining generators of supertranslations and identify them with
symmetries leading to non local approximately conserved currents.
Superrotations do not lead to approximately conserved currents in a dual
hydrodynamic setting.

Relations between hydrodynamics and horizon symmetries have been considered in
the past. In [12], the authors analysed asymptotically AdS black brane
solutions dual to a superfluid flow and identified the action of
supertranslations on horizon data with the superfluid Goldstone mode. In [13],
horizon symmetries in $3+1$ dimensions were shown to be in one to one
correspondence with symmetries of compressible non relativistic fluids in
$2+1$ dimensions (see also [14] for a similar relation in a different
context).

Our exposition starts with a review of the relativistic, conformal, enstrophy
current, as first discussed in [1], and its extensions [2, 3]. Using the
construction of [11], we then discuss the general structure of horizon
preserving diffeomorphisms. Finally, we use our knowledge of enstrophy
conservation in the boundary theory to show that AdS4 black brane geometries
possess special supertranslation symmetries. We end with a discussion and
outlook.

##  II The enstrophy current

The equations of motion of an uncharged, conformal, relativistic fluid are
given by

$\nabla_{\mu}T^{\mu\nu}=0\,,$ (1)

where $T^{\mu\nu}$ is the energy momentum tensor of the fluid and is a local
function of the the fluid velocity $u^{\mu}$ (satisfying $u^{\mu}u_{\mu}=-1$)
and fluid temperature $T$. Working in a derivative expansion we have

$T^{\mu\nu}=P(T)\left((d+1)\,u^{\mu}u^{\nu}+g^{\mu\nu}\right)+\mathcal{O}(\nabla)$
(2)

where $d>1$ is the number of spatial dimensions, $P(T)=p_{0}T^{d+1}$ is the
thermodynamic pressure with $p_{0}$ a positive real number, and
$\mathcal{O}(\nabla)$ denotes expressions which contain one or more
derivatives of the hydrodynamic variables $u^{\mu}$ and $T$.

For any function $g$ which satisfies

$u^{\mu}\nabla_{\mu}g={\cal O}(\nabla^{[g]+2})\,,$ (3)

we may construct the current

$J_{g}^{\mu}=g\,p_{0}(d+1)\,T^{d}u^{\mu}$ (4)

which satisfies

$\nabla_{\mu}J_{g}^{\mu}=\mathcal{O}(\nabla^{[g]+2})\,.$ (5)

In obtaining (5) we have used that
$\nabla_{\mu}(T^{d}u^{\mu})=\mathcal{O}(\nabla^{2})$ as a result of the
equations of motion (1) expanded in derivatives. The particular choice of the
overall constant $p_{0}(d+1)$ will become clear shortly.

A naive power counting argument would suggest that $\nabla_{\mu}J_{g}^{\mu}$
is of the same order as $g$ plus one in a derivative expansion. Instead, (5)
implies that it is order $g$ plus two. In other words, it is conserved at
least to leading order in a derivative expansion. In what follows we will
refer to $J_{g}^{\mu}$ as an approximately conserved current.

We often require conserved currents to be local in the hydrodynamic variables,
in this case $u^{\mu}$ and $T$. While there are many non local solutions to
(3), local solutions are more difficult to come by. Clearly, $g=1$, or any
constant for that matter, is a solution to (3). For such solutions we obtain

$J_{1}^{\mu}=su^{\mu}$ (6)

with $s=\frac{\partial P}{\partial T}$ the entropy density. Approximate
conservation of $J_{1}^{\mu}$ coincides with the leading order equation of
motion and implies conservation of entropy in the absence of dissipation.

Another solution to (3) which is local in the hydrodynamic variables is given
by

$g=\frac{\Omega_{\alpha\beta}\Omega^{\alpha\beta}}{s^{2}}\,,$ (7)

with

$\Omega_{\mu\nu}=\partial_{\mu}\left(Tu_{\nu}\right)-\partial_{\nu}\left(Tu_{\mu}\right)\,,$
(8)

and is valid only in $2+1$ spacetime dimensions. The associated current

$J_{\frac{\Omega^{2}}{s^{2}}}^{\mu}=\frac{\Omega_{\alpha\beta}\Omega^{\alpha\beta}}{s}u^{\mu}$
(9)

is the relativistic enstrophy current [1, 2, 3], and its associated charge is
referred to as enstrophy. Of course, if $g$ solves (3) so do powers of $g$,
and we find a set of conserved currents,

$J_{\left(\frac{\Omega^{2}}{s^{2}}\right)^{n}}^{\mu}=\left(\frac{\Omega_{\alpha\beta}\Omega^{\alpha\beta}}{s^{2}}\right)^{n}su^{\mu}\,.$
(10)

When $n=0$, the above expression reduces to the entropy current (6). The
currents (6) and (10) comprise the only known local solutions to (3).

We note in passing that in a non relativistic, incompressible fluid the
charges $\int\left(\omega_{ij}\omega^{ij}\right)^{n}d^{2}x$, with
$\omega_{ij}=\partial_{i}v_{j}-\partial_{j}v_{i}$ and $v_{i}$ the velocity
field, are conserved in the inviscid limit. The former integral with $n=1$ is
referred to as the total enstrophy. Once dissipative effects are included, the
total enstrophy decreases in time. This property, together with energy
conservation, leads to an inverse energy cascade in 2+1 dimensional
incompressible non relativistic turbulent flows whereby energy is transferred
from small to large scales [15]. Whether similar statements can be made for
relativistic fluids is yet an open problem.

##  III Horizon symmetries and charges

An extensive analysis of horizon symmetries and charges was carried out in
[11]. In what follows we summarize the essential ingredients of [11] required
for this work. Consider a spacetime $\mathcal{M}$ with metric $g_{ab}$ and
event horizon $\mathcal{N}$ whose topology is $\mathcal{Z}\times\mathbb{R}$
with $\mathbb{R}$ a null direction. We refer to $\mathcal{Z}$ as the base
space of $\mathcal{N}$. In the case of an asymptotically AdSd+2 black brane,
$\mathcal{Z}$ has topology $\mathbb{R}^{d}$. Let us denote the pullback to the
horizon by $\Pi_{i}{}^{a}$ so that $g_{ij}=\Pi_{j}{}^{b}\Pi_{j}{}^{b}g_{ab}$
is the induced metric on the event horizon. Since $\mathcal{N}$ is null,
$g_{ij}$ is not invertible. We denote the pullback from $\mathcal{N}$ to the
base space $\mathcal{Z}$ by $\Pi_{A}{}^{i}$ so that the induced metric on
$\mathcal{Z}$ is $g_{AB}=\Pi_{A}{}^{a}\Pi_{B}{}^{b}g_{ab}$ where
$\Pi_{A}{}^{a}=\Pi_{A}{}^{i}\Pi_{i}{}^{a}$. Since $\mathcal{Z}$ is spacelike,
$g_{AB}$ is invertible. In what follows we will consistently use
$a,\,b,\,\ldots$ for indices on $\mathcal{M}$, $i,\,j,\,\ldots$ for indices on
$\mathcal{N}$ and $A,\,B,\,\ldots$ for indices on $\mathcal{Z}$. Later, when
we will focus on asymptotically AdS spaces, we will introduce indices
$\mu,\,\nu,\ldots$ on the asymptotic boundary of the spacetime.

We denote by $\ell^{i}$ a representative vector field generating null
geodesics along the null direction $\mathbb{R}$ of $\mathcal{N}$, and by
$\ell^{a}$ an extension of it to all of $\mathcal{M}$. We define the non
affinity parameter $\kappa$ via

$\ell^{a}\nabla_{a}\ell^{b}\Big{|}_{\mathcal{N}}=\kappa\ell^{b}\Big{|}_{\mathcal{N}}\,,$
(11)

where, as usual, $\nabla_{a}$ is the covariant derivative on ${\mathcal{M}}$.
We also denote a null cotangent vector on $\mathcal{N}$ by $n_{i}$ and
normalize it and its extension to $\mathcal{M}$ such that $n_{a}\ell^{a}=-1$.

We will often need to go back and forth between tangent vectors on
$\mathcal{M}$ (or $\mathcal{N}$) and tangent vectors on $\mathcal{N}$ (or
$\mathcal{Z}$). For instance, suppose that $v^{a}\in T(\mathcal{M})$ satisfies
$v^{a}\ell_{a}\Big{|}_{\mathcal{N}}=0$ (recall that $\ell_{a}$ is the normal
to $\mathcal{N}$). Then, we may always define a unique $v^{i}\in
T(\mathcal{N})$ such that
$v^{a}w_{a}\Big{|}_{\mathcal{N}}=v^{i}\Pi_{i}{}^{a}w_{a}$ for any $w_{a}\in
T^{*}(\mathcal{M})$. To simplify our notation we will write

$v^{a}\partial_{a}\cong v^{i}\partial_{i}\,.$ (12)

An infinitesimal coordinate transformation $\chi=\chi^{i}\partial_{i}$ is
referred to as a generator of a horizon preserving diffeomorphism if

$\pounds_{\chi}\ell^{i}={\beta}\ell^{i}\,,\qquad\pounds_{\chi}\kappa=(\beta\kappa+\pounds_{\ell}\beta),$
(13)

with $\beta$ a function on $\mathcal{N}$. The first equation in (13) is an
infinitesimal version of a rescaling of the null vector $\ell^{i}\partial_{i}$
(which does not have a well defined length due to the fact that it’s null).
The second equation in (13) corresponds to a shift in the non affinity
parameter resulting from a rescaling of $\ell^{a}\partial_{a}$, c.f., (11).

The generator $\chi^{i}$ can be naturally decomposed into a component parallel
to $\ell^{i}$ and a component orthogonal to it,

$\chi^{i}\partial_{i}=X^{i}\partial_{i}+f\ell^{i}\partial_{i}\,,$ (14)

with $X^{i}n_{i}=0$. With this decomposition equation (13) reads

$\displaystyle\begin{split}\pounds_{\ell}X^{i}\propto\,&\ell^{i}\,,\\\
\qquad\pounds_{\ell}\left(\pounds_{\ell}+\kappa\right)f+X^{i}\pounds_{\ell}\left(\pounds_{\ell}+\kappa\right)n_{i}+\pounds_{X}\kappa=\,&0\,.\end{split}$
(15)

It is tempting to refer to a horizon symmetry associated with $X^{i}$ as a
superrotation and to a horizon symmetry associated with $f\ell^{i}$ as a
supertranslation. Note, however, that the distinction between the two is
dependent on the choice of $n_{i}$. In [11] it was shown, using an explicit
construction, that there exists an $n_{i}$ for which

$\pounds_{\ell}\left(\pounds_{\ell}+\kappa\right)n_{i}+\partial_{i}\kappa=0\,.$
(16)

With this choice of $n_{i}$, equations (15) can be shown to reduce to

$\pounds_{\ell}\left(\pounds_{\ell}+\kappa\right)f=0\,.$ (17)

One may refer to the supertranslations and superrotations obtained using the
$n_{i}$ which leads to (17) as canonical supertranslations and superrotations.

One of the results of [11] is that, in the absence of matter, we can associate
to each such $\chi$ a Wald-Zoupas charge, $Q_{\chi}$, which is conserved
whenever the horizon is stationary. Operatively, for each generator $\chi$ we
define a current $q_{\chi}^{i}$ satisfying

$q_{\chi}^{j}=\left(\chi^{i}\mathcal{K}_{i}{}^{j}-\theta\chi^{j}-\beta\ell^{j}\right)\,.$
(18)

Here $\beta$ is associated with the scaling of $\ell^{i}$ under $\chi^{j}$ as
in (13), $\mathcal{K}_{i}{}^{j}$ denotes the Weingarten map

$\mathcal{K}_{i}{}^{j}\partial_{j}\cong\Pi_{i}{}^{a}\nabla_{a}\ell^{b}\partial_{b}\,,$
(19)

and $\theta$ is the expansion associated with $\ell^{i}$,

$\theta=\nabla_{i}\ell^{i}=\frac{1}{\sqrt{|g_{AB}|}}\partial_{i}\left(\sqrt{|g_{AB}|}\ell^{i}\right)\,.$
(20)

It is straightforward though somewhat tedious to compute the divergence of
$q_{\chi}^{i}$. Recall that the Weingarten map satisfies

$\ell^{i}\mathcal{K}_{i}{}^{j}=\kappa\ell^{j}\,,\qquad\mathcal{K}_{i}{}^{j}g_{jk}=\frac{1}{2}\pounds_{\ell}g_{ik}\,.$
(21)

The expression on the right hand-side of the second equality is the second
fundamental form on $\mathcal{N}$, $K_{ij}=\frac{1}{2}\pounds_{\ell}g_{ij}$.
It is orthogonal to $\ell^{i}$ allowing us to write

$K_{ij}=\frac{\theta}{d}g_{ij}+\Sigma_{ij}$ (22)

where $\Sigma_{ij}dx^{i}dx^{j}\cong\Sigma_{AB}dx^{A}dx^{B}$ is symmetric and
traceless, $\Sigma_{AB}g^{AB}=0$. Thus, the most general expression for
$\mathcal{K}_{i}{}^{j}$ satisfying (21) is

$\mathcal{K}_{i}{}^{j}=\omega_{i}\ell^{j}+S_{i}{}^{j}\ \,,$ (23)

where

$S_{i}{}^{j}dx^{i}\partial_{j}\cong\left(\frac{\theta}{d}\delta_{A}{}^{B}+\Sigma_{A}{}^{B}\right)dx^{A}\partial_{B}\,,$
(24)

and

$\omega_{i}=-\kappa n_{i}dx^{i}+\Omega_{i}dx^{i}$ (25)

is the rotation one form (sometimes also referred to as the extrinsic
curvature one form) with $\Omega_{i}dx^{i}\cong\Omega_{A}dx^{A}$ the normal
fundamental form on $\mathcal{Z}$.

Inserting (14) into (18), using (13) to evaluate $\beta$ in (18), and also
inserting the decomposition (23) into (18), one finds

$q^{i}_{\chi}=q_{\chi}\ell^{i}+X^{j}S_{j}{}^{i}-\theta X^{i}\,,$ (26)

where

$q_{\chi}=\left(\pounds_{l}f+kf-\theta
f)+X^{i}(\omega_{i}+\pounds_{l}n_{i}\right)\,.$ (27)

Taking the divergence of (26) we find

$\displaystyle\begin{split}\nabla_{i}q_{\chi}^{i}=&\pounds_{\ell}\left(\pounds_{\ell}+\kappa\right)f+X^{i}\pounds_{\ell}\left(\pounds_{\ell}+\kappa\right)n_{i}+\pounds_{X}\kappa\\\
&+X^{i}\left(\pounds_{\ell}\omega_{i}-\partial_{i}\kappa\right)+\nabla_{j}\left(X^{i}\Sigma_{i}{}^{j}\right)\\\
&-\theta\left(f(\theta-\kappa)-X^{i}(\omega_{i}+\pounds_{\ell}n_{i})\right)-f\pounds_{\ell}\theta\\\
&-\nabla_{i}\left(\theta X^{i}\right)\left(1-\frac{1}{d}\right)\,.\end{split}$
(28)

Note that the first line on the right hand-side of (28) vanishes if $\chi^{i}$
is a generator of a horizon preserving diffeomoprhism, cf. (15).

If the event horizon is stationary, that is, there exists an $\alpha$ such
that $\tau^{a}=e^{\alpha}\ell^{a}$ is a Killing vector near the horizon

$\pounds_{\tau}g_{ab}\Big{|}_{\mathcal{N}}=0\,,\qquad\nabla_{c}\pounds_{\tau}g_{ab}\Big{|}_{\mathcal{N}}=0\,,$
(29)

then

$K_{ij}=\pounds_{\ell}g_{ij}=e^{-\alpha}\pounds_{\tau}g_{ij}=0\,,$ (30)

so that $\Sigma_{ij}=0$ and $\theta=0$. In addition, using

$\nabla_{a}\nabla_{b}\tau_{c}\Big{|}_{\mathcal{N}}=-R_{bca}{}^{d}\tau_{d}\Big{|}_{\mathcal{N}}$
(31)

(which results from (29)), we find that
$\pounds_{\tau}\nabla_{a}\tau^{b}\Big{|}_{\mathcal{N}}=0$ implying

$\pounds_{e^{\alpha}\ell}\left(\omega_{i}+\nabla_{i}\alpha\right)=0\,.$ (32)

Further, using the zeroth law of black holes (for stationary horizons) [16],
we have

$\partial_{i}\left(e^{\alpha}\left(\kappa+\pounds_{\ell}\alpha\right)\right)=0\,.$
(33)

Putting together (32) and (33) we find

$\pounds_{\ell}\omega_{i}-\partial_{i}\kappa=0\,,$ (34)

independent on $\alpha$. Thus, $\nabla_{i}q_{\chi}^{i}=0$ for stationary
horizons as long as $\xi$ is a supertranslation or superrotation (or a
combination thereof).

##  IV Enstrophy and supertranslations

In an asymptotically AdS geometry, there exist stationary black brane
solutions characterized by a uniform Hawking temperature, $T$, and a constant
center of mass velocity $u^{\mu}$ relative to an observer at infinity. Here
greek indices $\mu,\,\nu,$ denote coordinates on the boundary of AdS space. As
discussed in detail in [4], it is possible to perturb these black brane
solutions in a derivative expansion where one assumes that derivatives of $T$
and $u^{\mu}$ are small relative to $T$. The perturbative solution to the
Einstein equations takes the form

$\displaystyle\begin{split}g_{ab}dx^{a}dx^{b}=&-r^{2}h(r)u_{\mu}u_{\nu}dx^{\mu}dx^{\nu}+r^{2}P_{\mu\nu}dx^{\mu}dx^{\nu}\\\
&-2u_{\mu}dx^{\mu}dr+\mathcal{O}(\nabla)\,,\end{split}$ (35)

where $T$ and $u^{\mu}$ are constrained to satisfy

$\nabla_{\mu}\left(T^{d}u^{\mu}\right)=\mathcal{O}(\nabla^{2})\,,\qquad
Tu^{\nu}\nabla_{\nu}u_{\mu}-P^{\nu}_{\mu}\nabla_{\nu}T={\cal O}(\nabla^{2})$
(36)

with $\nabla_{\mu}$ a covariant derivative in Minkowski space,
$P_{\mu\nu}=\eta_{\mu\nu}+u_{\mu}u_{\nu}$, and

$h=1-\left(\frac{4\pi T}{(d+1)r}\right)^{d+1}\,.$ (37)

Incidentally, (36) correspond to the hydrodynamic equations (1) (see [4]).

The location of the event horizon for the geometry (35) is given by

$r=\frac{4\pi T}{d+1}+\mathcal{O}(\nabla)\,.$ (38)

Here and in the remainder of this section we will use the coordinates
$x^{\mu}$ to parameterize the horizon. It now follows that

$\ell^{i}\partial_{i}=u^{\mu}\partial_{\mu}+\mathcal{O}(\nabla)$ (39)

and also

$\kappa=2\pi T+\mathcal{O}(\nabla)\,.$ (40)

We will also choose,

$n_{i}dx^{i}=u_{\mu}dx^{\mu}+\mathcal{O}(\nabla)\,.$ (41)

(Note that this choice of $n_{i}$ satisfies (16) to leading order in a
derivative expansion.) With this parameterization we find that
$\Omega_{A}=\mathcal{O}(\nabla)$ and that

$\Sigma_{i}{}^{j}dx^{i}\partial_{j}={\frac{1}{2}}\sigma_{\mu}{}^{\nu}dx^{\mu}\partial_{\nu}+{\cal
O}(\nabla^{2})\,,$ (42)

where $\sigma_{\mu\nu}$ is the shear tensor for a fluid with velocity
$u^{\mu}$,

$\sigma^{\mu\nu}=P^{\mu\alpha}P^{\nu\beta}\left(\nabla_{\alpha}u_{\beta}+\nabla_{\beta}u_{\alpha}\right)-\frac{2}{d}P^{\mu\nu}\nabla_{\alpha}u^{\alpha}\,.$
(43)

With our choice of parameterization we find that the Einstein equations take
the form

$\theta=\mathcal{O}(\nabla^{2})\,,\qquad\left(\pounds_{\ell}\omega_{i}-\partial_{i}\kappa\right)\Pi^{i}_{A}=\mathcal{O}(\nabla^{2})\,.$
(44)

Suppose that $\chi^{i}$ is a supertranslation ($X^{i}=0$) and that $f$ is
order $\mathcal{O}(\nabla^{[f]})$ in a derivative expansion. In this case
$q_{\chi}^{i}$ is also $\mathcal{O}(\nabla^{[f]})$ but

$\nabla_{i}q_{fu}^{i}=\mathcal{O}\left(\nabla^{[f]+2}\right)$ (45)

on account of the equation of motion (44). Thus, supertranslations lead to an
approximately conserved current in the derivative expansion. Superrotations
will not lead to approximately conserved currents owing to the fact that
$\nabla_{i}q_{X}^{i}=\mathcal{O}(\nabla^{[X]+2})$ but
$q_{X}^{i}=\mathcal{O}(\nabla^{[X]+1})$.

In a derivative expansion the supertranslation constraint, (15), reads

$\pounds_{u}(\kappa f)=\mathcal{O}(\nabla^{[f]+2})$ (46)

and the resulting current is

$q_{fu}^{i}\partial_{i}=\kappa fu^{\mu}\partial_{\mu}\,.$ (47)

The divergence of $q_{fu}^{i}$ is given, in our current coordinate system, by

$\nabla_{i}q^{i}_{fu}=\frac{1}{T^{d}}\partial_{i}\left(T^{d}q^{i}_{fu}\right)\,,$
(48)

where the factors of $T^{d}$ come from the measure on the spatial section of
the horizon. We are guaranteed that $q^{i}_{fu}$ is approximately conserved
provided that (46) is satisfied which implies that the divergence of

$J_{f}^{\mu}=T^{d}\kappa fu^{\mu}$ (49)

in Minkowski space will approximately vanish.

Equation (49) and its approximate conservation reproduces (5) once we identify
$J^{\mu}_{f}$ in (49) with $J_{g}^{\mu}$ in (4). Thus, approximate enstrophy
conservation is a result of a particular set of supertranslations on the
horizon of AdS4 black branes which are local in the black hole temperature and
center of mass velocity, $T$ and $u^{\mu}$. Likewise, approximate entropy
conservation is a result of horizon supertranslations of AdSd+2 black branes
with $f=c/\kappa$, (with $c$ a constant).

##  V Discussion and outlook

In this work we have shown that horizon supertranslation generators of AdS
black brane geometries, which are conserved in the stationary limit, are
associated with approximately conserved currents in a dual fluid description
of the geometry.

In asymptotically AdS4 geometries there exist a small subset of
supertranslation generators which are local functions of the Hawking
temperature and black brane null generators which are dual to the
approximately conserved enstrophy and its various moments. Horizon
superrotations are not associated with conserved charges of the dual fluid
since conservation of superrotations in the stationary limit is not enhanced
to an approximate symmetry once stationarity is only approximate.

The analysis carried out in this work pertains to asymptotically AdS black
branes in the absence of matter, dual to uncharged conformal fluids. We expect
our main result to be applicable more broadly to charged non conformal fluids.
More generally, relying on the membrane paradigm [17], one might expect a
similar construction for black holes in asymptotically flat space, or even
black holes in general.

Non relativistic enstrophy is not only conserved in the absence of
dissipation, it can not increase in time. Whether the same can be said
regarding the relativistic enstrophy current is yet an open problem. Another
hydrodynamic quantity which we know must not decrease in time (in a
relativistic setting or not) is the entropy. That entropy can not decrease
translates into the well known area increase theorem of black holes [18].
Thus, one can not help but wonder whether there is an enstrophy decrease
theorem for black holes valid, at the very least, at low velocities. While the
present work has not dealt with a full description of black hole enstrophy and
its dynamics, we hope it will provide a stepping stone towards it.

## Acknowledgments

We would like to thank A. Frishman for useful discussions. NPF is supported by
the European Commission through the Marie Sklodowska-Curie Action UniCHydro
(grant agreement ID: 886540). NPF would also like to acknowledge support from
the Center for Theoretical Physics and the Department of Physics at the
Massachusetts Institute of Technology. AY and BT are supported in part by an
Israeli Science Foundation excellence center grant 2289/18 and a Binational
Science Foundation grant 2016324.

## References

  * Carrasco  _et al._ [2012] F. Carrasco, L. Lehner, R. C. Myers, O. Reula, and A. Singh, Turbulent flows for relativistic conformal fluids in 2+1 dimensions, Phys. Rev. D86, 126006 (2012), arXiv:1210.6702 [hep-th] .
  * Marjieh  _et al._ [2020] R. Marjieh, N. Pinzani-Fokeeva, and A. Yarom, Enstrophy from symmetry, (2020), arXiv:2009.03980 [hep-th] .
  * Pinzani-Fokeeva and Yarom [2021] N. Pinzani-Fokeeva and A. Yarom, Enstrophy without boost symmetry, (2021), arXiv:2103.06840 [hep-th] .
  * Bhattacharyya  _et al._ [2008] S. Bhattacharyya, V. E. Hubeny, S. Minwalla, and M. Rangamani, Nonlinear Fluid Dynamics from Gravity, JHEP 02, 045, arXiv:0712.2456 [hep-th] .
  * Donnay  _et al._ [2016a] L. Donnay, G. Giribet, H. A. Gonzalez, and M. Pino, Supertranslations and Superrotations at the Black Hole Horizon, Phys. Rev. Lett. 116, 091101 (2016a), arXiv:1511.08687 [hep-th] .
  * Donnay  _et al._ [2016b] L. Donnay, G. Giribet, H. A. González, and M. Pino, Extended Symmetries at the Black Hole Horizon, JHEP 09, 100, arXiv:1607.05703 [hep-th] .
  * Carlip [1999] S. Carlip, Entropy from conformal field theory at Killing horizons, Class. Quant. Grav. 16, 3327 (1999), arXiv:gr-qc/9906126 .
  * Hotta  _et al._ [2001] M. Hotta, K. Sasaki, and T. Sasaki, Diffeomorphism on horizon as an asymptotic isometry of Schwarzschild black hole, Class. Quant. Grav. 18, 1823 (2001), arXiv:gr-qc/0011043 .
  * Koga [2001] J.-i. Koga, Asymptotic symmetries on Killing horizons, Phys. Rev. D 64, 124012 (2001), arXiv:0107096 [gr-qc] .
  * Hotta [2002] M. Hotta, Holographic charge excitations on horizontal boundary, Phys. Rev. D 66, 124021 (2002), arXiv:hep-th/0206222 .
  * Chandrasekaran  _et al._ [2018] V. Chandrasekaran, E. E. Flanagan, and K. Prabhu, Symmetries and charges of general relativity at null boundaries, JHEP 11, 125, arXiv:1807.11499 [hep-th] .
  * Eling and Oz [2016] C. Eling and Y. Oz, On the Membrane Paradigm and Spontaneous Breaking of Horizon BMS Symmetries, JHEP 07, 065, arXiv:1605.00183 [hep-th] .
  * Penna [2017] R. F. Penna, Near-horizon BMS symmetries as fluid symmetries, JHEP 10, 049, arXiv:1703.07382 [hep-th] .
  * Donnelly  _et al._ [2021] W. Donnelly, L. Freidel, S. F. Moosavian, and A. J. Speranza, Gravitational edge modes, coadjoint orbits, and hydrodynamics, JHEP 09, 008, arXiv:2012.10367 [hep-th] .
  * Kraichnan [1967] R. H. Kraichnan, Inertial Ranges in Two-Dimensional Turbulence, Physics of Fluids 10, 1417 (1967).
  * Bardeen  _et al._ [1973] J. M. Bardeen, B. Carter, and S. W. Hawking, The Four laws of black hole mechanics, Commun. Math. Phys. 31, 161 (1973).
  * Damour [1979] T. Damour, Quelques propriétés mécaniques, électromagnétiques, thermodynamiques et quantiques des trous noirs, (1979).
  * Bekenstein [1972] J. D. Bekenstein, Black holes and the second law, Lett. Nuovo Cim. 4, 737 (1972).


What is the meaning of proofs?
A Fregean distinction in proof-theoretic semantics

Sara AyhanI would like to thank several people for supporting me in improving this paper essentially, among them Luca Tranchini for his thorough feedback and vital input on an earlier version of this paper and also two anonymous referees for their very constructive and helpful reports. I am especially grateful to Heinrich Wansing for the numerous and encouraging occasions to discuss this paper extensively and for his valuable comments.

Sara Ayhan Institute of Philosophy I, Ruhr University Bochum, Bochum, Germany

This is a post-peer-review, pre-copyedit version of an article published in the Journal of Philosophical Logic.
The final authenticated version will be available online at: DOI: 10.1007/s10992-020-09577-2

The origins of proof-theoretic semantics lie in the question of what constitutes the meaning of the logical connectives and its response: the rules of inference that govern the use of the connective.
However, what if we go a step further and ask about the meaning of a proof as a whole?
In this paper we address this question and lay out a framework to distinguish sense and denotation of proofs.
Two questions are central here.
First of all, if we have two (syntactically) different derivations, does this always lead to a difference, firstly, in sense, and secondly, in denotation?
The other question is about the relation between different kinds of proof systems (here: natural deduction vs. sequent calculi) with respect to this distinction.
Do the different forms of representing a proof necessarily correspond to a difference in how the inferential steps are given?
In our framework it will be possible to identify denotation as well as sense of proofs not only within one proof system but also between different kinds of proof systems.
Thus, we give an account to distinguish a mere syntactic divergence from a divergence in meaning and a divergence in meaning from a divergence of proof objects analogous to Frege's distinction for singular terms and sentences.

§ INTRODUCTION

In proof-theoretic semantics (PTS) the meaning of the logical constants is taken to be given by the rules of inference that govern their use.
As a proof is constituted by applications of rules of inference, it seems reasonable to ask what the meaning of proofs as a whole would consist of on this account.
What we are particularly interested in is a Fregean distinction between sense and denotation in the context of proofs.[We assume at least a basic familiarity with this idea, laid out in Frege's famous paper “Über Sinn und Bedeutung”, cf. [8] for an English translation.]
This account builds up on [26], where such a distinction is proposed and used in a proof-theoretic explanation of paradoxes.

The notion of denotation is nothing new in the context of proofs.
It is common in the literature on proof theory and PTS (e.g. <cit.>, [22], [16]) to distinguish between derivations, as linguistic objects, and proofs, as abstract (in the intuitionistic tradition: mental) entities.
Proofs are then said to be represented or denoted by derivations, i.e. the abstract proof object is the denotation of a derivation.
The notion of sense, on the other hand, has been more or less neglected.
Tranchini [26], therefore, made a proposal that for a derivation to have sense means to be made up of applications of correct inference rules.
While this is an interesting approach to consider, Tranchini only determines whether a proof has sense or not but does not go further into what the sense of a proof exactly consists of, so there might be further questions worth pursuing.
We will spell out an account of a distinction between sense and denotation of proofs, which can be considered a full-fledged analogy to Frege's distinction concerning singular terms and sentences.[There is some literature also in the field of proof theory concerned with this Fregean distinction, however, to our knowledge, apart from [26] this is not concerned with the sense of derivations but with the sense of sentences: cf. P. Martin-Löf (2001). The Sense/Reference Distinction in Constructive Semantics. Transcription of a lecture given at a conference on Frege organised by G. Sundholm at Leiden, 25 August 2001, transcription by B. Jespersen, 9 August 2002: https://www.academia.edu/25695205/The_Sense_Reference_Distinction_in_Constructive_Semantics, or [25].]
Another question concerns the relation of different kinds of proof systems (intuitionistic natural deduction (ND) and sequent calculus (SC) systems will be considered) with respect to such a distinction.
If we have two syntactically different derivations with the same denotation in different proof systems, do they always also differ in sense or can sense be shared over different systems?

§ CONNECTING STRUCTURE AND MEANING

The basic point of departure is the simple observation that there can be different ways leading from the same premises to the same conclusion, either in different proof systems or also within one system.
The focus in this matter so far has been on normal vs. non-normal derivations in ND and correspondingly on derivations containing cut vs. cut-free derivations in SC.
However, there can also simply be a change of the order of rule applications that can lead to syntactically different derivations from the same premises to the same conclusion.
Does this lead to a different denotation or should we say that it is only the sense that differs in such cases, while the underlying proof stays the same?

§.§ Normal form and the denotation of derivations

One and the same proof may be linguistically represented by different derivations.
We will follow the general opinion in taking proofs to be the denotation - the semantic value - of (valid) derivations.
In ND a derivation in normal form is the most direct form of representation of its denotation, i.e. the represented proof object.
For our purposes we will consider a derivation to be in normal form iff neither $\beta$- nor $\eta$-conversions (cf. rules below) can be applied to it.
A derivation in normal form in ND corresponds to a derivation in cut-free form in SC.
In intuitionistic logic derivations in non-normal form in ND (resp. with cut in SC) can be reduced to ones in normal form (resp. cut-free form).
These are then thought to represent the same underlying proof, just one more indirectly than the other, because, as Prawitz <cit.> says, they represent the same idea this proof is based on.
In order to make sense and denotation transparent, our approach will be to encode the derivations with $\lambda$-terms.
As is well known, by the Curry-Howard-isomorphism there is a correspondence between the intuitionistic ND calculus and the simply typed $\lambda$-calculus and we can formulate the following ND-rules annotated with $\lambda$-terms together with the usual $\beta$- and $\eta$-conversions for the terms.
The $\beta$-conversions correspond to the well-known reduction procedures, which can be formulated for every connective in ND <cit.>, while the $\eta$-conversions are usually taken to correspond to proof expansions <cit.>.
We use $p$, $q$, $r$,... for arbitrary atomic formulas, $A$, $B$, $C$,... for arbitrary formulas, and $\Gamma$, $\Delta$,... for sets of formulas.
$\Gamma$, $A$ stands for $\Gamma \cup \left\{A\right\}$.
For variables in terms $x$, $y$, $z$,... is used and $r$, $s$, $t$,... for arbitrary terms.

Term-annotated ND-rules:

[⊃I]λx.t:A ⊃B*t:BΓ,[x:A]
[⊃E]App(s, t):B*s: A ⊃BΓ    *t:AΔ

[∧I]⟨s, t⟩: A ∧B*s:AΓ   *t:BΔ
[∧E_1]fst(t):A*t:A ∧BΓ
[∧E_2]snd(t):B*t:A ∧BΓ

[∨I_1]s:A ∨B*s:AΓ
[∨I_2]s:A ∨B*s:BΓ
[∨E] r {x.s  | y.t}:C  *r: A ∨BΓ    *s:CΔ, [x:A]   *t: CΘ, [y:B]

App(λx.t, s)

fst(⟨s, t ⟩)

snd(⟨s, t ⟩)

r {x.s  | y.t}

r {x.s  | y.t}

$\lambda x.App(t, x) \rightsquigarrow t $ (if $x$ not free in $t$)

⟨fst(t), snd(t) ⟩⇝t

r {t.t  | s.s}

We read $x : A$ as “$x$ is a proof of $A$".
$t[t'/x]$ means that in term $t$ every free occurrence of $x$ is substituted with $t'$.
The usual capture-avoiding requirements for variable substitution are to be observed and $\alpha$-equivalence of terms is assumed.
A term that cannot be converted by either $\beta$- or $\eta$-conversion is in normal form.

Since there is a correspondence between intuitionistic SC and intuitionistic ND, for every derivation in ND there must be a derivation in SC named by the same $\lambda$-term.
This correspondence is of course not one-to-one, but many-to-one, i.e. for each proof in ND there are at least potentially different derivations in SC.[On the complications of such a correspondence and also on giving a term-annotated version of SC cf. e.g. [21], [31], [20], [13], [1], [18], [29]. Term-annotated sequent calculi can be found i.a. in [28] or [23], from which our presentation is only a notational variant.]
The following are our respective SC-rules, where we use the propositional fragment of an intuitionistic SC with independent contexts <cit.>.
The reduction procedures remain the same as above in ND; $\beta$-reduction corresponds to the procedures needed to establish cut-elimination, while $\eta$-conversion corresponds to what may be called “identicals-elimination" [12] or “identity atomization" [4][Showing that it is possible to get rid of axiomatic sequents with complex formulas and derive them from atomic axiomatic sequents. This is also part of cut-elimination but in principle those are separate procedures <cit.>.]:

Term-annotated G0ip:

Logical axiom:

[Rf]x : A ⊢x : A

Logical rules:

[∧R]Γ, Δ⊢⟨s, t⟩: A ∧BΓ⊢s: A   Δ⊢t: B
[∧L]Γ, z: A ∧B ⊢s[[fst(z)/x]snd(z)/y] : CΓ, x: A, y : B ⊢s : C

[∨R_1]Γ⊢s :A ∨BΓ⊢s:A
[∨R_2]Γ⊢s:A ∨BΓ⊢s:B
[∨L]Γ, Δ, z:A ∨B ⊢ {x.s  | y.t} : CΓ, x:A ⊢s:C   Δ, y:B ⊢t:C

[⊃R]Γ⊢λx.t:A ⊃BΓ, x:A ⊢t:B
[⊃L]Γ, Δ, x:A ⊃B ⊢s[App(x, t)/y]:CΓ⊢t: A   Δ, y:B ⊢s:C

[L]x: ⊢abort(x): C

Structural rules:

[W]Γ, x:A ⊢t:CΓ⊢t:C

[C]Γ, x : A ⊢t[x/y] : CΓ, x : A, y : A ⊢t : C

The rule of cut

[cut]Γ, Δ⊢s[t/x] : CΓ⊢t : D   Δ, x : D ⊢s : C

is admissible in G0ip.

In the left operational rules as well as in the weakening rule we have the case that variables occur beneath the line that are not explicitly mentioned above the line.
In these cases the variables must be either fresh or - together with the same type assignment - already occurring in the context $\Gamma$, $\Delta$, etc.
Same variables can only (but need not) be chosen for the same type, i.e., if a new type occurs in a proof, then a fresh variable must be chosen.
If we would allow to chose the same variable for different types, i.e. for example to let $x:A$ and $x:B$ occur in the same derivation this would amount to assuming that arbitrarily different formulas have the same proof, which is not desirable.

§.§ Identity of proofs and equivalence of derivations

Figuring prominently in the literature on identity of proofs is a conjecture by Prawitz <cit.> that two derivations represent the same proof iff they are equivalent.[Prawitz gives credit for this conjecture to Martin-Löf. Cf. also Martin-Löf <cit.> on this issue, in his terminology “definitional equality".]
This shifts the question of course to asking when two derivations can be considered equivalent.
Using the equational theory of the $\lambda$-calculus is one way to provide an answer here: terms on the right and the left hand side of the $\beta$- and $\eta$-conversions are considered denotationally equal <cit.>.
Hence, two derivations can be considered equivalent iff they are $\beta$-$\eta$-equal (cf. <cit.>, <cit.>, <cit.>).[There is some discussion about whether $\eta$-conversions are indeed identity-preserving. Martin-Löf <cit.> does not think so, for example. Prawitz <cit.> is not clearly decided but writes in the context of identity of proofs it would seem “unlikely that any interesting property of proofs is sensitive to differences created by an expansion". Widebäck [30], relating to results in the literature on the typed $\lambda$-calculus like [10] and [24], argues for $\beta$-$\eta$-equality to give the right account of identity of proofs and Girard <cit.> does the same, although he mentions, too, that $\eta$-equations “have never been given adequate status" compared to the $\beta$-equations.]
The denotation is then seen to be referred to by the term that annotates the formula or sequent to be proven.
We will call this the `end-term' henceforth so that we can cover and compare both ND and SC at once.
So if we have two derivations with essentially different end-terms (in the sense that they are not belonging to the same equivalence class induced by $\beta$-$\eta$-conversion), we would say that they denote essentially different proofs.
On the other hand, for two ND-derivations, where one reduces to the other (or both reduce to the same), e.g. via normalization, we have corresponding $\lambda$-terms, one $\beta$-reducible to the other (or both $\beta$-reducible to the same term).
In this case we would say that they refer to the same proof.
Prawitz <cit.> stresses that this seems evident since two derivations reducing to identical normal derivations must be seen as equivalent.
Note that we can also have the case that two derivations of the same formula, which would look identical in a non-term-annotated version, here for example of ND, are distinguished on the grounds of our term annotation, like the following two derivations:

ND1$p \supset (p \supset (p \wedge p))$

ND2$p \supset (p \supset (p \wedge p))$

[⊃I^2]λy.λx.⟨x, y ⟩: p ⊃(p ⊃(p ∧p))
[⊃I^1]λx.⟨x, y ⟩: p ⊃(p ∧p)
[∧I]⟨x, y ⟩: p ∧p[x : p]^1   [y : p]^2
[⊃I^2]λx.λy.⟨x, y ⟩: p ⊃(p ⊃(p ∧p))
[⊃I^1]λy.⟨x, y ⟩: p ⊃(p ∧p)
[∧I]⟨x, y ⟩: p ∧p[x : p]^2   [y : p]^1

The reason for this is that it is possible to generalize these derivations in different directions, which is made explicit by the variables.
Hence, the first one can be generalized to a derivation of $B \supset (A \supset (A \wedge B))$, while the second one generalizes to $A \supset (B \supset (A \wedge B))$.[For a more detailed examination of generalization cf. [30] or [3].]

So, encoding derivations with $\lambda$-terms seems like a suitable method to clarify the underlying structure of proofs.
There is one kind of conversion left, though, that needs consideration, namely what we will call permutative conversions, or also $\gamma$-conversions.[It goes under various other names, as well, like permutation/permuting conversions or commuting/commutative conversions. Some also prefer “reductions" but we will go with the - to us seemingly - more neutral “conversions". The term $\gamma$-conversions appears in [15]. Cf. about these conversions in general e.g. [22]: 251-259, [11]: Ch. 10, [2], [7].]
They become relevant here because we have disjunction as part of our logical vocabulary.
Prawitz [21] was the first to introduce these conversions.
In the conjunction-implication-fragment of intuitionistic propositional logic derivations in normal form satisfy the subformula property, i.e. in a normal derivation $\mathcal{D}$ of $A$ from $\Gamma$ each formula is either a subformula of $A$ or of some formula in $\Gamma$.
However, with the disjunction elimination rule this property is messed up, since we get to derive a formula $C$ from $A \vee B$ which is not necessarily related to $A$ or $B$.
That is why, in order to recover the subformula property, permutation conversions are introduced, which can be presented in their most general form in the following way:

D[∨E]C    *A ∨BΓ   *CΔ, A   *CΘ, B
[∨E]D   *A ∨BΓ   D*CΔ, A   D*CΘ, B

Whether or not these are supposed to be taken into the same league as $\beta$- and $\eta$-conversions in matters of identity preservation of proofs is an even bigger dispute than the one mentioned concerning $\eta$-conversions.
Prawitz <cit.> says that while there can be no doubt about the `proper reductions' having no influence on the identity of the proof, “[t]here may be some doubts concerning the permutative $\vee$E-[...]reductions in this connection" but does not go into that matter any further.
Since he needs these reductions to prove his normalization theorem, it seems that he would be inclined not to have too many doubts about identity preservation under the permutative conversions.
Girard <cit.>, on the other hand, does not seem to be convinced, as he says - considering an example of permutation conversion - that we are forced to identify “a priori different deductions" in these cases.
Even though he accepts these conversions for technical reasons, he does not seem to be willing to really identify the underlying proof objects.
Restall[Restall, G. (2017). Proof Terms for Classical Derivations. Article in progress: https://consequently.org/papers/proof-terms.pdf], however, analyzing derivations by assigning to them what he calls “proof terms" rather than $\lambda$-terms, considers the derivations above as merely distinct in representation but not in the underlying proof, which on his account is the same for both.
What is more, he does so not only for technical but rather philosophical reasons, since he claims the flow of information from premises to conclusion to be essentially the same.
Lindley <cit.> and Tranchini <cit.> both make a point about the connection between reductions and expansions (although they speak of certain kinds of “generalized" expansions) on the one hand and (“generalized") permutative conversions on the other, claiming that performing a (generalized) expansion on the left hand side of the conversion above followed by a reduction (and possibly $\alpha$-conversion) just yields the right hand side.
To conclude, if we only consider the $\supset$-$\wedge$-fragment of intuitionistic propositional logic, $\beta$-$\eta$-equality is enough, but if we consider a richer vocabulary, it seems to us at least that there are substantial reasons to include permutative conversions in our equational theory.[The consequence for this paper would be of course to add “$\gamma$-conversions" to the list of relevant conversions in our definitions about normal forms, identity of denotation, etc.]
We do not aim to make a final judgment on this issue here.
Rather, when we have laid out our distinction about sense and denotation of proofs below, we will consider the matter again and show why it makes no essential difference for our purposes whether we include permutative conversions or not.

§ THE SENSE OF DERIVATIONS

Let us spell out at this point what exactly we will consider as the sense and also again the denotation of a derivation in our approach:

Definition of denotation:
The denotation of a derivation in a system with $\lambda$-term assignment is referred to by the end-term of the derivation.
Identity of denotation holds modulo belonging to the same equivalence class induced by the set of $\alpha$-, $\beta$- and $\eta$-conversions of $\lambda$-terms, i.e. derivations that are denoted by terms belonging to the same equivalence class induced by these conversions are identical, they refer to the same proof object.[We use the more accurate formulation of “belonging to the same equivalence class" here instead of the formulation we used before of two terms “having the same normal form". The reason for this is that while these two properties coincide for most standard cases, they do not necessarily concur when it comes to Lindley's “general permutative conversions" or also to SC in general because in these cases the confluence property is not guaranteed. We want to thank one of the anonymous referees for indicating this important point.]

Definition of sense:
The sense of a derivation in a system with $\lambda$-term assignment consists of the set[One could also consider the question whether multi-sets are an even better choice here, which would of course yield a much stronger differentiation of senses. The reason why we consider sets instead of multi-sets is that to us the distinctions brought about by multi-sets, by e.g. a variable occurrence more or less, do not seem to go hand in hand with substantial differences in how inferences are built up.] of $\lambda$-terms that occur within the derivation.
Only a derivation made up of applications of correct inference rules, i.e. rules that have reduction procedures, can have sense.

§.§ Change of sense due to reducibility

Concerning a distinction between sense and denotation in the context of proofs, the rare cases where this is mentioned at all deal with derivations one of which is reducible to the other or with $\lambda$-terms which are $\beta$-convertible to the same term in normal form (cf. <cit.>, <cit.>, Restall 2017, p. 6).
Since Tranchini is the only one to spell out the part about sense in detail, we will briefly summarize his considerations.
As mentioned above, in his account, for a derivation to have sense means that it is made up of applications of correct inference rules.
The question to be asked then is of course what makes up correct inference rules?
Tranchini's answer is that inference rules are correct if they have reduction procedures available, i.e. a procedure to eliminate any maximal formula resulting from an application of an introduction rule immediately followed by an elimination rule of the same connective.
From a PTS point of view, applying reduction procedures can be seen as a way of interpreting the derivation because it aims to bring the derivation to a normal form, i.e. the form in which the derivation represents the proof it denotes most directly <cit.>.[Tranchini does not restrict his examination to derivations that normalize, though, but to the contrary, uses it to analyze non-normalizable derivations, like paradoxical ones.]
So the reduction procedures are the instructions telling us how to identify the denotation of the derivation, which for Tranchini means that they give rise to the sense of the derivation.
If we have two derivations denoting the same proof, for example, one in normal form and the other in a form that can be reduced to the former, we could say in Fregean terminology that they have the same denotation but differ in their sense because they denote the proof in different ways, one directly, the other indirectly.
So, we can take as an example the following two derivations, one in normal and one in non-normal form:

ND$p \supset p$

[x : p]
λx.x: p ⊃p

NDnon-normal $p \supset  p$

[x : p]
λx.x: p ⊃p
[y : q]
λy.y: q ⊃q
⟨λx.x, λy.y ⟩: (p ⊃p) ∧(q ⊃q)
fst(⟨λx.x, λy.y ⟩): p ⊃p

The latter obviously uses an unnecessary detour via the maximal formula $ (p \supset p) \wedge (q \supset q) $, which is introduced by conjunction introduction and then immediately eliminated again, thus, producing different and more complex terms than the former derivation.
The derivation can be easily reduced to the former, though, which can be also seen by $\beta$-reducing the term denoting the formula to be proven:

fst(⟨λx.x, λy.y ⟩)

We can also give an example analogous to the one above, where a non-normal term (highlighted in bold) in SC is created by using the cut rule:[Note however, that the connection between the application of cut and the resulting non-normal term is necessary but not sufficient, i.e. there can be applications of cut not creating a non-normal term. A non-normal term is produced if both occurrences of the cut formula in the premises are principal.]

SC$\vdash (p \wedge p) \supset  (p \vee p)$

z : p ⊢z : p
z : p, x : p ⊢z : p
y : p ∧p ⊢fst(y) : p
y : p ∧p ⊢fst(y) : p ∨p
⊢λy.fst(y) : (p ∧p) ⊃(p ∨p)

SCcut$\vdash (p \wedge p) \supset  (p \vee p)$

z : p ⊢z : p
z : p, x : p ⊢z : p
y : p ∧p ⊢fst(y) : p
z : p ⊢z : p
x : p, z : p ⊢z : p
y : p ∧p ⊢snd(y) : p
y : p ∧p, y : p ∧p ⊢⟨fst(y), snd(y)⟩: p ∧p
y : p ∧p ⊢⟨fst(y), snd(y)⟩: p ∧p
z : p ⊢z : p
z : p, x : p ⊢z : p
y : p ∧p ⊢fst(y) : p
y : p ∧p ⊢fst⟨fst(y), snd(y)⟩: p
y : p ∧p ⊢fst⟨fst(y), snd(y)⟩ : p ∨p
⊢λy.fst⟨fst(y), snd(y)⟩ : (p ∧p) ⊃(p ∨p)

λy.fst⟨fst(y), snd(y)⟩

In this case again the two derivations are essentially the same because the latter can be reduced to the former by eliminating the application of the cut rule.
Again, the proof object they represent is thus the same, only the way of making the inference, represented by the different terms occurring within the derivation, differs, i.e. the sense is different.

§.§ Change of sense due to rule permutations

So far we only considered the case in which there is an identity of denotation but a difference in sense of derivations due to one being represented by a $\lambda$-term in non-normal form reducible to one in normal form.
However, we want to show that this is not the only case where we can make such a distinction.
This is also the reason why our approach differs from Tranchini's (who works solely in an ND system) in how we grasp the notion of sense of a derivation.
Following Tranchini, the derivation having sense at all depends on there being reduction procedures available for the rules that are applied in it.
Since we are also interested in a comparison of sense-and-denotation relations between ND and SC systems, our approach requires that there are reduction procedures available for the created terms.
Thereby we will be able to cover both systems at once.

Encoding the proof systems with $\lambda$-terms also makes the connection between changing the order of the rule applications and the sense-and-denotation distinction transparent, which is the other case we want to cover.
In ND with disjunction rules it is possible to have rule permutations producing derivations with end-terms identifiable by means of the permutative conversions.
In SC, however, there are more cases of rule permutations possible.
When the left disjunction rule is involved, this also leads to different - though $\gamma$-equal - terms; with the left conjunction or implication rule the end-term remains completely unchanged.
Consider e.g. the following three derivations in SC of the same sequent $\vdash ((q \wedge r) \vee p) \supset ((p \vee q) \wedge (p \vee r))$:

SC$_{1\vdash ((q \wedge r) \vee p) \supset ((p \vee q) \wedge (p \vee r))}$

q ⊢q
q ⊢p ∨q
q, r ⊢p ∨q
q ∧r ⊢p ∨q
r ⊢r
r ⊢p ∨r
q, r ⊢p ∨r
q ∧r ⊢p ∨r
q ∧r, q ∧r ⊢(p ∨q) ∧(p ∨r)
q ∧r ⊢(p ∨q) ∧(p ∨r)
p ⊢p
p ⊢p ∨q
p ⊢p
p ⊢p ∨r
p, p ⊢(p ∨q) ∧(p ∨r)
p ⊢(p ∨q) ∧(p ∨r)
(q ∧r) ∨p ⊢(p ∨q) ∧(p ∨r)
⊢((q ∧r) ∨p) ⊃((p ∨q) ∧(p ∨r))

SC$_{2\vdash ((q \wedge r) \vee p) \supset ((p \vee q) \wedge (p \vee r))}$

q ⊢q
q, r ⊢q
q ∧r ⊢q
q ∧r ⊢p ∨q
r ⊢r
q, r ⊢r
q ∧r ⊢r
q ∧r ⊢p ∨r
q ∧r, q ∧r ⊢(p ∨q) ∧(p ∨r)
q ∧r ⊢(p ∨q) ∧(p ∨r)
p ⊢p
p ⊢p ∨q
p ⊢p
p ⊢p ∨r
p, p ⊢(p ∨q) ∧(p ∨r)
p ⊢(p ∨q) ∧(p ∨r)
(q ∧r) ∨p ⊢(p ∨q) ∧(p ∨r)
⊢((q ∧r) ∨p) ⊃((p ∨q) ∧(p ∨r))

SC$_{3\vdash ((q \wedge r) \vee p) \supset ((p \vee q) \wedge (p \vee r))}$

q ⊢q
q ⊢p ∨q
q, r ⊢p ∨q
q ∧r ⊢p ∨q
p ⊢p
p ⊢p ∨q
(q ∧r) ∨p ⊢p ∨q
r ⊢r
r ⊢p ∨r
q, r ⊢p ∨r
q ∧r ⊢p ∨r
p ⊢p
p ⊢p ∨r
(q ∧r) ∨p ⊢p ∨r
(q ∧r) ∨p, (q ∧r) ∨p ⊢(p ∨q) ∧(p ∨r)
(q ∧r) ∨p ⊢(p ∨q) ∧(p ∨r)
⊢((q ∧r) ∨p) ⊃((p ∨q) ∧(p ∨r))

The difference between SC1 and SC2 (highlighted in bold) is that the order of applying the right disjunction rule and the left conjunction rule is permuted.
The difference between SC1 and SC3 (highlighted with underlining) is that the order of applying the right conjunction rule and the left disjunction rule is permuted.
The order of applying the right disjunction rule and the left conjunction rule stays fixed this time.
Encoded with $\lambda$-terms, though, we see that in the first case, comparing SC1 and SC2, the permutation of rule applications produces exactly the same end-term.
Both derivations have the same end-term, namely:

$\boldsymbol{\lambda u.\texttt{case u}~\{v.\left\langle \texttt{inr}fst(v), \texttt{inr}snd(v) \right\rangle ~\vert~x.\left\langle \texttt{inl}x, \texttt{inl}x\right\rangle\}}$

SC$_{1\vdash ((q \wedge r) \vee p) \supset ((p \vee q) \wedge (p \vee r))}$

y : q ⊢y : q
y : q ⊢y : p ∨q
y : q, z : r ⊢y : p ∨q
v : q ∧r ⊢fst(v) : p ∨q
z : r ⊢z : r
z : r ⊢z : p ∨r
y : q, z : r ⊢z : p ∨r
v : q ∧r ⊢snd(v): p ∨r
v : q ∧r, v : q ∧r ⊢⟨fst(v), snd(v) ⟩: (p ∨q) ∧(p ∨r)
v : q ∧r ⊢⟨fst(v), snd(v) ⟩: (p ∨q) ∧(p ∨r)
x : p ⊢x : p
x : p ⊢x : p ∨q
x : p ⊢x : p
x : p ⊢x : p ∨r
x : p, x : p ⊢⟨x, x⟩: (p ∨q) ∧(p ∨r)
x : p ⊢⟨x, x⟩: (p ∨q) ∧(p ∨r)
u : (q ∧r) ∨p ⊢ {v.⟨fst(v), snd(v) ⟩ | x.⟨x, x⟩}  : (p ∨q) ∧(p ∨r)
⊢λu. {v.⟨fst(v), snd(v) ⟩ | x.⟨x, x⟩} : ((q ∧r) ∨p) ⊃((p ∨q) ∧(p ∨r))

SC$_{2\vdash ((q \wedge r) \vee p) \supset ((p \vee q) \wedge (p \vee r))}$

y : q ⊢y : q
y : q, z : r ⊢y : q
v : q ∧r ⊢fst(v) : q
v : q ∧r ⊢fst(v) : p ∨q
z : r ⊢z : r
y : q, z : r ⊢z : r
v : q ∧r ⊢snd(v) : r
v : q ∧r ⊢snd(v): p ∨r
v : q ∧r, v : q ∧r ⊢⟨fst(v), snd(v) ⟩: (p ∨q) ∧(p ∨r)
v : q ∧r ⊢⟨fst(v), snd(v) ⟩: (p ∨q) ∧(p ∨r)
x : p ⊢x : p
x : p ⊢x : p ∨q
x : p ⊢x : p
x : p ⊢x : p ∨r
x : p, x : p ⊢⟨x, x⟩: (p ∨q) ∧(p ∨r)
x : p ⊢⟨x, x⟩: (p ∨q) ∧(p ∨r)
u : (q ∧r) ∨p ⊢ {v.⟨fst(v), snd(v) ⟩ | x.⟨x, x⟩}  : (p ∨q) ∧(p ∨r)
⊢λu. {v.⟨fst(v), snd(v) ⟩ | x.⟨x, x⟩}  : ((q ∧r) ∨p) ⊃((p ∨q) ∧(p ∨r))

Considering the second comparison between SC1 and SC3 the situation is different: here the permutation of rule applications leads to a different end-term.
In the end-term for SC1 and SC2 the pairing operation is embedded within the case expression, whereas in the end-term for SC3 the case expression is embedded within the pairing:

$\lambda u.\left\langle \texttt{case u}~\{v.\texttt{inr}fst(v) ~\vert~x.\texttt{inl}x\}, \texttt{case u}~\{v.\texttt{inr}snd(v)~\vert~x.\texttt{inl}x\}\right\rangle$

SC$_{3\vdash ((q \wedge r) \vee p) \supset ((p \vee q) \wedge (p \vee r))}$

y : q ⊢y : q
y : q ⊢y : p ∨q
y : q, z : r ⊢y : p ∨q
v : q ∧r ⊢fst(v) : p ∨q
x : p ⊢x : p
x : p ⊢x : p ∨q
u : (q ∧r) ∨p ⊢ {v.fst(v)  | x.x} : p ∨q
z : r ⊢z : r
z : r ⊢z : p ∨r
y : q, z : r ⊢z : p ∨r
v : q ∧r ⊢snd(v) : p ∨r
x : p ⊢x : p
x : p ⊢x : p ∨r
u : (q ∧r) ∨p ⊢ {v.snd(v)  | x.x}: p ∨r
u : (q ∧r) ∨p, u : (q ∧r) ∨p ⊢⟨ {v.fst(v)  | x.x},  {v.snd(v)  | x.x}⟩: (p ∨q) ∧(p ∨r)
u : (q ∧r) ∨p ⊢⟨ {v.fst(v)  | x.x},  {v.snd(v)  | x.x}⟩: (p ∨q) ∧(p ∨r)
⊢λu.⟨ {v.fst(v)  | x.x},  {v.snd(v)  | x.x}⟩: ((q ∧r) ∨p) ⊃((p ∨q) ∧(p ∨r))

When we take a look at how the term-annotated rules must be designed in order to have a correspondence to the respective rules in ND, we see why some permutations of rule applications lead to different end-terms, while others do not; and why SC is in general more flexible in this respect than ND.
In SC the left conjunction rule as well as the left implication rule are substitution operations, i.e. they can change their place in the order without affecting the basic term structure because only in the inner term structure terms are substituted with other terms.[For $\supset$L the only exception is when an application of this rule is permuted with an application of $\vee$L, which creates a different, though $\gamma$-convertible term.]
In ND, on the other hand, there are no substitution operations used in the term assignment, i.e. for each rule application a new basic term structure is created.

How is this related to the distinction between sense and denotation?
In cases like SC1 vs. SC2 the way the inference is given differs, which can also be seen in different terms annotating the formulas occurring within the derivation: with otherwise identical terms in the two derivations y and z only occur in SC1, while fst(v) and snd(v) only occur in SC2.
However, the resulting end-term stays the same, thus, we would describe the difference between these derivations as a difference in sense but not in denotation.
In other cases, when disjunction elimination or the left disjunction rule is involved, permutation of rule applications can lead to a different end-term, as we see above in SC1 vs. SC3.
Whether this corresponds to a difference in denotation depends on whether we accept $\gamma$-conversions to be identity-preserving.
What all cases have in common, though, is that rule permutation always leads to a difference in sense of the given derivations because the sets of terms occurring within the derivations differ from each other.

§.§ Philosophical motivation

Let us have a look at how the Fregean conception of sense is received in the literature in order to show the philosophical motivation for adopting such a definition of sense for derivations.
According to Dummett <cit.>, Fregean sense is to be considered as a procedure to determine its denotation.[This idea of sense as procedures also occurs in more recent publications like [17] or [6].]
Girard <cit.>, in a passage about sense and denotation and the relation between proofs and programs, mentions that the sense is determined by a “sequence of instructions" and when we see in this context terms as representing programs and “the purpose of a program [...] to calculate [...] its denotation" (ibid., p. 17), then it seems plausible to view the terms occurring within the derivation, decorating the intermediate steps in the construction of the complex end-term that decorates the conclusion, as the sense of that derivation.
Tranchini holds the reduction procedures to be the sense because these `instructions' lead to the term in normal form.
However, in our framework - because we do not only consider normal vs. non-normal cases - it seems more plausible to look at the exact terms occurring within the derivations and view them as representing the steps in the process of construction encoding how the derivation is built up and leading us to the denotation, the end-term.
For us it is therefore only a necessary requirement for the derivation to have sense to contain only terms for which reduction procedures are available but it does not make up the sense.
In the case of rule permutation we can then say that the proof is essentially the same but the way it is given to us, the way of inference, differs: i.e. the sense differs.
This can be read off from the set of terms that occur within the derivation: they end up building the same end-term, but the way it is built differs, the procedures to determine the denotation differ.
Thus, this allows us to compare differences in sense within one proof system as well as over different proof systems.

Troelstra and Schwichtenberg <cit.> e.g. give an example of two derivations in SC producing the same end-term in different ways to show that just from the variables and the end-term we cannot read off how the derivation is built up:[For simplicity we omit the weakening steps that would strictly seen have to precede the applications of the $\wedge$L-rule.]

SC1$\vdash (s \wedge p) \supset ((q \wedge r) \supset (p \wedge q))$

x : p ⊢x : p
y : q ⊢y : q
x : p, y : q ⊢⟨x, y ⟩: p ∧q
x : p, z : q ∧r ⊢⟨x, fst(z) ⟩: p ∧q
u: s ∧p, z : q ∧r ⊢⟨snd(u), fst(z) ⟩: p ∧q
u : s ∧p ⊢λz.⟨snd(u), fst(z) ⟩: (q ∧r) ⊃(p ∧q)
⊢λu.λz.⟨snd(u), fst(z) ⟩: (s ∧p) ⊃((q ∧r) ⊃(p ∧q))

SC2$\vdash (s \wedge p) \supset ((q \wedge r) \supset (p \wedge q))$

x : p ⊢x : p
y : q ⊢y : q
x : p, y : q ⊢⟨x, y ⟩: p ∧q
u : s ∧p, y: q ⊢⟨snd(u), y ⟩: p ∧q
u: s ∧p, z : q ∧r ⊢⟨snd(u), fst(z) ⟩: p ∧q
u : s ∧p ⊢λz.⟨snd(u), fst(z) ⟩: (q ∧r) ⊃(p ∧q)
⊢λu.λz.⟨snd(u), fst(z) ⟩: (s ∧p) ⊃((q ∧r) ⊃(p ∧q))

The senses of these derivations would be the following:

Sense of SC1:

\begin{multline*}
\{x, y, z, u, \left\langle x, y \right\rangle, \underline{\left\langle x, fst(z) \right\rangle}, \left\langle snd(u), fst(z) \right\rangle, \lambda z.\left\langle snd(u), fst(z) \right\rangle,\\
\lambda u.\lambda z.\left\langle snd(u), fst(z) \right\rangle \}
\end{multline*}

Sense of SC2:

\begin{multline*}
\{x, y, z, u, \left\langle x, y \right\rangle, \underline{\left\langle snd(u), y \right\rangle}, \left\langle snd(u), fst(z) \right\rangle, \lambda z.\left\langle snd(u), fst(z) \right\rangle,\\ \lambda u.\lambda z.\left\langle snd(u), fst(z) \right\rangle\}
\end{multline*}

The two sets only differ with regard to the underlined terms, otherwise they are identical.
Thus, they only differ in the order in which the two left conjunction rules are applied.
For the resulting end-term this is inessential, but we can see that when taking the sense, and not only the end-terms, i.e. the denotation, into account, it is indeed possible to read off the structure of the derivations.
As noted above (examples on p. 6), the term annotation of the calculi makes this structure of derivations explicit so that we can differentiate between derivations which would otherwise look identical.
As several authors point out, this is a desirable feature if one is not only interested in mere provability but wants to study the structure of the derivations in question (cf. <cit.>, <cit.>) and also, for simplicity, if one wants to compare proof systems of ND and SC with each other <cit.>.
Since we are interested in both of these points, it seems the right choice for our purposes to consider the annotated versions of the calculi and that is also why these annotated versions are indeed needed for our notions of sense and denotation.
Of course, one could argue that the underlying structure is still the same in the non-annotated versions and can be made explicit by other means, too, like showing the different generalizations of the derivations, but still, we do not see how in these calculi our notions could be easily applied.

Another issue that needs to be considered is the one of identity of senses, i.e. synonymy.
Therefore, we want to extend our definition of sense given above with an addition:

If a sense-representing set can be obtained from another by uniformly replacing (respecting the usual capture-avoiding conventions) any occurrence of a variable, bound or free, by another variable of the same type, they express the same sense.

What we ensure with this point is just that it does not (and should not) matter which variables one chooses for which proposition as long as one does it consistently.
So, it does not make a difference whether we have

ND1$p \supset (q \supset p)$

[x : p]
λz.x: q ⊃p
λx. λz.x: p ⊃(q⊃p)

Sense1: {$x, \lambda z.x, \lambda x. \lambda z.x$}

ND2$p \supset (q \supset p)$

[y : p]
λz.y: q ⊃p
λy. λz.y: p ⊃(q⊃p)

Sense2: {$y, \lambda z.y, \lambda y. \lambda z.y$}

Sense1 and Sense2 represent the same sense.
Or to give another example (pointed to by one of the anonymous referees) where we have free variables occurring within the derivation but not appearing in the end-term: If one would replace all occurrences of the free variable $y$ by the variable $w$ in derivation SC1$\vdash (s \wedge p) \supset ((q \wedge r) \supset (p \wedge q))$ (cf. above), then this would make no difference to the sense according to our definition since the sense-representing sets would be obtained from replacing $y$ by $w$.

This also fits the Fregean criterion of two sentences' identical sense, as Sundholm <cit.> depicts it within a broader analysis: two propositions express the same sense if it is not possible to hold different epistemic attitudes towards them, i.e. “if one holds the one true, one also must hold the other one true, and vice versa".
Whereas, if we have two sentences which only differ in two singular terms, referring to the same object but differing in sense, we can easily hold the one sentence to be true, while thinking the other is false, if we do not know that they are referring to the same object.
With proofs it is the same: Looking at ND1$p \supset (q \supset p)$ and ND2$p \supset (q \supset p)$ we may not know whether the derivation is valid or not, we do know, however, that if one is a valid derivation then so is the other.
With derivations differing in sense this is not so straightforward.

For Frege this point of considering cases where intensionality is directed towards sentences was crucial to develop his notion of sense, so the question arises how we can explain cases of intensionality directed towards proofs with our notions of sense and denotation.
Let us suppose we have two denotationally-identical proofs which are represented by two different derivations $\mathcal{D}$ and $\mathcal{D'}$.
In this case it could happen that a (rational) person believes that derivation $\mathcal{D}$ is valid but does not believe that derivation $\mathcal{D'}$ is valid.
How can we account for that?
One explanation would be of course to point to the difference in linguistic representation.
After all, it can just be the case that one way of writing down a proof is more accessible to the person than another (they may not be familiar with a certain proof system, for example).
This would amount to letting the linguistic representation, the signs, collapse with the sense of a derivation.
However, then we would have no means to distinguish this case from cases in which we want to argue that it is not justified for a rational person to have different propositional attitudes towards propositions which are about derivations differing insignificantly from each other, like in the cases of ND1$p \supset (q \supset p)$	and ND2$p \supset (q \supset p)$ above.
For Frege <cit.> the referent of an expression in an intensional context is not its customary referent, i.e. the object it refers to or the truth value in the case of sentences, but its customary sense.
Here the situation is the same: What is referred to in such a setting, when speaking about the attitudes of a person towards propositions about derivations, is not the proof objects (which are identical in our situation) but their senses, which are in this context represented by the sets of terms encoding the steps of construction.
It seems plausible then to say that when the construction steps differ in two derivations, a person can have different attitudes towards propositions about them, because the different construction steps may lead to this person grasping the one derivation, while not understanding the other.

§ ANALOGY TO FREGE'S CASES

Let us finally compare how our conception of sense and denotation in the context of proofs fits the distinction Frege came up with for singular terms and sentences.
We can have the following two cases with Frege's distinction: firstly (cf. <cit.>), there can be different signs corresponding to exactly one sense (and then of course also only one denotation).
In the case of singular terms an example would be “Gottlob's brother” and “the brother of Gottlob".
The sense, the way the denoted individual object is given to us, is the same because there is only a minor grammatical difference between the two expressions.
More frequently, this occurs in comparing different languages, though, taking singular terms which express exactly the same sense only using different words, like “the capital of France" and “die Hauptstadt Frankreichs".
In the case of sentences an example would be changing from an active to a passive construction without changing the emphasis of the sentence; an example from Frege is the following: “$M$ gave document $A$ to $N$", “Document $A$ was given to $N$ by $M$" <cit.>.
In the case of proofs, finally, an example would be the following case:

ND$ (p\vee p) \supset (p\wedge p)$

[y : p ∨p]^3
[x : p]^1
[x : p]^1
{x.x | x.x} : p
[y : p ∨p]^3
[x : p]^2
[x : p]^2
{x.x | x.x} : p
⟨ {x.x | x.x},  {x.x | x.x}⟩: p ∧p
λy.⟨ {x.x | x.x},  {x.x | x.x}⟩ : (p ∨p) ⊃(p ∧p)

SC$\vdash (p\vee p) \supset (p \wedge p)$

x : p ⊢x : p
x : p ⊢x : p
y : p ∨p ⊢ {x.x | x.x} : p
x : p ⊢x : p
x : p ⊢x : p
y : p ∨p ⊢ {x.x | x.x}: p
y : p ∨p , y : p ∨p ⊢⟨ {x.x | x.x},  {x.x | x.x} ⟩: p ∧p
y : p ∨p ⊢⟨ {x.x | x.x},  {x.x | x.x}⟩: p ∧p
⊢λy.⟨ {x.x | x.x},  {x.x | x.x}⟩: (p ∨p) ⊃(p ∧p)

\begin{multline*}
\{x, y, \texttt{case y}~\{x.x~\vert~x.x\}, \left\langle \texttt{case y}~\{x.x~\vert~x.x\}, \texttt{case y}~\{x.x~\vert~x.x\}\right\rangle,\\ \lambda y.\left\langle \texttt{case y}~\{x.x~\vert~x.x\}, \texttt{case y}~\{x.x~\vert~x.x\}\right\rangle\}
\end{multline*}

Or to give another example:

ND$p \supset (p \supset (p \wedge p))$

[x : p]^2
[y : p]^1
⟨x, y ⟩: p ∧p
λy.⟨x, y ⟩: p ⊃(p ∧p)
λx.λy.⟨x, y ⟩: p ⊃(p ⊃(p ∧p))

SC$\vdash p \supset (p \supset (p \wedge p))$

x : p ⊢x : p
y : p ⊢y : p
x : p, y : p ⊢⟨x, y ⟩: p ∧p
x : p ⊢λy.⟨x, y ⟩: p ⊃(p ∧p)
⊢λx.λy.⟨x, y ⟩: p ⊃(p ⊃(p ∧p))

Sense: $\{x, y, \left\langle x, y \right\rangle, \lambda y.\left\langle x, y \right\rangle, \lambda x.\lambda y.\left\langle x, y \right\rangle\} $

In these cases derivations can consist of different signs, namely by having one representation in SC and one in ND, which do not differ in sense nor in denotation, since they both contain exactly the same terms and produce the same end-term.
This comparison between different proof systems seems to fit nicely with Frege's <cit.> comment on “the same sense ha[ving] different expressions in different languages".
However, as we have seen above with the examples ND1$p \supset (q \supset p)$ and ND2$p \supset (q \supset p)$, this case can also occur within the same proof system.
One could wonder whether there should not be a differentiation between the senses of the derivations in the first example since it seems that different rules are applied: in SC$\vdash (p\vee p) \supset (p \wedge p)$ we have an application of contraction, which we do not have in ND$ (p\vee p) \supset (p\wedge p)$.
This would also question whether our definition of sense distinguishes and identifies the right amount of cases.
We do believe that this is the case, though, because in the first example, where there is an application of the contraction rule in SC, there is also a multiple assumption discharge in the ND-derivation, which is generally seen as the corresponding procedure, just as cases of vacuous discharge of assumptions in ND correspond to the application of weakening in SC.
So just as in different languages of course not exactly the same expressions are used, here too, the rules differ from ND to SC but since the corresponding procedures are used, one can argue that the sense does not differ for that reason.

Another case that can occur according to Frege (ibid.) is that we have one denotation, i.e. one object a sign refers to, but different senses.
An example for this would be his famous “morning star" and “evening star" comparison, where both expressions refer to the same object, the planet Venus, but the denoted object is given differently.
On the sentence level this would amount to exchanging singular terms in a sentence by ones which have the same denotation: “The morning star is the planet Venus" and “The evening star is the planet Venus".
The denotation of the sentence - with Frege: its truth value - thus stays the same, only the sense of it differs, the information is conveyed differently to us.
For our proof cases we can say that this case is given when we have syntactically different derivations, be it in one or in different proof systems, which have end-terms belonging to the same equivalence class induced by the set of $\alpha$-, $\beta$- and $\eta$-conversions.
Thus, examples would be corresponding proofs in ND and SC, which share the same end-term, but contain different terms occurring within the derivations.
The reason for this to happen seems that in SC often more variables are necessary than in ND.
If we compare derivations within ND, one definite case in which we have the same denotation but a different sense is between equivalent but syntactically distinct derivations, e.g. non-normal and normal derivations, one reducible to the other.
Another case up for debate would be the one with rule permutations due to disjunction elimination.
Within SC we can have two cases: one due to rule permutation, one due to applications of cut.
For the first case, where the inference could be given in a different way, although ending on the same term, we gave examples above (cf. p. 12 and 14f.).
However, it is worth mentioning that our distinction still captures the usual distinction, the second case, where it is said that two derivations, one containing cut and the other one in cut-free form (as a result of cut-elimination applied to the former), have the same denotation but differ in sense:

SC$\vdash (p\wedge p) \supset (p\vee p)$

z : p ⊢z : p
z : p, x : p ⊢z : p
y : p∧p ⊢fst(y) : p
y : p ∧p ⊢fst(y) : p ∨p
⊢λy.fst(y) : (p ∧p) ⊃(p ∨p)

Sense: $\{z, x, y, fst(y), \texttt{inl}fst(y), \lambda y.\texttt{inl}fst(y)\}$

SCcut$\vdash (p\wedge p) \supset (p\vee p)$

z : p ⊢z : p
z : p, x : p ⊢z : p
y : p ∧p ⊢fst(y) : p
z : p ⊢z : p
z : p ⊢z: p ∨p
y : p ∧p ⊢fst(y) : p ∨p
⊢λy.fst(y): (p ∧p) ⊃(p ∨p)

Sense: $\{z, x, y, fst(y), \underline{\texttt{inl}z}, \texttt{inl}fst(y), \lambda y.\texttt{inl}fst(y)\}$

As mentioned above (fn 14), cut does not need to create a non-normal term, as it is the case here, but still any application of cut will necessarily change the sense of a derivation as opposed to its cut-free form.

Finally, cases that need to be avoided in a formal language according to Frege <cit.> would be to have one sign, corresponding to different senses, or on the other hand, one sense corresponding to different denotations.
As he mentions, these cases of course occur in natural languages but should not happen in formal ones, so it should also not be possible in our present context, for sure.
Fortunately, this cannot happen in the context of our annotated proof systems, either, since the signs (taken to be the derivation as it is written down) always express at most one sense in our annotated system, and likewise the sense always yields a unique denotation since the end-term is part of the sense-denoting set.[Another question would be whether there can be signs without any sense at all. Frege <cit.> dismisses this case, as well, with a remark that we need at least the requirement that our expressions are “grammatically well-formed". Tranchini [26] gives a good analogy pointing to the notorious connective  playing this role in the case of proofs.]

§ CONCLUSION

The context in which Frege considered sense and denotation was the context of identity.
Likewise, we argued in this paper, if we use term-annotated calculi, we can also say something about proof identity: identity of proofs over different calculi or within the same calculus consists in having end-terms that belong to the same equivalence class induced by the set of $\alpha$-, $\beta$- and $\eta$-conversions.
In ND this can happen when we have the same proof in normal and non-normal form, in SC this can happen when we have the same proof using cut and in cut-free form but also when there are forms of rule permutations where an application of the $\wedge$L-rule or the $\supset$L-rule switches place with another rule.
Including disjunction in our language creates for both calculi the additional question of whether rule permutations including disjunction elimination (resp. the left disjunction rule) lead to a different proof, or whether these proofs should be identified.
We are more interested in sense, however, and here we can conclude that what in all these cases changes is the sense of the derivation in question.
Finally, considering the question of identity of sense, i.e. synonymy, and trying to follow Frege's conception on this matter, too, we can say the following: if two derivations are supposed to be identical in sense, this means that the way the inference is given is essentially the same, so the set of terms building up the end-term must be the same.
The end-term itself does not necessarily tell us anything about the structure of the proof.
Sense, on the other hand, is more fine-grained in that the set of terms occurring within the derivation reflects how the derivation is built up.
Especially in SC, where we can have different orders of rule applications leading up to the same end-term, the sense gives us means to distinguish on a more fine-grained level.

[1] Barendregt, H., & Ghilezan, S. (2000). Lambda terms for natural deduction, sequent calculus and cut elimination. Journal of Functional Programming, 10(1), 121–134.

[2] De Groote, P. (1999). On the Strong Normalisation of Natural Deduction with Permutation-Conversions. In P. Narendran, & M. Rusinowitch (Eds), Rewriting Techniques and Applications: RTA 1999 (pp. 45–59). Berlin/Heidelberg: Springer.

[3] Došen, K. (2003). Identity of Proofs Based on Normalization and Generality. Bulletin of Symbolic Logic, 9, 477–503.

[4] Došen, K. (2008). Cut Elimination in Categories. Springer.

[5] Dummett, M. (1973). Frege: Philosophy of Language. New York: Harper & Row.

[6] Duží, M., Jespersen, B., & Materna, P. (2010). Procedural Semantics for
Hyperintensional Logic: Foundations and Applications of Transparent Intensional Logic. Springer.

[7] Francez, N. (2017). On harmony and permuting conversions. Journal of Applied Logic, 21, 14–23.

[8] Frege, G. (1948) [1892]. Sense and Reference. The Philosophical Review, 57(3), 209–230.

[9] Frege, G. (1979). Posthumous Writings. Oxford: Basil Blackwell.

[10] Friedman, H. (1975). Equality between functionals. In R. Parikh (Ed.), Logic colloquium: Lecture notes in mathematics 453 (pp. 23–37). Berlin/Heidelberg: Springer.

[11] Girard, J.-Y. (1989). Proofs and Types. Cambridge: Cambridge University Press.

[12] Hacking, I. (1979). What is Logic? The Journal of Philosophy, 76(6), 285–319.

[13] Herbelin, H. (1994). A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure. Computer Science Logic, 61–75.

[14] Kreisel, G. (1971). A survey of proof theory II. In J.E. Fenstad (Ed.), Proceedings of the Second Scandinavian Logic Symposium (pp. 109–170). Amsterdam: North-Holland.

[15] Lindley, S. (2007). Extensional Rewriting with Sums. In S. Ronchi Della Rocca (Ed.), Typed Lambda Calculi and Applications: TLCA 2007 (pp. 255–271). Berlin/Heidelberg: Springer.

[16] Martin-Löf, P. (1975). About Models for Intuitionistic Type Theories and the Notion of Definitional Equality. In S. Kanger (Ed.), Proceedings of the Third Scandinavian Logic Symposium (pp. 81–109). Amsterdam: North-Holland.

[17] Muskens, R. (2005). Sense and the Computation of Reference. Linguistics and Philosophy, 28(4), 473–504.

[18] Negri, S., & von Plato, J. (2001). Structural Proof Theory. Cambridge/New York: Cambridge University Press.

[19] Pfenning, F. (2000). Structural Cut Elimination: I. Intuitionistic and Classical Logic. Information and Computation, 157, 84–141.

[20] Pottinger, G. (1977). Normalization as a homomorphic image of cut-elimination. Annals of Mathematical Logic, 12, 323–357.

[21] Prawitz, D. (1965). Natural Deduction. Stockholm: Almqvist & Wiksell.

[22] Prawitz, D. (1971). Ideas and results in proof theory. In J.E. Fenstad (Ed.), Proceedings of the Second Scandinavian Logic Symposium (pp. 235–307). Amsterdam: North-Holland.

[23] Sørensen, M., & Urzyczyn, P. (2006). Lectures on the Curry-Howard Isomorphism. Amsterdam: Elsevier Science.

[24] Statman, R. (1983). $\lambda$-definable functionals and $\beta\eta$ conversion. Archiv für Mathematische Logik, 23, 21–26.

[25] Sundholm, G. (1994). Proof-Theoretical Semantics and Fregean Identity Criteria for Propositions. The Monist, 77(3), 294–314.

[26] Tranchini, L. (2016). Proof-theoretic semantics, paradoxes and the distinction between sense and denotation. Journal of Logic and Computation, 26(2), 495–512.

[27] Tranchini, L. (2018). Stabilizing Quantum Disjunction. Journal of Philosophical Logic, 47, 1029–1047.

[28] Troelstra, A., & Schwichtenberg, H. (2000). Basic Proof Theory. 2nd ed., Cambridge: Cambridge University Press.

[29] Urban, C. (2014). Revisiting Zucker's Work on the Correspondence Between Cut-Elimination and Normalisation. In L. Pereira, E. Haeusler, & V. de Paiva (Eds), Advances in Natural Deduction: A Celebration of Dag Prawitz's Work (pp. 31–50). Dordrecht: Springer.

[30] Widebäck, F. (2001). Identity of Proofs. Stockholm: Almquist & Wiksell International.

[31] Zucker, J. (1974). The correspondence between cut-elimination and normalization. Annals of Mathematical Logic, 7, 1–112.