# Universal Relations of Energy Flow, Acoustic Spin and Torque for Near-Field
Acoustic Tweezers

Yang Long  Chenwen Yang  Hong Chen  Jie Ren  Corresponding author:
<EMAIL_ADDRESS>Center for Phononics and Thermal Energy Science, China-EU
Joint Lab On Nanophononics, Shanghai Key Laboratory of Special Artificial
Microstructure Materials and Technology, School of Physics Science and
Engineering, Tongji University, Shanghai 200092, China

###### Abstract

Acoustic spin, radiation torque, energy flow, and reactive power are of
significant importance from both fundamental and practical aspects,
responsible for flexible tweezer manipulations and near-field sound
directionality. Nevertheless, the intrinsic relations among these physical
quantities are far from clear. Here, we prove the universal geometric
relations among them in acoustics, independent on wave structure details.
Particularly, we connect acoustic spin and torque to the cross product of
time-averaged energy flow and reactive power, as well as to the local
vorticity of energy flow. These relations are universally valid, verified in a
variety of different acoustic systems. We also demonstrate the multipole
mechanical torques and forces generated in three acoustic near-field sources:
Janus, Huygens and Spin sources, applying on small lossy particles. These
universal geometric relations uncover hidden locking relations beyond simple
spin-momentum locking of near-field waves, and show the basic principles
between the acoustic spin, radiation torque, and energy flow, reactive power.

††preprint: APS/123-QED

Introduction

Since the pioneering works by J. H. Poynting, radiation force and energy flow
are studied for many decades, which are playing fundamental roles in optical
and acoustic tweezers. Meanwhile, the spin angular momentum (SAM) in the near-
field wave physics has attracted much attention recently: non-trivial
topological properties for surface optical waves Bliokh  _et al._ (2015a,
2019, 2014), selective optical excitations Bliokh  _et al._ (2015b); Aiello
_et al._ (2015), optical torque Bliokh and Nori (2015); Bekshaev  _et al._
(2015), and chiral quantum interaction enhancement Lodahl  _et al._ (2017).
The SAMs in acoustic and elastic waves have also been theoretically proposed
Long  _et al._ (2018) and experimentally verified Shi  _et al._ (2019) in
parallel, following with applications, $i.e.$ momentum-locked transverse SAM
in surface evanescent waves Shi  _et al._ (2019); Long  _et al._ (2018);
Bliokh and Nori (2019a) or mirror-symmetry breaking waveguide Long  _et al._
(2020a), multiphysics interactions between surface phononic waves and magnons
Zhang  _et al._ (2020) and self-rotation torques on lossy particles Shi  _et
al._ (2019); Toftul  _et al._ (2019). As unveiled in Refs. Picardi  _et al._
(2018); Long  _et al._ (2020b); Wei and Rodríguez-Fortuño (2020); Long  _et
al._ (2020c), there are another two important physical quantities in near-
field waves, time-averaged energy flow $\bm{\mathcal{J}}$ and reactive power
$\bm{\mathcal{R}}$, which exhibit inner symmetric relations in evanescent wave
modes, not only for acoustics Long  _et al._ (2020b); Wei and Rodríguez-
Fortuño (2020) but also for optics Picardi  _et al._ (2018); Long  _et al._
(2020c), resulting in fertile selective near-field excitations beyond spin-
momentum locking Long  _et al._ (2020b, c). These research works have
suggested possible connections among the SAM, $\bm{\mathcal{J}}$ and
$\bm{\mathcal{R}}$ in near-field waves, which however are still not clear, and
need to be uncovered.

In this work, we unveil the universal geometric relations in near-field
acoustic SAM and show the multipole mechanical torques fo near-field selective
sources. We find that the acoustic SAM density $\bm{s}$ and torques can be
directly related with the time-averaged energy flow $\bm{\mathcal{J}}$ and
reactive power vector $\bm{\mathcal{R}}$ as:
$\bm{s}\propto\bm{\mathcal{J}}\times\bm{\mathcal{R}}$ with right(left)
handedness in right (left) handed medium. The acoustic SAM and torque are also
related to the local vorticity of energy flow $\nabla\times\bm{\mathcal{J}}$,
resulting in universal existence conditions and geometric features for
acoustic SAM. We verify the relations in diverse systems, including surface
acoustic waves, surface Bessel waves, near-field acoustic sources, Bessel and
Laguerre- Gaussian beams with non-zero topological charges and so on. These
relations show hidden locking relations beyond simple spin-momentum locking of
near-field waves, and show the basic principles between the acoustic spin,
radiation torque, and energy flow, reactive power. Furthermore, the multipole
mechanical operations for various near-field acoustic sources have been
demonstrated. Our work would pave the way about the understanding of geometric
features of near-field wave physics and could inspire new insights for
acoustic tweezer manipulations.

Results

Universal relations between acoustic spin, energy flow, and reactive power.
The acoustic spin density is associated with the local acoustic velocity field
as $\bm{s}=\frac{\rho}{2\omega}{\rm Im}[\bm{v}^{*}\times\bm{v}]$ Shi  _et al._
(2019); Long  _et al._ (2018), where $\rho$ is the mass density of medium,
$\omega$ is the frequency, ${\rm Im}[\cdot]$ is the imaginary part and
$\bm{v}$ is the acoustic velocity vector field. Obviously, the nonzero
$\bm{s}$ will correspond to the circularly (or generally elliptical) polarized
velocity field, which makes $\bm{s}$ a local property of the velocity field.
Besides the SAM, there are two other important physical quantities in near-
field waves that can reflect flow directions and field confinements for
acoustic waves Long  _et al._ (2020b): the time-averaged energy flow
$\bm{\mathcal{J}}=\frac{1}{2}{\rm Re}[p^{*}\bm{v}]$ and the reactive power
vector $\bm{\mathcal{R}}=\frac{1}{2}{\rm Im}[p^{*}\bm{v}]$, where $p$ is the
pressure field and ${\rm Re}[\cdot]$(${\rm Im}[\cdot]$) is the real(imaginary)
part. From acoustic equations, the reactive power vector can be represented
as: $\bm{\mathcal{R}}=-\frac{1}{4\rho\omega}\nabla|p|^{2}$. Clearly, the
physical meaning of $\bm{\mathcal{R}}$ can be understood as the non-zero
gradient of the potential energy from the pressure field, so that of curl-free
nature $\nabla\times\bm{\mathcal{R}}=0$.

According to the definitions of $\bm{\mathcal{J}}$ and $\bm{\mathcal{R}}$,
${\rm Re}[p^{*}\bm{v}]=\frac{1}{2}(p^{*}\bm{v}+p\bm{v}^{*})$, and ${\rm
Im}[p^{*}\bm{v}]=\frac{1}{2i}(p^{*}\bm{v}-p\bm{v}^{*})$, we obtain that
$\bm{\mathcal{J}}\times\bm{\mathcal{R}}=\frac{|p|^{2}}{8}\frac{\bm{v}^{*}\times\bm{v}-\bm{v}\times\bm{v}^{*}}{2i}$.
Considering further ${\rm
Im}[\bm{v}^{*}\times\bm{v}]=\frac{1}{2i}(\bm{v}^{*}\times\bm{v}-\bm{v}\times\bm{v}^{*})$
and the definition of acoustic SAM density, we finally find a universal
geometric relation about the acoustic SAM as (More details in Supplementary
information):

$\bm{s}=\frac{4\rho}{\omega|p|^{2}}\bm{\mathcal{J}}\times\bm{\mathcal{R}}.$
(1)

From this cross product relation, we can see that although the acoustic spin
is physically defined by local velocities Shi  _et al._ (2019); Long  _et al._
(2018); Bliokh and Nori (2019a), it can be determined simultaneously by time-
averaged energy flows and spatially inhomogeneous field distributions. For
given $\bm{\mathcal{J}}$ and $\bm{\mathcal{R}}$ in acoustic waves, $\bm{s}$
becomes determinate and does not have inner degree of freedom like Jones
vector in transverse planes for polarized optical waves. The physical reason
of the locking relation between $\bm{s}$ and $\bm{\mathcal{R}}$ can be
understood as imperfect cancellations of neighbour spin momentum loops in
spatially inhomogeneous wave fields Bliokh  _et al._ (2014); Long  _et al._
(2018).

Further, considering $\nabla\times(p^{*}\bm{v})=\nabla p^{*}\times\bm{v}$
since $\nabla\times\bm{v}=0$ for the longitudinal wave, we can also obtain
another universal geometric relation as:

$\bm{s}=\frac{1}{\omega^{2}}\nabla\times\bm{\mathcal{J}},$ (2)

which reflects that the divergence-free $\bm{s}$ can be connected to the non-
zero local vorticity of $\bm{\mathcal{J}}$, relating to the local circulation
of energy flow in the zero loop limit. Combined with the universal geometric
relations, Eq. (1) and Eq. (2), it is readily to see that the inhomogeneous
potential energy gradient $\bm{\mathcal{R}}$ will lead to finite energy flow
vorticity $\nabla\times\bm{\mathcal{J}}$ for acoustics. In the following, we
will demonstrate several examples to improve understandings and show the
validity of the universal geometric relations.

Figure 1: Universal geometric features in acoustic surface evanescent waves. a
The directions of the time-averaged energy flow $\bm{\mathcal{J}}$ and
reactive power $\bm{\mathcal{R}}$ as the spatially gradient of the acoustic
field will determine the acoustic SAM density $\bm{s}$. b Although the surface
modes have the spin-momentum ($\bm{s}-\bm{\mathcal{J}}$) locking relation,
some spin for modes will be forbidden due to the extra locking of
$\bm{s}-\bm{\mathcal{R}}$. Figure 2: Universal geometric features in acoustic
surface Bessel waves and acoustic spin source $D_{x}+iD_{y}$. Their pressure
field $p$ (a,e) that is normalized by the maximum amplitude $p_{0}$, time-
averaged energy flow $\bm{\mathcal{J}}$ (b,f), reactive power
$\bm{\mathcal{R}}$ (c,g) and SAM density $\bm{s}$ (d,h) have been
demonstrated. Here, for surface Bessel waves, $k=1.2k_{0}$, $\ell=1$,
$\lambda$ is the wavelength. For the spin source, the region around the spin
source with the distance smaller than $\lambda/10$ (the center black circle)
is not shown for avoiding the singularity of the field, $D_{x}$ and $D_{y}$
denote the acoustic dipoles along $x$ and $y$ direction, respectively.

Verification of universal relations in diverse acoustic wave structures. The
first famous spatially confined propagating near-field wave should be surface
evanescent wave Shi  _et al._ (2019); Long  _et al._ (2018); Bliokh and Nori
(2019a). The SAM and spin-momentum locking of acoustic surface evanescent wave
have been observed and verified recently Shi  _et al._ (2019); Long  _et al._
(2020b). The physical reason behind spin-momentum locking in acoustic
evanescent waves was considered as the analogy of the quantum spin Hall
effects with non-zero spin Chern number Bliokh  _et al._ (2015a); Shi  _et
al._ (2019); Long  _et al._ (2018) and described by topological properties of
four-momentum operators for acoustic surface modes Bliokh and Nori (2019b).
Without the topological argument, the acoustic spin-momentum locking can be
naturally understood with the help of the universal geometric relations.
Considering the evanescent wave form $p=p_{0}e^{-\tau y}e^{i(kx-\omega t)}$,
where $\tau=\sqrt{k^{2}-k_{0}^{2}}$, $k_{0}=\omega/c$, $c$ is the sound speed
in the air, $y=0$ is the surface position, we can obtain that
$\bm{\mathcal{J}}=\frac{|p_{0}|^{2}}{2\rho\omega}ke^{-2\tau y}\bm{e}_{z}$,
$\bm{\mathcal{R}}=\frac{|p_{0}|^{2}}{2\rho\omega}\tau e^{-2\tau y}\bm{e}_{y}$
and $\bm{s}=\frac{|p_{0}|^{2}}{\rho\omega^{3}}k\tau e^{-2\tau y}\bm{e}_{z}$,
as shown in Fig. 1. It is readily to check that they satisfy the universal
geometric relations of Eq. (1) and Eq. (2). Although spin-momentum locking
reflects that the sign of SAM is strongly locked with $k$ Bliokh  _et al._
(2015a); Van Mechelen and Jacob (2016), it can not tell us which sign of the
SAM will be locked with the given $k$, but Eq. (1) does. As unveiled in Fig.
1, it is physically impossible for surface modes with $k>0$ to carry the SAM
$\bm{s}<0$. The Eq. (1) can be regarded as a hidden geometric property that
restricts and forbids spin-momentum pairs in topological surface modes Shi
_et al._ (2019); Bliokh and Nori (2019b). It is worth noting that although Eq.
(1) indicates the right-hand relation of $\bm{\mathcal{J}}$,
$\bm{\mathcal{R}}$ and $\bm{s}$, the left-hand relation (so that the forbidden
spin) would be possible in effective left-handed medium, $i.e.$, the double-
negative acoustic metamaterial with negative mass density and negative
compressibility simultaneously. The geometric relation of $\bm{\mathcal{J}}$,
$\bm{\mathcal{R}}$ and $\bm{s}$ in near-field waves described by Fig. 1 is
verified by the experimental data observed in Ref. Long  _et al._ (2020b).

The second example is the acoustic surface wave in the cylindrical
coordination. The acoustic surface Bessel waves
$p=p_{0}J_{\ell}(kr)e^{i\ell\varphi}e^{-\tau z}e^{-i\omega t}$ in Fig. 2(a)
will carry non-zero SAM, where $J_{\ell}(kr)$ is the Bessel function of the
first kind with order $\ell$, $\tau=\sqrt{k^{2}-k_{0}^{2}}$ and
$(r,\varphi,z)$ are the cylindrical coordinates in real space. One can obtain
$\bm{\mathcal{J}}=\frac{|p_{0}|^{2}}{2\rho\omega}\frac{\ell}{r}J_{\ell}^{2}(kr)e^{-2\tau
z}\bm{e}_{\varphi}$ in Fig. 2(b). Its Bessel-type inhomogeneous surface
acoustic field will induce non-zero spatially gradient of acoustic field
$\nabla|p|^{2}=J_{\ell}^{2}(kr)e^{-2\tau z}$, leading to nonzero
$\bm{\mathcal{R}}$, as shown in Fig. 2(c), such that
$\bm{\mathcal{R}}=\frac{|p_{0}|^{2}}{2\rho\omega}e^{-2\tau
z}(-\frac{k}{2}J_{\ell}(kr)(J_{\ell-1}(kr)-J_{\ell+1}(kr))\bm{e}_{r}+\tau
J^{2}_{\ell}(kr)\bm{e}_{z})$. According to the velocity fields, we can get
$\ell$-dependent SAM as:
$\bm{s}=\frac{|p_{0}|^{2}}{\rho\omega^{3}}\frac{\ell}{r}e^{-2\tau z}(\tau
J_{\ell}^{2}(kr)\bm{e}_{r}+\frac{k}{2}J_{\ell}(kr)(J_{\ell-1}(kr)-J_{\ell+1}(kr))\bm{e}_{z})$
in Fig. 2(d). Clearly, they satisfy the universal geometric relations of Eq.
(1) and Eq. (2).

The third example is the setup of near-field acoustic sources that have been
recently proposed and verified experimentally Long  _et al._ (2020b); Wei and
Rodríguez-Fortuño (2020), which can excite the evanescent modes selectively
according to the geometric and symmetric features of the source itself. As a
demonstration illustrated in Fig. 2(e-h), the acoustic spin source that can
selectively excite surface waves due to spin-momentum locking Long  _et al._
(2020b); Shi  _et al._ (2019); Bliokh and Nori (2019a) has exhibited
$\bm{\mathcal{J}}$ (f), $\bm{\mathcal{R}}$ (e), $\bm{s}$ (g) in Fig. 2, around
its near-field subwavelength regions (smaller than $\lambda$). We check that
these quantities around the near-field directional source also satisfy the
relations of Eqs. (1, 2). Furthermore, we also verify the validity of
universal geometric relations for far-field modes, including the wave
interference case, Bessel and Laguerre-Gaussian beams with non-zero
topological charges (The details can be found in Supplementary Information).

Figure 3:  Mechanical interactions between the lossy small particle and near-
field acoustic sources. a, the acoustic source placed at the original point
will apply non-zero force and torque on the small lossy particle with the
radius $a$($ka=0.1$). The distance between the source and particle is
$\lambda/2$; b,c the $\bm{\mathcal{J}}$, $\bm{\mathcal{R}}$ and torque $T_{z}$
induced by the Janus source ($M+D_{y}$). The solid line and circles denote the
analytical (Eq. 3) and numerical acoustic spin torques, respectively. The
radius means the absolute amplitude ($|T_{z}|$) and the color denotes the sign
(red for positive, blue for negative). $T_{z}$ are normalized by the maximum
of their absolute values; d,e the $\bm{\mathcal{J}}$, $\bm{\mathcal{R}}$ and
torque $T_{z}$ induced by the Huygens source ($M+iD_{x}$); f,g the
$\bm{\mathcal{J}}$, $\bm{\mathcal{R}}$ and torque $T_{z}$ induced by the Spin
source ($D_{x}+iD_{y}$); h, the circle array of 19 particles is placed near
the near-field sources with distance $R=\lambda/2$ initially. Their time
evolutions (after $t=1.5$s) are shown for: Janus source (i), Huygens source
(j) and Spin source (k). The lines denote the particles’ motion trajectories
and their colors mean the angular frequency $\omega_{s}$ of the particles’
self-rotations. $m=\frac{4}{3}a^{3}\rho_{d}$, $I_{s}=\frac{2}{5}ma^{2}$,
$\rho_{d}=2\rho$.

Universal relations for acoustic torques and forces. We find that similar
universal geometric relations also hold for the acoustic spin torque and
acoustic forces for small absorptive particles Toftul  _et al._ (2019);
Abdelaziz and Grier (2020); Marzo and Drinkwater (2018). We can follow Ref.
Toftul  _et al._ (2019) to obtain the acoustic SAM absorbing induced local
torque $\bm{T}$:

$\bm{T}=\frac{4\rho}{|p|^{2}}{\rm
Im}[\alpha_{d}]\bm{\mathcal{J}}\times\bm{\mathcal{R}}=\frac{{\rm
Im}[\alpha_{d}]}{\omega}\nabla\times\bm{\mathcal{J}},$ (3)

and the radiation force $\bm{F}=\bm{F}^{\rm grad}+\bm{F}^{\rm scat}$, as

$\displaystyle\bm{F}^{\rm grad}$ $\displaystyle=$
$\displaystyle-\frac{\omega}{c^{2}}({\rm Re}[\alpha_{m}]+{\rm
Re}[\alpha_{d}])\bm{\mathcal{R}}-\frac{1}{2\omega}{\rm
Re}[\alpha_{d}]\nabla^{2}\bm{\mathcal{R}},$ (4) $\displaystyle\bm{F}^{\rm
scat}$ $\displaystyle=$ $\displaystyle\frac{\omega}{c^{2}}({\rm
Im}[\alpha_{m}]+{\rm Im}[\alpha_{d}])\bm{\mathcal{J}}+\frac{1}{2\omega}{\rm
Im}[\alpha_{d}]\nabla^{2}\bm{\mathcal{J}},$ (5)

where $\alpha_{m}$ and $\alpha_{d}$ are the monopole and dipole
polarizabilities of the small lossy particle Toftul  _et al._ (2019).
$\bm{F}^{\rm grad}$ is the gradient part of total force with no curl
($\nabla\times\bm{F}^{\rm grad}=0$) and $\bm{F}^{\rm scat}$ is the scattering
part with no divergence ($\nabla\cdot\bm{F}^{\rm scat}=0$). As a consequence
of Eq. (1), for a small absorptive particle, we can obtain the following
geometric orthogonal constraints for the SAM torque and acoustic forces (See
Supplementary Information):

$\displaystyle\bm{T}\cdot\bm{F}^{\rm scat}$ $\displaystyle=\frac{1}{2}{\rm
Im}[\alpha_{d}]^{2}\bm{s}\cdot(\nabla^{2}\bm{\mathcal{J}}),$ (6)
$\displaystyle\bm{T}\cdot\bm{F}^{\rm grad}$ $\displaystyle=-\frac{1}{2}{\rm
Re}[\alpha_{d}]{\rm Im}[\alpha_{d}]\bm{s}\cdot(\nabla^{2}\bm{\mathcal{R}}).$

It is clear that the geometric orthogonal condition between radiation forces
and the SAM torque depends on whether $\bm{s}$ is orthogonal to
$\nabla^{2}\bm{\mathcal{R}}$ and $\nabla^{2}\bm{\mathcal{J}}$, or whether
$\nabla^{2}\bm{\mathcal{R}}$ and $\nabla^{2}\bm{\mathcal{J}}$ are zero. For
the surface evanescent wave, one can find $\bm{T}\perp\bm{F}^{\rm scat}$,
$\bm{T}\perp\bm{F}^{\rm gard}$, coinciding with previous predictions Toftul
_et al._ (2019); Bruus (2012). Generally, from Eq. (6), the orthogonality
between the SAM torque and the acoustic force is not guaranteed.

Now let us demonstrate the mechanical operations on small lossy particles
induced by selective near-field sources. The excited pressure field of sources
combined linearly by acoustic monopole $M$ and dipoles $\bm{D}$ can be written
as: $p(\bm{r})=i\rho\omega(MG(\bm{r})-\frac{1}{k}\bm{D}\cdot\nabla
G(\bm{r}))$, where $G(\bm{r})=\frac{e^{ikr}}{4\pi r}$ is the Green function
that the source is at the original point, $r=|\bm{r}|$ and $k=k_{0}$. For two-
dimension case, the Green function will be $G(\bm{r})=H_{0}^{(1)}(kr)$, where
$H_{0}^{(1)}$ is the Hankel function of the first kind. As shown in Fig. 3(a),
the dynamics of a small lossy particle driven by acoustic fields can be
described as: $m\frac{d^{2}\bm{r}}{dt^{2}}=\bm{F}$ and
$I_{s}\frac{d\bm{\omega}_{s}}{dt}=\bm{T}$, where $m$ is the mass and $\bm{r}$
is the position of the particle, $I_{s}$ is the moment of inertia and
$\bm{\omega}_{s}$ is the angular frequency along the particle’s own axis. We
consider that the particle radius $a$ is so small ($ka=0.1$) that the back-
action effect from the particle to wave fields is negligible. Specially,
according to Eq. (6), for near-field sources in 2D planes, their near-field
waves will induce the geometrically orthogonal radiation forces and spin
torques, $\bm{T}\perp\bm{F}^{\rm scat}$ and $\bm{T}\perp\bm{F}^{\rm gard}$,
namely, the forces are in plane while the torques are out of plane.

Here, we consider three typical near-field sources placed at the origin point
of the $xOy$ 2D dimension: acoustic Janus, Huygens and Spin sources Long  _et
al._ (2020b). The $\bm{\mathcal{J}}$, $\bm{\mathcal{R}}$ and the SAM torque
along the $z$-axis $T_{z}$ in the near-field region at the distance
$\lambda/2$ far away from the source are calculated in Fig. 3. Without loss of
generality, we consider the lossy particle with the relative density
$\overline{\rho}/\rho=2+0.5i$ and compressibility
$\overline{\beta}/\beta=3+0.7i$ Toftul  _et al._ (2019). For Janus source
$M+D_{y}$ in Fig. 3(b,c), the near-field directionality mainly comes from the
asymmetric $\bm{\mathcal{R}}$. Combining with the slightly asymmetric
$\bm{\mathcal{J}}$, Janus source produces the quadrupole-like spin torque:
$T_{z}(\theta)=-T_{z}(\theta+\pi/2)$, where $\theta={\rm arg}[x+iy]$ and ${\rm
arg}[\cdot]$ means the angle of the complex. For Huygens source $M+iD_{x}$ in
Fig. 3(d,e), it has both the directional $\bm{\mathcal{J}}$ and
$\bm{\mathcal{R}}$, producing the dipole-like SAM torque:
$T_{z}(\theta)=-T_{z}(-\theta)$. For Spin source $D_{x}+iD_{y}$ in Fig.
3(f,g), it induces the isotropic radiation pattern and monopole-like SAM
torque $T_{z}(\theta)={\rm const.}<0$. As verified, the universal geometric
relations Eqs. (1, 2, 3) are generally valid in these three near-field source
systems.

To demonstrate the effect of acoustic torques and radiation forces, we place
$19$ particles around these sources with the distance $R=\lambda/2$ initially,
and calculate their motions and trajectories, as illustrated in Fig. 3(i,j,k):
(i) Janus source; (j) Huygens source; (k) Spin source. From the simulations,
one can see that the particles’ trace and self-rotation angular frequencies
$\omega_{s,z}$ reflect the mechanical operations of different sources:
quadrupole, dipole and monopole-like SAM torque patterns. The details about
radiation forces of these sources can be found in Supplementary Information.

Figure 4: The acoustic pulling for the small lossy particle ($ka\ll 1$). a,b,c
For the near-field sources, they will trap particle at the different positions
(denoted as the black line) due to their characteristic near-field properties:
Janus source $M+D_{y}$ (a), Huygens source $M+iD_{x}$ (b) and one combination
$M+iD_{x}+D_{y}$ (c). d The relation between $F_{y}$ induced by the evanescent
wave and the distance of particle away from the interface. Obviously, the
particle will be trapped at $\approx-0.17\lambda$. e, the time evolution
(after $t=2$s) of the motion of particles placed around the distance
$=0.17\lambda$ away from the interface. Here, $|p_{0}|=400$ Pa, $k=1.5k_{0}$,
$F_{0}=|p_{0}|^{2}a^{2}\beta$, $F_{b}=0$ for the simplicity.

Besides pushing the particle, the near-field sources can also be exploited to
pull the particle. As we will see, when the particle is closing to the center
of near-field sources, the radiation pushing force may not be increasing, but
becomes decreasing and even changes to an attracting force. As shown in Fig.
4(a), in the region denoted by elliptical black line, the acoustic Janus
source will pull the particle to the source center, namely $F_{n}<0$. For
Huygens source in Fig. 4(b), the pulling region will be deformed and become
non-symmetric horizontally due to its relation with $\bm{\mathcal{J}}$ Long
_et al._ (2020b). Specially, the pulling region of the near-field source can
be manipulated by adjusting the linear combinations of acoustic monopole and
dipoles, as shown in Fig. 4(c). Therefore, the black line plays a reminiscent
role of the event horizon that particles within the critical region will
collapse into the center. The conventional surface acoustic wave
$p=p_{0}e^{\tau y}e^{ikx}$, $y\in(-\infty,0]$ can also be used to pull the
particle along the $y$ axis even considering the gravity along the $-y$ and
the buoyancy force $F_{b}$. Theoretically, there exists a critical condition
for the evanescent wave to pull the particles (See Supplementary Information):

$|p_{0}|^{2}\geqslant\frac{2\rho\omega^{2}(mg-F_{b})}{2\tau^{3}{\rm
Re}[\alpha_{d}]+\tau k_{0}^{2}{\rm Re}[\alpha_{d}+\alpha_{m}]}$ (7)

where $g$ is the gravitational acceleration. As an example as shown in Fig.
4(d), when the evanescent wave satisfies this condition, there is a region
$y>-0.17\lambda$ where the total force compose of acoustic force and gravity
points along $y$: $F_{y}>0$ so that the evanescent wave will pull the
particles to the surface. Based on the numerical simulations, we can see that
the particles released around $y=-0.17\lambda$ will have different traces: the
particles within distance $-0.17\lambda$ will be pulled to the surface and the
other particles will fall due to the gravity. Specially, due to spin-momentum
locking, all particles will have negative self-rotation angular frequencies
$\omega_{s,z}<0$.

To summarize, we have uncovered universal geometric relations of acoustic spin
and radiation torque with energy flow and reactive power in acoustics. The
intrinsic relations among. these acoustic quantities are. independent on wave
structure details. The acoustic SAM is generally related the cross product of
time-averaged energy flow and reactive power, as well as the local vorticity
of energy flow. Similar geometric relations have also been uncovered for
acoustic torques and forces, resulting in the geometrically orthogonal
conditions. Spin-related mechanical behaviours of different near-field
selective sources, Janus, Huygens and Spin sources have been demonstrated,
exhibiting the quadrupole, dipole, monopole-like spin torque behaviors,
respectively. Our work shows basic principles for physical mechanisms behind
the acoustic SAM and would inspire new applications for SAM-related wave
controls Zhang  _et al._ (2020); Long  _et al._ (2020c); Yuan  _et al._
(2021), near-field directional excitations Long  _et al._ (2020b); Shi  _et
al._ (2021) and mechanical operations for small particles Ding  _et al._
(2013); Tian  _et al._ (2020); Shen  _et al._ (2018). Our work would also be
meaningful for other wave field systems including optical Shi  _et al._ (2021)
and elastic waves Yuan  _et al._ (2021).

Data availability The data that support the findings of this study are
available from the corresponding author upon reasonable request.

Acknowledgments This work is supported by the National Natural Science
Foundation of China (Nos. 11935010 and 11775159) and the Opening Project of
Shanghai Key Laboratory of Special Artificial Microstructure Materials and
Technology.

Author Contributions Author contributions Y.L and J.R derived the the- ory and
developed the analysis. Y.L and C.Y carried out the numerical simulations. J.R
and H.C conceived the project. All the authors contributed to discussion,
interpreting the data and the writing.

Competing interests The authors declare no competing interests.

## References

  * Bliokh  _et al._ (2015a) Konstantin Y Bliokh, Daria Smirnova, and Franco Nori, “Quantum spin hall effect of light,” Science 348, 1448–1451 (2015a).
  * Bliokh  _et al._ (2019) Konstantin Y Bliokh, Daniel Leykam, Max Lein, and Franco Nori, “Topological non-hermitian origin of surface maxwell waves,” Nat. Commun. 10, 580 (2019).
  * Bliokh  _et al._ (2014) Konstantin Y Bliokh, Aleksandr Y Bekshaev, and Franco Nori, “Extraordinary momentum and spin in evanescent waves,” Nat. Commun. 5, 3300 (2014).
  * Bliokh  _et al._ (2015b) Konstantin Yu Bliokh, Francisco J Rodríguez-Fortuño, Franco Nori, and Anatoly V Zayats, “Spin–orbit interactions of light,” Nat. Photonics 9, 796–808 (2015b).
  * Aiello  _et al._ (2015) Andrea Aiello, Peter Banzer, Martin Neugebauer, and Gerd Leuchs, “From transverse angular momentum to photonic wheels,” Nat. Photonics 9, 789–795 (2015).
  * Bliokh and Nori (2015) Konstantin Y Bliokh and Franco Nori, “Transverse and longitudinal angular momenta of light,” Phys. Rep. 592, 1–38 (2015).
  * Bekshaev  _et al._ (2015) Aleksandr Y Bekshaev, Konstantin Y Bliokh, and Franco Nori, “Transverse spin and momentum in two-wave interference,” Phys. Rev. X 5, 011039 (2015).
  * Lodahl  _et al._ (2017) Peter Lodahl, Sahand Mahmoodian, Søren Stobbe, Arno Rauschenbeutel, Philipp Schneeweiss, Jürgen Volz, Hannes Pichler, and Peter Zoller, “Chiral quantum optics,” Nature 541, 473–480 (2017).
  * Long  _et al._ (2018) Yang Long, Jie Ren, and Hong Chen, “Intrinsic spin of elastic waves,” Proc. Natl. Acad. Sci. U.S.A. 115, 9951–9955 (2018).
  * Shi  _et al._ (2019) Chengzhi Shi, Rongkuo Zhao, Yang Long, Sui Yang, Yuan Wang, Hong Chen, Jie Ren, and Xiang Zhang, “Observation of acoustic spin,” Natl. Sci. Rev. 6, 707–712 (2019).
  * Bliokh and Nori (2019a) Konstantin Y Bliokh and Franco Nori, “Transverse spin and surface waves in acoustic metamaterials,” Phys. Rev. B 99, 020301 (2019a).
  * Long  _et al._ (2020a) Yang Long, Danmei Zhang, Chenwen Yang, Jianmin Ge, Hong Chen, and Jie Ren, “Realization of acoustic spin transport in metasurface waveguides,” Nat. Commun. 11, 4716 (2020a).
  * Zhang  _et al._ (2020) Xiang Zhang, Gerrit E. W. Bauer, and Tao Yu, “Unidirectional pumping of phonons by magnetization dynamics,” Phys. Rev. Lett. 125, 077203 (2020).
  * Toftul  _et al._ (2019) ID Toftul, KY Bliokh, MI Petrov, and F Nori, “Acoustic radiation force and torque on small particles as measures of the canonical momentum and spin densities,” Phys. Rev. Lett, 123, 183901 (2019).
  * Picardi  _et al._ (2018) Michela F Picardi, Anatoly V Zayats, and Francisco J Rodríguez-Fortuño, “Janus and huygens dipoles: near-field directionality beyond spin-momentum locking,” Phys. Rev. Lett, 120, 117402 (2018).
  * Long  _et al._ (2020b) Yang Long, Hao Ge, Danmei Zhang, Xiangyuan Xu, Jie Ren, Ming-Hui Lu, Ming Bao, Hong Chen, and Yan-Feng Chen, “Symmetry selective directionality in near-field acoustics,” Natl. Sci. Rev. 7, 1024–1035 (2020b).
  * Wei and Rodríguez-Fortuño (2020) Lei Wei and Francisco J Rodríguez-Fortuño, “Far-field and near-field directionality in acoustic scattering,” New J. Phys. 22, 083016 (2020).
  * Long  _et al._ (2020c) Yang Long, Jie Ren, Zhiwei Guo, Haitao Jiang, Yuqian Wang, Yong Sun, and Hong Chen, “Designing all-electric subwavelength metasources for near-field photonic routings,” Phys. Rev. Lett. 125, 157401 (2020c).
  * Bliokh and Nori (2019b) Konstantin Y Bliokh and Franco Nori, “Klein-gordon representation of acoustic waves and topological origin of surface acoustic modes,” Phys. Rev. Lett, 123, 054301 (2019b).
  * Van Mechelen and Jacob (2016) Todd Van Mechelen and Zubin Jacob, “Universal spin-momentum locking of evanescent waves,” Optica 3, 118–126 (2016).
  * Abdelaziz and Grier (2020) Mohammed A Abdelaziz and David G Grier, “Acoustokinetics: Crafting force landscapes from sound waves,” Phys. Rev. Research 2, 013172 (2020).
  * Marzo and Drinkwater (2018) Asier Marzo and Bruce W. Drinkwater, “Holographic acoustic tweezers,” Proc. Natl. Acad. Sci. U.S.A. 116, 84–89 (2018).
  * Bruus (2012) Henrik Bruus, “Acoustofluidics 7: The acoustic radiation force on small particles,” Lab Chip 12, 1014 (2012).
  * Yuan  _et al._ (2021) Weitao Yuan, Jinfeng Zhao, Yang Long, Jie Ren, and Zheng Zhong, “Multi-branch valley-chiral edge states of antisymmetric plate wave in phononic crystal plates with double-sided symmetric pillars,” Int. J. Mech. Sci. 197, 106347 (2021).
  * Shi  _et al._ (2021) Peng Shi, Luping Du, Congcong Li, Anatoly V. Zayats, and Xiaocong Yuan, “Transverse spin dynamics in structured electromagnetic guided waves,” Proc. Natl. Acad. Sci. U.S.A. 118, e2018816118 (2021).
  * Ding  _et al._ (2013) Xiaoyun Ding, Peng Li, Sz-Chin Steven Lin, Zackary S. Stratton, Nitesh Nama, Feng Guo, Daniel Slotcavage, Xiaole Mao, Jinjie Shi, Francesco Costanzo, and Tony Jun Huang, “Surface acoustic wave microfluidics,” Lab Chip 13, 3626 (2013).
  * Tian  _et al._ (2020) Zhenhua Tian, Zeyu Wang, Peiran Zhang, Ty Downing Naquin, John Mai, Yuqi Wu, Shujie Yang, Yuyang Gu, Hunter Bachman, Yaosi Liang, Zhiming Yu, and Tony Jun Huang, “Generating multifunctional acoustic tweezers in petri dishes for contactless, precise manipulation of bioparticles,” Sci. Adv. 6, eabb0494 (2020).
  * Shen  _et al._ (2018) Zhiyuan Shen, Thomas R. Neil, Daniel Robert, Bruce W. Drinkwater, and Marc W. Holderied, “Biomechanics of a moth scale at ultrasonic frequencies,” Proc. Natl. Acad. Sci. U.S.A. 115, 12200–12205 (2018).


# Resolution for Constrained Pseudo-Propositional Logic

Ahmad-Saher Azizi-Sultan  P.O. Box 30098
Taibah University
Medina Munawarah
Saudi Arabia<EMAIL_ADDRESS>
###### Abstract.

This work, shows how propositional resolution can be generalized to obtain a
resolution proof system for constrained pseudo-propositional logic (CPPL),
which is an extension resulted from inserting the natural numbers with few
constraints symbols into the alphabet of propositional logic and adjusting the
underling language accordingly. Unlike the construction of CNF formulas which
are restricted to a finite set of clauses, the extended CPPL does not require
the corresponding set to be finite. Although this restriction is made
dispensable, this work presents a constructive proof showing that the
generalized resolution for CPPL is sound and complete. As a marginal result,
this implies that propositional resolution is also sound and complete for
formulas with even infinite set of clauses.

###### Key words and phrases:

Propositional logic, resolution proof system, pseudo-Boolean constraints,
Constrained pseudo-propositional logic

###### 1991 Mathematics Subject Classification:

Primary 03B05; Secondary 03B22, 03F03, 05A05

##  1\. Introduction

The gradual improvements of SAT algorithms, developed over the last few
decades, have made them the ideal choice for approaching a wide range of
important problems such as formal verification [5, 6, 12], planning [9, 11],
scheduling [8] and so forth. Generally, these algorithms are based on the
resolution proof system, which is built within the framework of propositional
logic where formulas are represented by their CNF.

Naturally many important problems in different areas contain counting
constraints. Unfortunately the limitations of the expressive power of
propositional language does not allow for counting tools to be built within
the framework of the language itself. Thus, in general, encoding counting
constraints in CNF increases the number of clauses and variables extensively
[1, 4], resulting in impractical excessive complexity as SAT is one of the
canonical NP-complete problems [7]. This had motivated the development of
CPPL, which evolved from propositional logic by interpolating the natural
numbers with few constraint symbols into its alphabet and adjusting the
underlying language accordingly [2, 3]. The resulting evolved logic became
capable of formulating counting constraints or SAT instances naturally and
much more succinctly than having them being encoded using CNF. Moreover, its
evolved proof system retained its soundness and completeness [3]. The
inference rules involved are listed in Table 1. From this table, It can be
noticed that the list of inference rules is quite long and hence unfortunate
for computerized implementation. A proof system with fewer inference rules
results in less cases to be considered and enhances its complexity.

Analogously to propositional resolution, this work is presenting a resolution
proof system for CPPL, with only two rules involved, and showing that it is
sound and complete.

##  2\. Background

Consider the set of natural numbers, $\mathbb{N}$, and let
$\mathcal{P}=\\{p,p_{1},p_{2},\dots\\}$ be a finite or countably infinite set
of propositional variables.

###  2.1. PPL

The alphabet $\mathcal{A}$ underling the language of PPL is the union
$\mathbb{N}\cup\mathcal{P}\cup\left\\{\neg,+,\left(,\right)\right\\}$, where
the symbols $\neg$, $+$, (, and ) resemble the negation, addition, opening and
closing punctuation symbols, respectively.

The language of PPL is the set of formulas $\mathcal{F}$ which is defined to
be the smallest set satisfying the two rules:

  1. (r1) $\mathcal{P}\subset\mathcal{F}$.

  2. (r2) If $n\in\mathbb{N}$ and the strings $\alpha$ and $\beta$ are formulas, then the strings $n(\alpha)$, $\neg\alpha$ , and $(\alpha+\beta)$ are also formulas.

For the sake of simplicity and smoothing readability, the following additional
definitions and notations are adopted:

  1. $\bullet$

Every formula which is a propositional variable is called prime formula.

  2. $\bullet$

As in writing arithmetical terms, parenthesis are omitted whenever it is
possible.

  3. $\bullet$

A prime formula or its negation is called a _literal_ and denoted by
$\lambda$.

  4. $\bullet$

A formula of the form $n(\lambda)$, or simply $n\lambda$, is called _pseudo-
literal_.

  5. $\bullet$

A formula which is a pseudo-literal or an addition of two or more pseudo-
literals is said to be in _normal form_.

  6. $\bullet$

A _subformula_ of a formula $\alpha$ is a substring occurring in $\alpha$ that
is itself a formula.

  7. $\bullet$

Formulas will be denoted by $\alpha,\beta,\dots$, and sets of formulas by $F$
and $F^{\prime}$, where these symbols may also be indexed.

Having defined formulas, it is time now to look at their meanings and
semantics. A proposition can only have one of the _truth values_ , true or
false. In PPL, these values are represented by $(1,0)$ for true and $(0,1)$
for false. Each of which can serve as a meaning for a prime formula.
Furthermore, assigning a meaning to some formula $F\in\mathcal{F}$, is done by
the aid of the following three functions:

  * •

Scalar multiplication:
$\mathbb{N}\times\mathbb{Z}^{2}\rightarrow\mathbb{Z}^{2}$ where
$n(z,z^{\prime})=(nz,nz^{\prime})$.

  * •

Negation $\neg^{*}:\mathbb{Z}^{2}\rightarrow\mathbb{Z}^{2}$ where
$\neg^{*}(z,z^{\prime})=(z^{\prime},z)$.

  * •

Addition111This addition is easily distinguished from the addition of
formulas. $+:\mathbb{Z}^{2}\times\mathbb{Z}^{2}\rightarrow\mathbb{Z}^{2}$,
where $+((n,m),(k,l))=(n+k,m+l)$.

Yet, an interpretation $I$ is a subset of $\mathcal{P}$ represented by the
mapping $I:\mathcal{F}\rightarrow\mathbb{Z}^{2}$ which is defined recursively
as follows:

  * 1)

Recursion base. If $\alpha$ is a prime formula then $\alpha=p$ for some
$p\in\mathcal{P}$. The recursion base for this case reads

$I(\alpha)=I(p)=\begin{cases}\,(1,0)&\mbox{ if }p\in I,\\\ \,(0,1)&\mbox{ if
}p\notin I.\\\ \end{cases}.$

  * 2)

Recursion steps.

$I(\alpha)=\begin{cases}n\,(I(\beta))&\text{ if $\alpha$ is of the form
}n\,\beta,\mbox{ where }n\in\mathbb{N},\\\ \neg^{*}(I(\beta))&\mbox{ if
$\alpha$ is of the form }\neg\beta,\\\ I(\beta_{1})+I(\beta_{2})&\mbox{ if
$\alpha$ is of the form }\beta_{1}+\beta_{2}.\\\ \end{cases}$

If two formulas have the same meaning they are called equivalent. More
precisely, it is said that $\alpha$ and $\beta$ are _equivalent_ , in symbols
$\alpha\equiv\beta$, iff for every interpretation $I$ we have
$I(\alpha)=I(\beta)$.

###  2.2. CPPL

Given the set of constraint types $\mathcal{C}=\\{>,\geq,=,<,\leq\\}$, CPPL
utilizes these constraint types additionally to the PPL formulas to build up
its language. The alphabet $\mathcal{A}_{c}$ underlying the language of CPPL
is formed by the unions
$\mathcal{F}\cup\mathcal{C}\cup\left\\{\sim,\left(,\;\right)\right\\}\cup\mathbb{N}$,
where $\sim$, (, and ) resemble the negation and opening and closing
punctuation symbols, respectively.

The set of sentences in CPPL, denoted $\mathcal{S}$, is the smallest set
satisfying the two rules:

  1. (R1) Every triple $(\varphi,\bowtie,n)\in\mathcal{F}\times\mathcal{C}\times\mathbb{N}$ forms a sentence, denoted $\varphi^{(\bowtie,n)}$.

  2. (R2) If the string $\Phi$ is a sentence, then the string $\sim(\Phi)$ is also a sentence.

Sentences are denoted by the Greek letters A, B, $\Gamma$, …, and sets of
sentences are indicated by $S$ and $S^{\prime}$, where these symbols may also
be indexed. Moreover, parenthesis are omitted whenever it is possible. Hence
$\sim(\Phi)$ is simply written as $\sim\Phi$.

It is said that an interpretation $I$ is a model for a sentence
$\Phi=\varphi^{(\bowtie,n)}$, in symbols $I\models\Phi$ or
$I\models\varphi^{(\bowtie,n)}$, iff $I(\varphi)=(m,l)$ with $m\bowtie n$. It
is also said $I$ is a model for $S$ or $I\models S$, iff $I\models\Phi$ for
every sentence $\Phi\in S$.

A direct consequence of this definition is the following proposition.

######  Proposition 2.1.

Let $\varphi^{(\bowtie,\,n)},\psi^{(\bowtie,\,m)}\in\mathcal{S}$. If $I$ is an
interpretation such that $I\models\varphi^{(\bowtie,\,n)}$ and
$I\models\psi^{(\bowtie,\,m)}$, then
$I\models(\varphi+\psi)^{(\bowtie,\,n+m)}$.

To this end, satisfiability and semantic equivalence in CPPL can be considered
analogously to propositional logic.

  * •

It is said that $\Phi$ (resp. $S$) is _satisfiable_ iff there exists an
interpretation $I$ such that $I\models\Phi$ (resp. $I\models$ $S$).

  * •

It is said that $\Phi$ (resp. $S$) is _valid_ or a _tautology_ iff for all
interpretations $I$ we find that $I\models\Phi$ (resp. $I\models S$).

  * •

It is said that $\Phi$ (resp. $S$) is _unsatisfiable_ iff for every
interpretation $I$ we have $I\not\models\Phi$ (resp. $I\not\models$ $S$). If
$\Phi$ is unsatisfiable it will be abbreviated by $\bot$.

  * •

It is said that $S^{\prime}$ is a logical consequence of $S$, denoted $S$
$\models$ $S^{\prime}$, if $I\models$ $S$ $\Rightarrow I\models$ $S^{\prime}$
for all interpretations $I$.

  * •

It is said that $S$ and $S^{\prime}$ are semantically equivalent, denote
$S\equiv S^{\prime}$, if $S$ $\models$ $S^{\prime}$ and $S^{\prime}$ $\models$
$S$

Conventionally, $S\models\Phi$ (resp. $\Phi\models$ $S$) means $S$
$\models\\{\Phi\\}$ (resp. $\\{\Phi\\}\models S$). More generally,
$S\models\Phi_{1},\Phi_{2},\dots,\Phi_{k}$ (resp.
$\Phi_{1},\Phi_{2},\dots,\Phi_{k}\models$ $S$) is written instead of $S$
$\models\\{\Phi_{1},\Phi_{2},\dots,\Phi_{k}\\}$ (resp.
{$\Phi_{1},\Phi_{2},\dots,\Phi_{k}\\}\models S$), and more briefly
$S,\Phi\models\Psi$ is written instead of $S\cup\\{\Phi\\}\models\Psi$.
Analogous notations are used regarding semantic equivalence.

According to these conventions, defining negation in CPPL becomes
straightforward. Let $\Phi,\Psi\in\mathcal{S}$. If for any interpretation $I$
we have $I\models\Phi\iff I\not\models\Psi$ and $I\not\models\Phi\iff
I\models\Psi$, then it is said that $\Psi$ is the negation of $\Phi$ and
abbreviated by $\sim\Phi=\Psi$. Thus, $I\models\Phi\iff
I\not\models\sim\Phi\iff I\models\sim\sim\Phi$. That is
$\Phi\equiv\sim\sim\Phi$.

Under the presented terminology, the following theorems can be proven (see
[3]).

######  Theorem 2.2 (Resolution theorem).

If $\varphi\in\mathcal{F}$ and $n>m^{\prime}\geq m$, then the following
consequence holds:

$(\varphi+m^{\prime}p+m(\neg
p))^{(\bowtie,\,n)}\models(\varphi+(m^{\prime}-m)p)^{(\bowtie,\,n-m)}.$

######  Theorem 2.3.

If $\Phi=\varphi^{(\geq,\,n)}$ is a sentence and $N$ is the coefficient sum of
$\varphi$, then the negation of $\Phi$ can be represented by the sentence
$(\neg\varphi)^{(\geq,\,N-n+1)}$. That is
$\sim\Phi=(\neg\varphi)^{(\geq,\,N-n+1)}$.

Finally, to conclude this section, one more definition is needed. It is said
that the sentence $\varphi^{(\bowtie,\,n)}$ is in standard form or simply
standard, if the formula $\varphi$ is in its normal form and the symbol
“$\bowtie$” corresponds to the constraint type “$\geq$”. $S$ is in standard
form if every sentence $\Phi\in S$ is in its standard form.

Every sentence in CPPL can be transformed equivalently into a standard
sentence [3]. Thus any $\Phi\in\mathcal{S}$, can be represented as follows:

$\Phi=\left(\sum_{i=1}^{i=k}n_{i}\lambda_{i}\right)^{(\geq,\,n)},$

The ultimate goal of CPPL, as in every logic, is to have a system of formal
proof which consists of inference rules for deducing the logical consequence
of sentences from that of another. Restricting inference rules to standard
sentences results in giving fewer cases to be handled, and hence simplifies
the proof system and enhances its implementational efficiency. Thus, the
indicated restriction will be utilized throughout the remaining part of this
paper.

###  2.3. Formal proofs

A proof system consists of a set of inference rules that allow for deducing
sentences from another set of sentences. If $S^{\prime}$ can be deduced from
$S$ by one or several applications of the inference rules, then it is said
that $S^{\prime}$ is derivable from $S$ and denoted by $S\vdash S^{\prime}$.

Each inference rule consists of certain premises that lead to a certain
conclusion and written as $\frac{Premises}{Conclusion}$. Thus the inference
rule $\frac{S\subseteq S^{\prime}}{S^{\prime}\vdash S}$, called the initial
rule, means that $S$ is derivable from $S^{\prime}$ whenever $S\subseteq
S^{\prime}$.

Given a proof system, such as the one listed in Table 1, a formal proof is a
finite sequence of statements of the form $S\vdash S^{\prime}$. Each of these
statements is a result from the previous ones and an application of some
inference rule in the system. If there is a formal proof that ends up with the
statement $S\vdash S^{\prime}$, it is said that $S^{\prime}$ is derivable from
$S$. Additionally, if whenever $S\vdash S^{\prime}$ it turns out that
$S\models S^{\prime}$ then it is said that the proof system is sound. If, on
the other hand, we can prove that $S\models S^{\prime}$ implies $S\vdash
S^{\prime}$, then it is said that the proof system is complete. For example,
the proof system listed in Table 1 is sound and complete [3].

$\text{Conclusion}\text{Premices}$ | Name
---|---
$S^{\prime}\vdash SS\subseteq S^{\prime}$ | Initial Rule
$S_{2}\vdash S\lx@proof@logical@and S_{1}\vdash SS_{1}\subseteq S_{2}$ | Rule of Monotonicity I
$S\vdash S_{2}\lx@proof@logical@and S\vdash S_{1}S_{2}\subseteq S_{1}$ | Rule of Monotonicity II
$S\vdash S_{1}\cup S_{2}\lx@proof@logical@and S\vdash S_{1}S\vdash S_{2}$ | Union Rule
$S\vdash S^{\prime}\lx@proof@logical@and S,\Phi\vdash S^{\prime}S,\sim\Phi\vdash S^{\prime}$ | Negation Rule
$S^{\prime}\vdash SS^{\prime}\vdash\bot$ | Constant Rule
$S\vdash(\varphi+\psi)^{(\geq,\,m+n)}S\vdash\varphi^{(\geq,m)},\psi^{(\geq,\,n)}$ | Addition Rule
$S\vdash(\varphi+(m^{\prime}-m)p)^{(\geq,\,n-m)}\lx@proof@logical@and n>m^{\prime}\geq mS\vdash(\varphi+m^{\prime}p+m(\neg p))^{(\geq,\,n)}$ | Resolution Rule
Table 1.  Rules for derivations.

If we have a proof system that is sound, then any formal proof for $S\vdash
S^{\prime}$ provides an alternative to the mathematical thinking for
determining whether $S^{\prime}$ is a consequence of $S$. Instead of thinking,
we could simply follow a set of rules ending up with the desired assertion.

######  Example.

Considering the proof system listed in Table 1, a formal proof for the
implication $S,\sim\Phi\vdash\bot\implies S\vdash\Phi$ can be represented in a
three-column table, like Table 2.

Line | Statement | Justification
---|---|---
1. | $S,\sim\Phi\vdash\bot$ | Assumption
2. | $S,\sim\Phi\vdash\Phi$ | Constant Rule applied to line 1
3. | $S,\Phi\vdash\Phi$ | Initial Rule
4. | $S\vdash\Phi$ | Negation Rule applied to lines 2 and 3
Table 2. Formal proof for $S,\sim\Phi\vdash\bot$ implies $S\vdash\Phi$.

Although this proof system enables us to prove assertions by applying blindly
a set of rules, it is intended for human use. A proof system is ideal, if it
could completely replace the thought process so that we could program a
computer to perform the needed proofs.

The rest of this paper is devoted to present a proof system with minimal
number of rules called CPPL resolution, analogously to propositional
resolution. It takes the thinking process out of formal proofs allowing for
computerized deductions.

##  3\.  CPPL resolution

CPPL resolution is a system of formal proof with the only two rules listed in
Table 3.

$\text{Conclusion}\text{Premices}$ | Name
---|---
$S^{\prime}\vdash^{r}SS\subseteq S^{\prime}$ | Rule I
$S\vdash^{r}(\varphi_{1}+\varphi_{2})^{(\geq,n_{1}+n_{2}-|\beta|)}S\vdash^{r}(\varphi_{1}+\beta)^{(\geq,n_{1})},\,(\varphi_{2}+\neg\beta)^{(\geq,n_{2})}$ | Rule II
Table 3. Derivation rules of CPPL resolution.

Please note that, the derivation symbol in CPPL resolution proof system is
symbolized by $\vdash^{r}$ to differentiate it from the derivation proof
system listed in Table 1.

Our goal now is to prove that the CPPL resolution is sound and complete. Let
us start with the soundness part, which is rather straightforward.

######  Theorem 3.1 (Soundness).

If $S\vdash^{r}S^{\prime}$, then $S\models S^{\prime}$.

###### Proof.

Assuming $S\vdash^{r}S^{\prime}$ means that there is a formal proof of several
lines, each contains a statement of the form $X\vdash^{r}Y$ justified by one
of the two rules of Table 3, and the final line contains and justifies the
statement $S\vdash^{r}S^{\prime}$. Thus proving this theorem is achieved by
showing that for each line of the formal proof, if $X\vdash^{r}Y$, then
$X\models Y$. But this follows from verifying the two inference rules in Table
3.

Rule I concludes with ${S^{\prime}\vdash^{r}S}$ under the premise $S\subseteq
S^{\prime}$. Thus we need to show that if $S\subseteq S^{\prime}$, then
${S^{\prime}\models S}$. This verification is rather easy. ${I\models
S^{\prime}}$ means ${I\models\Phi^{\prime}}$ for all $\Phi^{\prime}\in
S^{\prime}$. Since $S\subseteq S^{\prime}$, it follows that ${I\models\Phi}$
for all $\Phi\in S$. Thus $S^{\prime}\models S$.

To verify Rule II we need to show that the consequence
$S\models(\varphi_{1}+\beta)^{(\geq,n_{1})},\,(\varphi_{2}+\neg\beta)^{(\geq,n_{2})}$
implies $S\models(\varphi_{1}+\varphi_{2})^{(\geq,n_{1}+n_{2}-|\beta|)}$.
Considering the standard form, we can assume that
$\beta=\sum_{i=1}^{i=k}m_{i}\lambda_{i}$. Accordingly, this means that
$\neg\beta=\sum_{i=1}^{i=k}m_{i}\neg\lambda_{i}$. Now, let $I\models S$. From
the assumption this means that $I\models(\varphi_{1}+\beta)^{(\geq,n_{1})}$
and $I\models(\varphi_{2}+\neg\beta)^{(\geq,n_{2})}$. Taking into account
Proposition 2.1, we conclude that
$I\models(\varphi_{1}+\beta+\varphi_{2}+\neg\beta)^{(\geq,n_{1}+n_{2})}$. That
is
$I\models(\varphi_{1}+\sum_{i=1}^{i=k}m_{i}\lambda_{i}+\varphi_{2}+\sum_{i=1}^{i=k}m_{i}\neg\lambda_{i})^{(\geq,n_{1}+n_{2})}$.
Applying Theorem 2.2 $k$ times results in
$I\models(\varphi_{1}+\varphi_{2})^{(\geq,n_{1}+n_{2}-\sum_{i=1}^{i=k}m_{i})}$.
Hence, $I\models(\varphi_{1}+\varphi_{2})^{(\geq,n_{1}+n_{2}-|\beta|)}$. We
conclude that
$S\models(\varphi_{1}+\varphi_{2})^{(\geq,n_{1}+n_{2}-|\beta|)}$. ∎

The soundness theorem means that $\vdash^{r}\;\subseteq\;\models$. In order to
verify the opposite inclusion, which presents the completeness theorem, some
more notations and results are needed.

######  Lemma 3.2.

For any $S^{\prime}\subseteq S$, if $S\not\models\Phi$ then
$S^{\prime}\not\models\Phi$.

###### Proof.

$S\not\models\Phi$ implies that there is a model $I$ such that $I\models S$
but $I\not\models\Phi$. Since $S^{\prime}\subseteq S$ it follows that
$I\models S^{\prime}$ and $I\not\models\Phi$. That is
$S^{\prime}\not\models\Phi$. ∎

Taking into account the soundness theorem, which also means
$\not\models\subseteq\not\vdash^{r}$, Lemma 3.2 entails the following
corollary.

######  Corollary 3.3.

For any $S^{\prime}\subseteq S$, if $S\not\vdash^{r}\Phi$ then
$S^{\prime}\not\vdash^{r}\Phi$.

######  Definition 3.4.

Let $S$ be a set of sentences. It is said that $S$ is deductively closed if it
contains every sentence that is derivable from it. Formally: if
$S\vdash^{r}S^{\prime}$ then $S^{\prime}\subseteq S$. The deductive closure
of $S$, denoted $D(S)$ is the smallest set that is deductively closed and
contains $S$.

######  Corollary 3.5.

If $S^{\prime}\subseteq S$ then $D(S^{\prime})\subseteq D(S)$.

###### Proof.

Assume that $D(S^{\prime})\not\subseteq D(S)$. That is there exists $\Phi\in
D(S^{\prime})$ such that $\Phi\not\in D(S)$. This implies that
$S\not\vdash^{r}\Phi$. Since $S^{\prime}\subseteq S$ from Corollary 3.3 we
conclude that $S^{\prime}\not\vdash^{r}\Phi$. This means that $\Phi\not\in
D(S^{\prime})$ which results in a contradiction. ∎

######  Corollary 3.6 (Union Rule).

If ${S\vdash^{r}S_{1}}$ and ${S\vdash^{r}S_{2}}$, then ${S\vdash^{r}S_{1}\cup
S_{2}}$.

###### Proof.

${S\vdash^{r}S_{1}}\Rightarrow S_{1}\subseteq D(S)$ and
${S\vdash^{r}S_{2}}\Rightarrow S_{2}\subseteq D(S)$. It follows that
${S_{1}\cup S_{2}\subseteq D(S)}$, which implies the derivation of
$S\vdash^{r}S_{1}\cup S_{2}$. ∎

######  Lemma 3.7 (Constant Rule).

If $S\vdash^{r}\bot$, then $S\vdash^{r}\Phi$.

###### Proof.

Suppose $S\not\vdash^{r}\Phi$. It follows that $S\not\vdash^{r}\Phi,\sim\Phi$
or $S\not\vdash^{r}\bot$ which contradict the assumption of $S\vdash^{r}\bot$.
∎

######  Lemma 3.8 (Contradiction rule).

If $S\vdash^{r}\Phi,\sim\Phi$, then $S\vdash^{r}\bot$.

###### Proof.

Suppose that $\Phi=\varphi^{(\geq,\,n)}$. Thus from theorem 2.3 it follows
that $\sim~{}\Phi=(\neg\varphi)^{(\geq,\,|\varphi|-n+1)}$. Yet, a formal proof
for this example can be represented in a three-column table, namely Table 4.

Line | Statement | Justification
---|---|---
1. | $S\vdash^{r}\varphi^{(\geq,\,n)},(\neg\varphi)^{(\geq,\,|\varphi|-n+1)}$ | Assumption
2. | $S\vdash^{r}(\,)^{(\geq,\,n+|\varphi|-n+1-|\varphi|)}=(\,)^{(\geq,\,1)}=\bot$ | Rule II applied to line 1
Table 4.  Formal proof for the contradiction rule.

∎

######  Definition 3.9.

It is said that $S$ is inconsistent if $S\vdash^{r}\bot$ and otherwise
consistent. $S$ is called maximally consistent if $S$ is consistent but each
$S^{\prime}\supset S$ is inconsistent.

In the context of consistency the following corollary helps in proving
important lemmas.

######  Corollary 3.10.

If $S\models\sim\Phi$, then $S\not\models\Phi$.

###### Proof.

Let $I\models S$. Since $S\models\sim\Phi$ it follows that $I\models\sim\Phi$.
This implies that $I\not\models\Phi$. We conclude that $S\not\models\Phi$. ∎

######  Lemma 3.11.

Let $S$ be a consistent set such that $S\not\vdash^{r}\Phi$ and
$S\not\vdash^{r}\sim\Phi$ then $S\cup\\{\Phi\\}$ is also consistent.

###### Proof.

Assume that $S\cup\\{\Phi\\}$ is inconsistent. This implies the derivation
$S,\Phi\vdash^{r}\bot$. From Lemma 3.7 it follows that
$S,\Phi\vdash^{r}\sim\Phi$. By Theorem 3.1, this implies the consequence
$S,\Phi\models\sim\Phi$. Applying corollary 3.10, we conclude that
$S,\Phi\not\models\Phi$ which is a contradiction. ∎

######  Lemma 3.12.

$S\not\vdash^{r}\Phi$ iff $S,\sim\Phi\not\vdash^{r}\bot$.

###### Proof.

Let

$S\not\vdash^{r}\Phi$ (3.1)

and suppose that

$S,\sim\Phi\vdash^{r}\bot.$ (3.2)

By Lemma 3.7, this implies $S,\sim\Phi\vdash^{r}\Phi$. From Theorem 3.1, it
follows that $S,\sim\Phi\models\Phi$ which implies $S\models\Phi$. By
corollary 3.10, that is $S\not\models\sim\Phi$. From Theorem 3.1 we conclude
that

$S\not\vdash^{r}\sim\Phi.$ (3.3)

Applying Lemma 3.11 to (3.1) and (3.3) gives the consistency of the set
$S\cup\\{\sim\Phi\\}$. That is $S,\sim\Phi\not\vdash^{r}\bot$, which
contradicts the derivation of (3.2).

To prove the opposite direction let

$S,\sim\Phi\not\vdash^{r}\bot$ (3.4)

and assume that $S\vdash^{r}\Phi.$ This means that

$\Phi\in D(S)\subseteq D(S\cup\\{\sim\Phi\\})$ (3.5)

On the other hand, $S,\sim\Phi\vdash^{r}\sim\Phi$. Thus

$\sim\Phi\in D(S\cup\\{\sim\Phi\\})$ (3.6)

From (3.5) and (3.6) we conclude that $S,\sim\Phi\vdash^{r}\Phi,\sim\Phi$ or
$S,\sim\Phi\vdash^{r}\bot$ which contradicts (3.4). ∎

Consequently, $S\not\vdash^{r}\Phi$ is equivalent to the consistency of
$S^{\prime}:=S\cup\\{\sim\Phi\\}$, and $S\not\models\Phi$ is equivalent to the
satisfiability of $S^{\prime}$. Thus, to prove the claim
$\models\;\subseteq\;\vdash^{r}$, which is equivalent to
$S\not\vdash^{r}\Phi\Rightarrow S\not\models\Phi$, we only need to show that
consistent sets of sentences are satisfiable. In order to accomplish this we
need the following lemma, whose proof can be achieved as a consequence of
Zorns’s lemma222 Zorns’s lemma If every chain in a nonempty partially ordered
set $S$ is bounded then $S$ has a maximal element., which is one of the basic
mathematical tools [10].

######  Lemma 3.13.

Every consistent set of sentences $S\subseteq\mathcal{S}$ can be extended to a
maximally consistent set $S^{\prime}\supseteq S$.

######  Lemma 3.14.

A maximally consistent set $S\subseteq\mathcal{S}$ is satisfiable.

###### Proof.

Assume that $S$ is unsatisfiable. It follows that for any interpretation $I$
there exists a sentence $\Phi\in S$ such that $I\not\models\Phi$. Thus
$I\models\sim\Phi$ To this end, we have two cases. Case 1: $\sim\Phi\in S$. It
follows from the initial rule that $S\vdash^{r}\sim\Phi$. Since $\Phi\in S$ it
also follows that $S\vdash^{r}\Phi$. Applying Corollary 3.6 on
$S\vdash^{r}\sim\Phi$ and $S\vdash^{r}\Phi$ results in
$S\vdash^{r}\Phi,\sim\Phi$. By Lemma 3.8 this implies that $S\vdash^{r}\bot$,
which contradict the consistency of $S$. Case 2: $\sim\Phi\not\in S$. This
means that $S\subset S^{\prime}:=S\cup\\{\sim\Phi\\}$. From
$\sim\Phi\not\models\Phi$ it follows that $S^{\prime}\not\models\Phi$. This
implies that $S^{\prime}\not\vdash^{r}\Phi$. By Lemma 3.12 this is equivalent
to the consistency of $S^{\prime}\cup\\{\sim\Phi\\}=S^{\prime}$, which
contradicts the maximality of $S$. ∎

Lemmas 3.13 and 3.14 facilitate our way to obtain the most significant result
of this work, namely the completeness theorem.

######  Theorem 3.15 (Completeness theorem).

For any $S,S^{\prime}\in\mathcal{S}$, if $S\models S^{\prime}$ then
$S\vdash^{r}S^{\prime}$.

###### Proof.

Let us assume that $S\not\vdash^{r}S^{\prime}$. It means that there exists
$\Phi\in S^{\prime}$ such that $S\not\vdash^{r}\Phi$. But this implies the
consistency of $S\cup\\{\sim\Phi\\}$ that can be, according to Lemma 3.13,
extended to a maximally consistent set of sentences, say $S^{\prime\prime}$.
By Lemma 3.14, $S^{\prime\prime}$ is satisfiable, hence $S\cup\\{\sim\Phi\\}$
is also satisfiable. Thus $S\not\models\Phi$. And since $\Phi\in S^{\prime}$
it follows that $S\not\models S^{\prime}$. ∎

##  4\. Conclusion

In this work, the well-known proof system of propositional resolution has been
utilized for CPPL. The resultant CPPL resolution can be viewed as a
generalization of propositional resolution. This is justified by the fact that
every CNF formula, which is a finite set of clauses, can be represented
equivalently by a set of sentences in CPPL [2]. Additionally, CPPL does not
require the corresponding set of sentences to be finite. Although such a
restriction is made dispensable, this work has provided us with a constructive
proof showing that the CPPL resolution is sound and complete. One can
conclude, as a marginal consequence of this result, that propositional
resolution is maintained to be sound and complete even for formulas with
infinite set of clauses.

### Acknowledgment

I would like to thank Prof. Steffen Hölldobler, TU Dresden, Germany. I have
learned from him how to rationalize logically rather than just thinking
mathematically. Without his influence this work would not have been initiated.

## References

  * [1] Aavani, A., Mitchell, D.G., Ternovska, E.: New encoding for translating pseudo-boolean constraints into SAT.  In: Proceedings of the Tenth Symposium on Abstraction, Reformulation, and Approximation, SARA 2013, 11-12 July 2013, Leavenworth, Washington, USA. (2013).  URL http://www.aaai.org/ocs/index.php/SARA/SARA13/paper/view/7212
  * [2] Azizi-Sultan, A.: Pseudo-propositional logic.  In: Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2018), Oxford, UK, July 18, 2018., pp. 26–33 (2018).  URL http://ceur-ws.org/Vol-2095/paper1.pdf
  * [3] Azizi-Sultan, A.: Constrained pseudo-propositional logic.  Logica Universalis 14(4), 523–535 (2020).  10.1007/s11787-020-00266-x.  URL https://doi.org/10.1007/s11787-020-00266-x
  * [4] Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of pseudo-boolean constraints into CNF.  In: Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009\. Proceedings, pp. 181–194 (2009).  10.1007/978-3-642-02777-2_19.  URL https://doi.org/10.1007/978-3-642-02777-2_19
  * [5] Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using sat procedures instead of bdds.  In: Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, DAC ’99, pp. 317–320. ACM, New York, NY, USA (1999).  10.1145/309847.309942.  URL http://doi.acm.org/10.1145/309847.309942
  * [6] Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds.  In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS ’99, pp. 193–207. Springer-Verlag, London, UK, UK (1999).  URL http://dl.acm.org/citation.cfm?id=646483.691738
  * [7] Cook, S.A.: The complexity of theorem-proving procedures.  In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pp. 151–158 (1971).  10.1145/800157.805047.  URL http://doi.acm.org/10.1145/800157.805047
  * [8] Gomes, C.P., Selman, B., McAloon, K., Tretkoff, C.: Randomization in backtrack search: Exploiting heavy-tailed profiles for solving hard scheduling problems.  In: Proceedings of the Fourth International Conference on Artificial Intelligence Planning Systems, Pittsburgh, Pennsylvania, USA, 1998, pp. 208–213 (1998).  URL http://www.aaai.org/Library/AIPS/1998/aips98-025.php
  * [9] Kautz, H., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search.  In: Proceedings of the Thirteenth National Conference on Artificial Intelligence - Volume 2, AAAI’96, pp. 1194–1201. AAAI Press (1996).  URL http://dl.acm.org/citation.cfm?id=1864519.1864564
  * [10] Lang, S.: Real and Functional Analysis, 3rd ed.  Springer-Verlag, New York (1993)
  * [11] Russell, S.J., Norvig, P.: Artificial intelligence - a modern approach, 2nd Edition.  Prentice Hall series in artificial intelligence. Prentice Hall (2003).  URL http://www.worldcat.org/oclc/314283679
  * [12] Velev, M.N., Bryant, R.E.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors.  Journal of Symbolic Computation 35(2), 73 – 106 (2003).  https://doi.org/10.1016/S0747-7171(02)00091-3.  URL http://www.sciencedirect.com/science/article/pii/S0747717102000913