Gheorghiu, Alexander V. Pym, David J.

# Defining Logical Systems via Algebraic Constraints on Proofs

Alexander V. Gheorghiu  University College London,
London WC1E 6BT, UK<EMAIL_ADDRESS>David J. Pym  University
College London,
London WC1E 6BT, UK  Institute of philosophy, University of London,
London WC1H 0AR, UK<EMAIL_ADDRESS>
###### Abstract

We present a comprehensive programme analysing the decomposition of proof
systems for non-classical logics into proof systems for other logics,
especially classical logic, using an algebra of constraints. That is, one
recovers a proof system for a target logic by enriching a proof system for
another, typically simpler, logic with an algebra of constraints that act as
correctness conditions on the latter to capture the former; for example, one
may use Boolean algebra to give constraints in a sequent calculus for
classical propositional logic to produce a sequent calculus for intuitionistic
propositional logic. The idea behind such forms of reduction is to obtain a
tool for uniform and modular treatment of proof theory and provide a bridge
between semantics logics and their proof theory. The article discusses the
theoretical background of the project and provides several illustrations of
its work in the field of intuitionistic and modal logics. The results include
the following: a uniform treatment of modular and cut-free proof systems for a
large class of propositional logics; a general criterion for a novel approach
to soundness and completeness of a logic with respect to a model-theoretic
semantics; and, a case study deriving a model-theoretic semantics from a
proof-theoretic specification of a logic.

###### keywords:

Logic, Proof Theory, Model Theory, Semantics, Modal Logic, Intuitionistic
Logic

##  1 Introduction

The general goal of this paper is to provide a unifying meta-level framework
for studying logics. To this end, we introduce a framework in which one can
represent the _reasoning_ in a logic, as captured by a concept of proof for
that logic, in terms of the reasoning within another logic through an algebra
of constraints — as a slogan,

Proof in $\mathsf{L}$ = Proof in $\mathsf{L}$′ \+ Algebra of Constraints
$\mathcal{A}$

We shall refer back to this slogan often and will use the following
abbreviated form:

$\mathsf{L}=\mathsf{L^{\prime}}\oplus\mathcal{A}$

The $\oplus$ is not formal— that is, $\mathsf{L^{\prime}}\oplus\mathcal{A}$
may denote any one of several ways of applying constraints $\mathcal{A}$ to
$\mathsf{L}^{\prime}$.

Such decompositions of $\mathsf{L}$ into $\mathsf{L}^{\prime}$ and
$\mathcal{A}$ allow us to study the metatheory of the former by analyzing the
latter. This is advantageous when the latter is typically simpler in some
desirable way — for example, it may relax the side conditions on the use of
specific rules — which facilitates the study of the original logic of
interest. There are already some examples of such relationships within the
literature — they are discussed below. The framework herein provides a general
view of the phenomena and provides an umbrella for these seemingly disparate
cases. Importantly, there is no guarantee that the constraints will be
solvable algorithmically as it depends on how complex the algebra is, but even
relatively simple algebras can have a dramatic impact; for example, we
illustrate how constraint systems using Boolean algebra, which admits solvers,
are helpful for the study of proof-search and meta-theory in substructural and
intuitionistic logics.

The decompositions expressed by the slogan above may be iterated in valuable
ways; that is, it is possible to decompose $\mathsf{L}^{\prime}$ in the slogan
above. Each time we do such a decomposition, the combinatorics of the proof
system become more tractable as more and more is delegated to the algebra.
Eventually, the combinatorics becomes as simple as possible, and one recovers
something with all the flexibility of the proof theory for classical logic.
Thus, we advance the view that, in general, classical logic forms a
combinatorial core of syntactic reasoning since its proof theory is
comparatively relaxed — that is, possibly after iterating decompositions of
the kind above, one eventually witnesses the following:

Proof in $\mathsf{L}$ = Classical Proof + Algebra of Constraints $\mathcal{A}$

The view of classical logic as the core of logic has, of course, been advanced
before — see, for example, Gabbay [Gabbay1993].

Using techniques from universal algebra, we define the algebraic constraints
by a theory of first-order classical logic; for example, we may define Boolean
algebra by its axiomatization — see Section 2. We then enrich rules of a
system $\mathsf{L}$ with expressions from $\mathcal{A}$ to express rules of
another system $\mathsf{L}^{\prime}$ — for example, by using Boolean algebra
for the constraints, we may express the single-conclusioned
$\mathsf{\lor_{R}}$-rule from Gentzen’s $\mathsf{LJ}$ [Gentzen1969] with the
combinatorics of the multiple-conclusioned $\mathsf{\lor_{R}}$-rule from
Gentzen’s $\mathsf{LK}$ [Gentzen1969],

$\Gamma\vdash_{\mathsf{}}\phi\lor\psi\Gamma\vdash_{\mathsf{}}\phi\cdot
x,\psi\cdot\bar{x}$

— one recovers the single-conclusion condition by assigning the variable $x$
to $0$ or $1$ in the Boolean algebra and evaluating the formula accordingly:
one keeps formulae that carry a $1$ and deletes formulae which carry $0$. A
system of rules enriched in this way is called a _constraint system_. Detailed
examples are below.

We consider two kinds of relationships the constraint systems may have with
the logic of interest. A constraint system is _sound and complete_ when the
evaluation of construction from the constraints system concludes a sequent iff
that sequent is valid in the logic. A stronger relationship is _faithfulness
and adequacy_ :

  * -

(_Faithful_) The evaluation of a construction from the constraint system is a
proof in the logical system of interest.

  * -

(_Adequate_) Every proof in the logical system of interest is the evaluation
of some construction from the constraint system.

Both relationships are important, as illustrated by the examples below.

The point of constraint systems is that they allow us to study the metatheory
of the logic of interest. There are two principal such activities presented in
this paper: first, one may use constraint systems to study questions of proof-
search (i.e., how one constructs proofs) in the logic of interest; second,
they may be used to bridge the gap between the proof theory and model theory
of a logic. On the latter use, constraint systems allow a novel approach to
soundness and completeness proofs which bypasses truth-in-a-model and term-
model constructors; furthermore, they give a principled way of generating a
correct-by-design model-theoretic semantics for the logic of interest by
analyzing a proof system for it, making essential use of algebraic constraints
and the aforementioned decomposition to classical logic.

Of course, the idea that one may use labels to internalize the semantics of
logics within proof systems has taken several forms and goes back as far as
Kanger [kanger1957provability]. It underpins a systematic development of
analytic tableaux (see, for example, Fitting [Fitting1983, Fitting1998],
Catach [catach1991tableaux], Massacci [massacci1994strongly], Baldoni
[baldoni1998normal], Docherty and Pym [Docherty2018, docherty2019non,
Docherty2019], and Galmiche and Méry [galmiche2002resource,
galmiche2003semantic, Galmiche2005, galmiche2010tableaux]), natural deduction
systems (see, for example, Simpson [simpson1994proof], and Basin et al.
[basin1998natural]), sequent calculi (see, for example, Mints [mints1968cut,
mints1997indexed], Viganò [vigano2013labelled], Kushida and Okada
[kushida2003proof]). Particularly significant within this stream are the
relational calculi studied by Negri [negri1998cut, negri2003contraction,
Negri2005].

The notion of constraint system presented in this paper is closely related to
Gabbay’s _Labelled Deductive Systems_ (LDSs) [Gabbay1996] — see also Russo
[Russo1996]. However, the paper deviates from the established theory of LDSs
in two fundamental ways: First, one may choose any syntactic structure in the
grammar of the object-logic (e.g., data composed of formulae, such as sets,
multisets, bunches), not just formulae, to annotate; second, the labels do not
only express additional information but have an action on the structure. Note,
there are other proof systems in the literature in which one labels data
composed of formulae — see, for example, Marx et al. [marx2000mosaic].
Consequently, more subtle examples are available, not otherwise captured by
LDSs.

In summary, two main ideas are developed in this paper: a meta-logic for
studying object-logics and algebraic constraints for studying the metatheory
of a logic. Both ideas are present elsewhere in the literature and have been
studied for different logics but have yet to be formalized and uniformed. This
paper aims to provide a general and uniform framework for analyzing and
understanding the proof theory of logics represented in this way.

The paper begins in Section 2 with an example of a constraint system already
in the literature. It continues in Section 3 with the background and notation
required for the general treatment throughout the rest of the paper.
Constraint systems are defined in general in Section 4, where the correctness
properties of soundness, completeness, faithfulness, and adequacy are also
discussed. In Section 5, we study relational calculi as a general class of
constraint systems and study an approach to proving soundness and completeness
which works with validity directly. We give a concrete illustration of the
approach applied to intuitionistic propositional logic (IPL) in Section 6 —
specifically, by using constraint systems, we derive the model-theoretic
semantics given by Kripke [Kripke1963] from $\mathsf{LJ}$, which is sound and
complete by construction. In Section 7, we consider the treatment of first-
order logics with constraints, the rest of the paper being restricted to
propositional logics. The paper concludes in Section 8 with a summary and a
discussion of future research.

##  2 Example: Resource-distribution via Boolean Constraints

In this section, we summarize the resource-distribution via Boolean
constraints (RDvBC) mechanism, which was introduced by Harland and Pym
[Harland1997, Pym2001dis] as a tool for reasoning about the context-management
problem during proof-search in logics with multiplicative connectives, such as
Linear Logic (LL) and the logic of Bunched Implications (BI). It is the
original example of a decomposition of a proof system in the sense of this
paper, as explained at the end of the section. We present RDvBC to motivate
the abstract technical work in Section 4 for the general approach. We
concentrate on the case of BI to indicate the scope of the approach and the
challenges involved in setting it up because the logic operates over quite a
subtle data structure — bunches.

###  2.1 The Logic of Bunched Implications

One may regard BI as the free combination (i.e., the fibration — see Gabbay
[Gabbay1993]) of intuitionistic propositional logic (IPL), with connectives
$\land,\lor,\to,\top,\bot$, and intuitionistic multiplicative linear logic
(IMLL), with connectives $*,-\mkern-6.0mu*,\top^{*}$. Let $\mathbb{A}$ be a
set of atomic propositions. The following grammar generates the formulae of
BI:

$\phi::=\and{p}\in\mathbb{A}\mid\top\mid\bot\mid\top^{*}\mid\phi\land\psi\mid\phi\lor\psi\mid\phi\to\phi\mid\phi*\phi\mid\phi-\mkern-6.0mu*\phi$

The set of all formulae is $\mathbb{FORM}$.

A distinguishing feature of BI is that it has two primitive implications,
$\to$ and $-\mkern-6.0mu*$, each corresponding to a different context-former,
$\fatsemi$ and , representing the two conjunctions $\land$ and $*$,
respectively. As these context-formers do not commute with each other, though
individually they behave as usual, contexts in BI are not one of the familiar
structures of lists, multisets, or sets. Instead, its contexts are _bunches_ —
a term that derives from the relevance logic literature (see, for example,
Read [Read1988]). The set of bunches $\mathbb{BUNCH}$ is defined by the
following grammar:

$\Gamma::=\phi\in\mathbb{FORM}\mid\varnothing_{+}\mid\varnothing_{\times}\mid\Gamma\fatsemi\Gamma\mid\Gamma\fatcomma\Gamma$

A bunch $\Delta$ is a sub-bunch of a bunch $\Gamma$ iff $\Delta$ is a sub-tree
of $\Gamma$. One may write $\Gamma(\Delta)$ to mean that $\Delta$ is a sub-
bunch of $\Gamma$. The operation $\Gamma[\Delta\mapsto\Delta^{\prime}]$ —
abbreviated to $\Gamma(\Delta^{\prime})$ where no confusion arises — is the
result of replacing the occurrence of $\Delta$ by $\Delta^{\prime}$.

Bunches have similar structural behaviour to the more familiar data-structures
used for contexts in logic (e.g., lists, multisets, sets, etc.). We define
this behaviour explicitly by means of an equivalence relation called _coherent
equivalence_. Two bunches $\Gamma,\Gamma^{\prime}\in\mathbb{BUNCH}$ are
coherently equivalent when $\Gamma\equiv\Gamma^{\prime}$, where $\equiv$ is
the smallest relation satisfying:

  * -

commutative monoid equations for $\fatsemi$ with unit $\varnothing_{+}$

  * -

commutative monoid equations for with unit $\varnothing_{\times}$

  * -

coherence; that is, if $\Delta\equiv\Delta^{\prime}$, then
$\Gamma(\Delta)\equiv\Gamma(\Delta^{\prime})$.

A sequent in BI is a pair $\Gamma\triangleright\phi$ in which $\Gamma$ is a
bunch, and $\phi$ is a formula. We use $\triangleright$ as a pairing symbol
defining sequents to distinguish it from the judgment $\vdash_{\mathsf{}}$
that asserts that a sequent is a consequence of BI. We may characterize the
consequence judgment $\vdash_{\mathsf{}}$ for BI by provability in the sequent
calculus $\mathsf{LBI}$ in Figure 1 (see Pym [Pym2003]). That is,
$\Gamma\vdash_{\mathsf{}}\phi$ iff there is an $\mathsf{LBI}$-proof of
$\Gamma\triangleright\phi$.

$\phi\triangleright\phi\qquad\Gamma(\bot)\triangleright\phi\qquad\varnothing_{\times}\triangleright\top^{*}\qquad\varnothing_{+}\triangleright\top$
$\Gamma(\Delta\fatcomma\Delta^{\prime}\fatcomma\phi-\mkern-6.0mu*\psi)\triangleright\chi\lx@proof@logical@and\Delta^{\prime}\triangleright\phi\Gamma(\Delta\fatcomma\psi)\triangleright\chi\qquad\Delta\triangleright\phi-\mkern-6.0mu*\psi\Delta\fatcomma\phi\triangleright\psi$
$\Delta(\phi*\psi)\triangleright\chi\Delta(\phi\fatcomma\psi)\triangleright\chi\qquad\Delta\fatcomma\Delta^{\prime}\triangleright\phi*\psi\lx@proof@logical@and\Delta\triangleright\phi\Delta^{\prime}\triangleright\psi\qquad\Delta(\top^{*})\triangleright\chi\Delta(\varnothing_{\times})\triangleright\chi$
$\Delta(\phi\land\psi)\triangleright\chi\Delta(\phi\fatsemi\psi)\triangleright\chi\qquad\Delta\triangleright\phi\land\psi\lx@proof@logical@and\Delta\triangleright\phi\Delta\triangleright\psi\qquad\Delta(\top)\triangleright\chi\Delta(\varnothing_{+})\triangleright\chi$
$\Delta(\phi\lor\psi)\triangleright\chi\lx@proof@logical@and\Delta(\phi)\triangleright\chi\Delta(\psi)\triangleright\chi\qquad\Delta\triangleright\phi\lor\psi\Delta\triangleright\phi\qquad\Delta\triangleright\phi\lor\psi\Delta\triangleright\psi$
$\Gamma(\Delta\fatsemi\phi\to\psi)\triangleright\chi\lx@proof@logical@and\Delta\triangleright\phi\Gamma(\Delta\fatsemi\psi)\triangleright\chi\qquad\Delta\triangleright\phi\to\psi\Delta\fatsemi\phi\triangleright\psi$
$\Delta(\Delta^{\prime}\fatsemi\Delta^{\prime\prime})\triangleright\chi\Delta(\Delta^{\prime})\triangleright\chi\qquad\Delta^{\prime}\triangleright\chi\Delta\triangleright\chi\qquad\Delta(\Delta^{\prime})\triangleright\chi\Delta(\Delta^{\prime}\fatsemi\Delta^{\prime})\triangleright\chi$

Figure 1: Sequent Calculus $\mathsf{LBI}$

As bunches are intended to be the syntactic trees of $\mathbb{BUNCH}$ modulo
$\equiv$, we may somewhat relax the formal reading of the rules of
$\mathsf{LBI}$. The effect of coherent equivalence is, essentially, to render
bunches into two-sorted nested multisets — see Gheorghiu and Marin [Alex2021].
Therefore, we may suppress brackets for sections of the bunch with the same
context-former and apply rules sensitive to context-formers (e.g.,
$\mathsf{\ast_{R}}$) accordingly. For example, any context-former may be used
in $\mathsf{\ast_{R}}$ applied to
$\and{p}_{1}\fatcomma\and{p}_{1}\fatcomma\and{p}_{3}\triangleright\and{q}_{1}\ast\and{q}_{2}$;
the possibilities are as follows:

$\and{p}_{1}\fatcomma\and{p}_{2}\fatcomma\and{p}_{3}\triangleright\and{q}_{1}\ast\and{q}_{2}\lx@proof@logical@and\and{p}_{1}\triangleright\and{q}_{1}\and{p}_{2}\fatcomma\and{p}_{3}\triangleright\and{q}_{2}\qquad\and{p}_{1}\fatcomma\and{p}_{2}\fatcomma\and{p}_{3}\triangleright\and{q}_{1}\ast\and{q}_{2}\lx@proof@logical@and\and{p}_{1}\fatcomma\and{p}_{2}\triangleright\and{q}_{1}\and{p}_{3}\triangleright\and{q}_{2}$

This concludes the introduction of BI. In the next section, we apply the RDvBC
mechanism to analyze proof-search in $\mathsf{LBI}$.

###  2.2 Resource-distribution via Boolean Constraints

Proof-search in $\mathsf{LBI}$ is complex because the presence of
multiplicative connectives (i.e., $\ast$ and $-\mkern-6.0mu*$) requires
deciding how to distribute the formulae (or, rather, sub-bunches) when making
reductions.

######  Example 2.1.

The following proof-search attempts differ only in the choice of distribution,
but one successfully produces a proof, and the other fails:

$\underbrace{\and{p}\fatcomma\and{q}\fatcomma\and{r}\triangleright\and{p}\ast(\and{q}\ast\and{r})\lx@proof@logical@and\and{p}\triangleright\and{p}\and{q}\fatcomma\and{r}\triangleright\and{q}\ast\and{r}\lx@proof@logical@and\and{q}\triangleright\and{q}\and{r}\triangleright\and{r}}_{\mbox{succeeds}}\qquad\underbrace{\and{p}\fatcomma\and{q}\fatcomma\and{r}\triangleright\and{p}\ast(\and{q}\ast\and{r})\lx@proof@logical@and\and{p}\fatcomma\and{q}\triangleright\and{p}?\and{r}\triangleright\and{q}\ast\and{r}?}_{\text{fails}}$

How can we analyze the various distribution strategies? This is the question
RDvBC addresses. $\Diamond$

There is substantial literature on intricate rules of inference in
multiplicative logics that are used to keep track of the relevant information
to enable proof-search. However, they are generally tailored for one
particular distribution method — see, for example, Hodas and Miller
[hodas1994logic, Hodas1994thesis], Winikoff and Harland
[winikoff1995implementing], Cervasto [Cervesato2000], and Lopez [Lopez2005].
It is in this context that Harland and Pym [Harland1997, Pym2001dis]
introduced the RDvBC mechanism. The idea is that rather than commit to a
particular strategy for managing the distribution, one uses Boolean
expressions to express that a resource distribution needs to be made and the
conditions it needs to satisfy.

Before presenting the technical details of RDvBC, we give a heuristic account.
Essentially, one assigns a Boolean expression to each formula requiring
distribution. Constraints on the possible values of this expression are then
generated during the proof-search and propagated up the search tree, resulting
in a set of Boolean equations. A successful proof-search in the enriched
system will generate a soluble set of equations corresponding to a
distribution of formulae across the branches of the structure, and
instantiating that distribution results in an actual proof. It remains to give
the formal detail. We begin by defining the constraint algebra that delivers
RDvBC.

A _Boolean algebra_ is a tuple
$\mathcal{B}:=\langle\mathbb{B},\\{+,\times,\bar{\cdot}\\},\\{0,1\\}\rangle$
in which $\mathbb{B}$ is a set, $+:\mathbb{B}^{2}\to\mathbb{B}$,
$\times:\mathbb{B}^{2}\to\mathbb{B}$, $\bar{\cdot}:\mathbb{B}\to\mathbb{B}$ be
operators on $\mathbb{B}$, and $0,1\in\mathbb{B}$, satisfying the following
conditions for any $a,b,c\in\mathbb{B}$:

$\begin{array}[]{cc}a+(b+c)=(a+b)+c\quad a\times(b\times c)=(a\times b)\times
c&a+b=b+c\quad a\times b=b\times a\\\ a+(a\times b)=a\quad
a\times(a+b)=a&a+0=a\quad a\times 1=a\\\ a+(b\times
c)=(a+b)\times(a+c)&a\times(b+c)=(a\times b)+(a\times c)\\\
a+\bar{a}=1&a\times\bar{a}=0\end{array}$

A _presentation_ of the Boolean algebra is a first-order classical logic with
equality for which the Boolean algebra is a model. We use the following, in
which $X$ is a set of _variables_ , $e$ are _Boolean expressions_ , and $\phi$
are _Boolean formulae_ :

$e::=x\in X\mid e+e\mid e\times e\mid\bar{e}\mid 0\mid
1\quad\phi::=(e=e)\mid\phi\with\phi\mid\phi\parr\phi\mid\neg\phi\mid\forall
x\phi\mid\exists x\phi$

The symbols $\with$ and $\parr$ are used as classical conjunction and
disjunction, respectively.

We are overloading $+$ and $\times$ to be both function-symbols in the term
language and their corresponding operators in the Boolean algebra; similarly,
we are overloading $0$ and $1$ to be both constants in the term language and
the bottom and top element of the Boolean algebra. This is to economize on
notation. We may suppress the $\times$ when no confusion arises — that is,
$t_{1}\times t_{2}$ may be expressed $t_{1}t_{2}$. For a list of Boolean
expressions $V=[e_{1},\hdots e_{n}]$, let
$\bar{V}:=[\bar{e}_{1},\hdots\bar{e}_{n}]$; we may write $V=e$ to denote that
$V$ is a list containing only $e$.

Let some presentation of Boolean algebra be fixed. An _annotated BI-formula_
is a BI-formula $\phi$ with a Boolean expression $e$, denoted $\phi\cdot e$.
The annotation of a bunch $\Gamma$ by a list of Boolean expressions $V$ is
defined as follows:

  * -

if $\Gamma=\gamma$, where
$\gamma\in\mathbb{FORM}\cup\\{\varnothing_{+},\varnothing_{\times}\\}$ and
$V=[e]$, then $\Gamma\cdot V:=\gamma\cdot e$;

  * -

if $\Gamma=(\Delta_{1}\fatsemi\Delta_{2})$, and $V=[e]$, then $\Gamma\cdot
V:=(\Delta_{1}\fatsemi\Delta_{2})\cdot e$;

  * -

if $\Gamma=(\Delta_{1}\fatcomma\Delta_{2})$, and $V$ is the concatenation of
$V_{1}$ and $V_{2}$, then $\Gamma\cdot V:=(\Delta_{1}\cdot
V_{1}\fatsemi\Delta_{2}\cdot V_{2})$.

For example, $p\fatcomma(q\fatsemi r)\cdot[x,y]:=p\cdot x\fatcomma(q\fatsemi
r)\cdot y$. Notably, the annotation only acts on the top-level of
multiplicative connectives and treats everything below (e.g., additive sub-
bunches) as formulae. This makes sense as all of the distributions in
$\mathsf{LBI}$ take place at this level of the bunch.

This concludes the technical overhead required to define the RDvBC mechanism
for BI. Roughly, Boolean constraints are used to mark the multiplicative
distribution of formulae. The mechanism is captured by proof-search in the
sequent calculus $\mathsf{LBI}_{\mathcal{B}}$ comprised of the rules in Figure
2, in which $V$ is a list of Boolean variables that do not appear in any
sequents present in the tree and labels that do not change are suppressed. The
same names are used for rules in $\mathsf{LBI}_{\mathcal{B}}$ and
$\mathsf{LBI}$ to economize on notation.

$\phi\cdot y\fatcomma\Delta\cdot V\triangleright\phi\cdot 1y=1\land
V=0\qquad\bot\cdot y\fatcomma\Delta\cdot V\triangleright\phi y=1\land V=0$
$\varnothing_{\times}\cdot y\fatcomma\Delta\cdot
V\triangleright\top^{*}y=1\with V=0\qquad\varnothing_{+}\cdot
y\fatcomma\Delta\cdot V\triangleright\top y=1\with V=0$
$\Gamma(\Delta\fatcomma\phi-\mkern-6.0mu*\psi\cdot
e)\triangleright\chi\lx@proof@logical@and\Delta\cdot V\triangleright\phi\cdot
e\Gamma(\Delta\cdot\bar{V}\fatcomma\psi\cdot e)\triangleright\chi
e=1\qquad\Delta\triangleright(\phi-\mkern-6.0mu*\psi)\cdot
e\lx@proof@logical@and\Delta\fatcomma\phi\cdot e\triangleright\psi\cdot ee=1$
$\Delta((\phi*\psi)\cdot
e)\triangleright\chi\lx@proof@logical@and\Delta(\phi\cdot e\fatcomma\psi\cdot
e)\triangleright\chi
e=1\qquad\Delta\fatcomma\Delta^{\prime}\triangleright\phi*\psi\lx@proof@logical@and\Delta\cdot
V\triangleright\phi\Delta^{\prime}\cdot\bar{V}\triangleright\psi\qquad\Delta(\top^{*}\cdot
e)\triangleright\chi\lx@proof@logical@and\Delta(\varnothing_{\times}\cdot
e)\triangleright\chi e=1$
$\Delta((\phi\land\psi)\cdot
e)\triangleright\chi\lx@proof@logical@and\Delta(\phi\cdot e\fatsemi\psi\cdot
e)\triangleright\chi
e=1\qquad\Delta\triangleright\phi\land\psi\lx@proof@logical@and\Delta\triangleright\phi\Delta\triangleright\psi\qquad\Delta(\top\cdot
e)\triangleright\chi\lx@proof@logical@and\Delta(\varnothing_{+}\cdot
e)\triangleright\chi e=1$
$\Delta((\phi\lor\psi)\cdot
e)\triangleright\chi\lx@proof@logical@and\Delta(\phi\cdot
e)\triangleright\chi\Delta(\psi\cdot e)\triangleright\chi
e=1\qquad\Delta\triangleright\phi\lor\psi\Delta\triangleright\phi\qquad\Delta\triangleright\phi\lor\psi\Delta\triangleright\psi$
$\Gamma(\Delta\fatsemi(\phi\to\psi)\cdot
e)\triangleright\chi\lx@proof@logical@and\Delta\triangleright\phi\Gamma(\Delta\fatsemi\psi\cdot
e)\triangleright\chi
e=1\qquad\Delta\triangleright\phi\to\psi\lx@proof@logical@and\Delta\fatsemi\phi\cdot
e\triangleright\psi e=1$
$\Gamma(\Delta\cdot e\fatsemi\Delta\cdot
e)\triangleright\chi\lx@proof@logical@and\Gamma(\Delta\cdot
e)\triangleright\chi
e=1\qquad\Delta^{\prime}\triangleright\chi\Delta\triangleright\chi\qquad\Gamma(\Delta\cdot
e)\triangleright\chi\lx@proof@logical@and\Gamma(\Delta\cdot
e\fatsemi\Delta\cdot e)\triangleright\chi e=1$

Figure 2: Sequent Calculus $\mathsf{LBI}_{\mathcal{B}}$

An $\mathsf{LBI}_{\mathcal{B}}$-reduction is a tree constructed by applying
the rules of $\mathsf{LBI}_{\mathcal{B}}$ reductively, beginning with a
sequent in which each formula is annotated by $1$.

######  Example 2.2.

The following is an $\mathsf{LBI}_{\mathcal{B}}$-reduction $\mathcal{D}$:

$(\and{p}\cdot 1)\fatcomma(\and{q}\cdot 1)\fatcomma(\and{r}\cdot
1)\triangleright\and{p}\ast(\and{q}\ast\and{r})\cdot
1\lx@proof@logical@and(\and{p}\cdot x_{1})\fatcomma(\and{q}\cdot
x_{2})\fatcomma(\and{r}\cdot x_{3})\triangleright\and{p}\cdot
1(x_{1}=1)\land(x_{2}=0)\land(x_{3}=0)\mathcal{D}^{\prime}$

— the sub-tree $\mathcal{D}^{\prime}$ is the following:

$(\and{p}\cdot\bar{x}_{1})\fatcomma(\and{q}\cdot\bar{x}_{2})\fatcomma(\and{r}\cdot\bar{x}_{3})\triangleright\and{q}\ast\and{r}\cdot
1\lx@proof@logical@and(\and{p}\cdot\bar{x}_{1}y_{1})\fatcomma(\and{q}\cdot\bar{x}_{2}y_{2})\fatcomma(\and{r}\cdot\bar{x}_{3}y_{3})\triangleright\and{q}(\bar{x}_{1}y_{1}=0)\land(\bar{x}_{2}y_{2}=1)\land(\bar{x}_{3}y_{3}=0)\and{p}\cdot(\bar{x}_{1}\bar{y}_{1})\fatcomma\and{q}\cdot(\bar{x}_{2}\bar{y}_{2})\fatcomma\and{r}\cdot(\bar{x}_{3}\bar{y}_{3})\triangleright\and{r}(\bar{x}_{1}\bar{y}_{1}=0)\land(\bar{x}_{2}\bar{y}_{2}=0)\land(\bar{x}_{3}\bar{y}_{3}=1)$

$\Diamond$

Having produced an $\mathsf{LBI}_{\mathcal{B}}$-reduction, if the constraints
are consistent, they determine the variables’ interpretations to satisfy the
constraints. Such interpretations $I$ induce a valuation $\nu_{I}$ that acts
on formulae by keeping formulae whose label evaluates to $1$ and deleting
(i.e., producing the empty-string $\varepsilon$) for formulae whose label
evaluates to $0$; that is, let $\phi$ be a BI-formula and $e$ a Boolean
expression,

$\nu_{I}(\phi\cdot e):=\cases{\phi}&\text{if}I(e)=1\\\
\varepsilon\text{if}I(e)=0$

A valuation extends to sequents by acting on each formulae occurring in it,
and it extends to $\mathsf{LBI}_{\mathcal{B}}$-reductions by acting on each
sequent occurring in it and removing the constraints.

######  Example 2.3 (Example 2.2 cont’d).

The constraints on $\mathcal{D}$ are satisfied by any interpretation $I(z)=1$
for $z\in\\{x_{1},y_{2}\\}$ and $I(z)=0$ for
$z\in\\{x_{2},x_{3},y_{1},y_{3}\\}$. For any such $I$, the tree $\nu_{I}(D)$
is as follows:

$\and{p}\fatcomma\and{q}\fatcomma\and{r}\triangleright\and{p}\ast(\and{q}\ast\and{r})\lx@proof@logical@and\and{p}\triangleright\and{p}\and{q}\fatcomma\and{r}\triangleright\and{q}\ast\and{r}\lx@proof@logical@and\and{q}\triangleright\and{q}\and{r}\triangleright\and{r}$

This is the successful derivation in $\mathsf{LBI}$ in Example 2.1. According
to the constraints, a distribution strategy results in a successful proof-
search just in case it sends only the first formula to the left branch.
$\Diamond$

Harland and Pym [Harland1997, Pym2001dis] proved that
$\mathsf{LBI}_{\mathcal{B}}$ is _faithful_ and _adequate_ for $\mathsf{LBI}$
in the following sense:

  * -

_Faithfulness_. If $\mathcal{R}$ is an $\mathsf{LBI}_{\mathcal{B}}$-reduction
and $I$ is an interpretation satisfying those constraints, then there is a
$\mathsf{LBI}$-proof $\mathcal{D}$ such that
$\nu_{I}(\mathcal{R})=\mathcal{D}$.

  * -

_Adequacy_. If $\mathcal{D}$ is an $\mathsf{LBI}$-proof, then there is a
$\mathsf{LBI}_{\mathcal{B}}$-reduction $\mathcal{R}$ and an interpretation $I$
satisfying its constraints such that $\nu_{I}(R)=\mathcal{D}$.

Recall that we may think of BI as the combination of IPL and IMLL. We may
express $\mathsf{LBI}$ as the combination of sequent calculi for these two
logics (i.e., $\mathsf{IMLL}$ and $\mathsf{LJ}$, respectively) — that is,

$\mathsf{LBI}=\mathsf{IMLL}\cup\mathsf{LJ}$

The RDvBC outsources the substructurallity in $\mathsf{IMLL}$ to Boolean
constraints. Hence, in the form of the slogan of this paper,

$\mathsf{IMLL}=\mathsf{LJ}\oplus\mathcal{B}$

In this section, we have chosen to study BI (as opposed to just IMLL) to
illustrate the modularity of constraint systems. That is, we only have
constraints participating actively in part of the sequent calculus for BI, but
with the same overall effect since the other part conserves them. Abusing the
slogan somewhat, we may express the work of this section as follows:

$\mathsf{LBI}=(\mathsf{LJ}\oplus\mathcal{B})\cup\mathsf{LJ}$

This paper aims to study the use of constraints in proof systems in general.
It provides conditions under which they exist and illustrates the use of
constraints to study metatheory.

##  3 Background

We have two things to set up to give a general presentation of algebraic
constraint systems: algebra and propositional logic. The former is captured by
first-order classical logic (FOL) (e.g., as Boolean algebra is captured by its
axiomatization in Section 2), and the latter is given by a general account of
propositional logic as a propositional language together with a consequence
relation. There are many presentations of these subjects within the
literature; therefore, to avoid confusion, in this section, we define them as
they are used in this paper. Importantly, this section introduces much
notation used in the rest of the paper. As we wish to reserve traditional
symbols such as $\vdash_{\mathsf{}}$ and $\to$ for the object-logics, we will
use $\mathbin{{\scriptstyle\blacktriangleright}}$ and $\Rightarrow$ for the
meta-logic. In both cases, we use the symbol $\triangleright$ as the sequents
symbol, regarding $\vdash_{\mathsf{}}$ and
$\mathbin{{\scriptstyle\blacktriangleright}}$ as _consequence_ relations.

###  3.1 First-order Classical Logic

This section presents first-order classical logic (FOL), which we use to
define what we mean by algebra in _algebraic_ constraints. We assume
familiarity with FOL, so give a terse (but complete) summary to keep the paper
self-contained. In particular, we assume familiarity with proof theory for FOL
— as covered in, for example, Troelstra and Schwichtenberg
[troelstra2000basic], and Negri and von Plato [negri2001].

######  Definition 3.1 (First-order Language).

An alphabet is a tuple
$\mathscr{A}:=\langle\mathbb{R},\mathbb{F},\mathbb{K},\mathbb{V}\rangle$ in
which $\mathbb{R}$, $\mathbb{F}$, $\mathbb{K}$, and $\mathbb{V}$ are pairwise
disjoint countable sets of symbols, and each element of $\mathbb{R}$,
$\mathbb{F}$ and $\mathbb{K}$ has a fixed arity. The terms, atoms, and well-
formed formulae (wffs) of an alphabet are as follows:

  * -

The set $\mathbb{TERM}(\mathscr{A})$ of _terms_ from $\mathscr{A}$ is the
smallest set containing $\mathbb{K}$ and $\mathbb{V}$ such that, for any
$F\in\mathbb{F}$, if F has arity $n$ and
$T_{1},...,T_{n}\in\mathbb{TERM}(\mathscr{A})$, then
$F(T_{1},...,T_{n})\in\mathbb{TERM}(\mathscr{A})$

  * -

The set $\mathbb{ATOMS}(\mathbb{A})$ is set of strings $R(T_{1},...,T_{n})$
such that $R\in\mathbb{R}$ has arity $n$ and
$T_{1},...,T_{n}\in\mathbb{TERM}(\mathscr{A})$

  * -

The set $\mathbb{WFF}(\mathscr{A})$ of _formulae_ from $\mathscr{A}$ is
defined by the following grammar, in which $X\in\mathbb{V}$:

$\Phi:=A\in\mathbb{ATOMS}(\mathbb{A})\mid\Phi\Rightarrow\Phi\mid\Phi\with\Phi\mid\Phi\parr\Phi\mid\bot\mid\forall
X\Phi\mid\exists X\Phi$

$\triangleleft$

The symbols $\Rightarrow$, $\with$, $\parr$, and $\bot$ are _implication_ ,
_conjunction_ , _disjunction_ , and _absurdity_ , respectively, in FOL. The
more traditional symbols, such as $\to$, $\land$, and $\lor$, are reserved for
other logics in the paper. We use the usual convention for suppressing
brackets; that is, conjunction ($\with$) and disjunction ($\parr$) bind more
strongly than implication ($\Rightarrow$). Moreover, we may use the usual
auxiliary terminology for first-order languages (e.g., _sub-formula_ ,
_closed-formula_ , _sentence_ , etc.) without further explanation. Let be $X$
a variable, $T$ be a term, and $\Phi$ a wff; we write $\Phi[X\mapsto T]$ to
denote the result of replacing every free occurrence of $X$ by the term $T$ so
that no variable in $T$ becomes bound in $\Phi$ after the substitution.

######  Definition 3.2 (First-order Sequent).

A first-order sequent is a pair $\Pi\triangleright\Sigma$ in which $\Pi$ and
$\Sigma$ are multisets of first-order formulae. $\triangleleft$

We think of sequents as unjudged statements, hence we use a sequent
constructor $\triangleright$ instead of the consequence relation
($\mathbin{{\scriptstyle\blacktriangleright}}$). For example, though
$\varnothing\triangleright\varnothing$ is a well-formed sequent in FOL, it is
not a consequence of the logic.

####  3.1.1 Proof Theory

One way to characterize FOL — that is, the consequence relation
$\mathbin{{\scriptstyle\blacktriangleright}}$ — is by provability in a sequent
calculus.

######  Definition 3.3 (Sequent Calculus $\mathsf{G3c}$).

The sequent calculus $\mathsf{G3c}$ is composed of the rules in Figure 3 in
which $T$ is a term free for $X$ in $\Phi$ and $Y$ is an eigenvariable.
$\triangleleft$

$\begin{array}[]{c@{\qquad}c}\Phi,\Pi\triangleright\Sigma,\Phi&\bot,\Pi\triangleright\Sigma\\\\[6.45831pt]
\Phi\with\Psi,\Pi\triangleright\Sigma\Phi,\Psi,\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,\Phi\with\Psi\lx@proof@logical@and\Pi\triangleright\Sigma,\Phi\Pi\triangleright\Sigma,\Psi\\\\[6.45831pt]
\Phi\parr\Psi,\Pi\triangleright\Sigma\lx@proof@logical@and\Phi,\Pi\triangleright\Sigma\Psi,\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,\Phi\parr\Psi\Pi\triangleright\Sigma,\Phi,\Psi\\\\[6.45831pt]
\Phi\Rightarrow\Psi,\Pi\triangleright\Sigma\lx@proof@logical@and\Pi\triangleright\Sigma,\Phi\Psi,\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,\Phi\Rightarrow\Psi\Phi,\Pi\triangleright\Sigma,\Psi\\\\[6.45831pt]
\forall X\Phi,\Pi\triangleright\Sigma\forall X\Phi,\Phi[X\mapsto
T],\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,\forall
X\Phi\Pi\triangleright\Sigma,\Phi[X\mapsto Y]\\\\[6.45831pt] \exists
X\Phi,\Pi\triangleright\Sigma\Phi[X\mapsto
Y],\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,\exists
X\Phi\Pi\triangleright\Sigma,\exists X\Phi,\Phi[X\mapsto T]\end{array}$

Figure 3: Sequent Calculus $\mathsf{G3c}$

We write $\Pi\vdash_{\mathsf{G3c}}\Sigma$ to denote that there is a
$\mathsf{G3c}$-proof of $\Pi\triangleright\Sigma$. Troelstra and
Schwichtenberg [troelstra2000basic] proved that $\mathsf{G3c}$-provability
characterizes classical consequence:

###### Proposition 3.4

Let $\Pi$ and $\Sigma$ be multisets of formulae,

$\Pi\mathbin{{\scriptstyle\blacktriangleright}}\Sigma\qquad\mbox{iff}\qquad\Pi\vdash_{\mathsf{G3c}}\Sigma$

We have chosen to use $\mathsf{G3c}$ to characterize FOL, as opposed to other
proof systems, because of its desirable proof-theoretic properties — for
example, Troelstra and Schwichtenberg [troelstra2000basic] have shown that the
rules of the calculus are (height-preserving) invertible, and that the
following rules are admissible:

$\Phi,\Pi\triangleright\Sigma\Pi\triangleright\Sigma\quad\Pi\triangleright\Sigma,\Phi\Pi\triangleright\Sigma\quad\Phi,\Pi\triangleright\Sigma\Phi,\Phi,\Pi\triangleright\Sigma\quad\Pi\triangleright\Sigma,\Phi\Pi\triangleright\Sigma,\Phi,\Phi$

####  3.1.2 Model-theoretic Semantics.

Another way to characterize FOL is by validity in its model-theoretic
semantics. As mentioned above, we assume familiarity with the subject and
therefore give a terse but complete account of definitions to keep the paper
self-contained.

######  Definition 3.5 (First-order Structure).

A first-order structure is a tuple
$\mathcal{S}=\langle\mathbb{U},\mathbb{R},\mathbb{F},\mathbb{K}\rangle$ in
which $\mathbb{U}$ is a countable set of elements,
$\mathbb{K}\subseteq\mathbb{U}$, $\mathbb{F}$ is a countable set of operators
on $\mathbb{U}$ (i.e., endomorphisms $f:\mathbb{U}^{n}\to\mathbb{U}$, for
finite $n$), and $\mathbb{R}$ is a countable set of relations on $\mathbb{U}$.
$\triangleleft$

######  Definition 3.6 (Interpretation).

Let $\mathcal{S}:=\langle\mathbb{U},\mathbb{R},\mathbb{F},\mathbb{K}\rangle$
be a first-order structure, and let
$\mathscr{A}:=\langle\mathbb{R}^{\prime},\mathbb{F}^{\prime},\mathbb{K}^{\prime},\mathbb{V}\rangle$
be an alphabet. An interpretation of $\mathscr{A}$ in $\mathcal{S}$ is a
function $\llbracket-\rrbracket$ satisfying the following:

  * -

if $X\in\mathbb{V}$, then $\llbracket X\rrbracket\in\mathbb{U}$;

  * -

if $C\in\mathbb{K}^{\prime}$, then $\llbracket C\rrbracket\in\mathbb{K}$;

  * -

if $F\in\mathbb{F}^{\prime}$, then $\llbracket F\rrbracket\in\mathbb{F}$, and
the arity of $\llbracket F\rrbracket$ is the arity of $F$;

  * -

if $R\in\mathbb{R}^{\prime}$, then $\llbracket R\rrbracket\in\mathbb{R}$, and
the arity of $\llbracket R\rrbracket$ is the arity of $R$.

$\triangleleft$

We may write $\llbracket-\rrbracket:\mathscr{A}\to\mathcal{S}$ to denote that
$\llbracket-\rrbracket$ is an interpretation of $\mathscr{A}$ in
$\mathcal{S}$. Interpretations extend to terms as follows:

$\llbracket F(T_{1},...,T_{n})\rrbracket:=\llbracket F\rrbracket(\llbracket
T_{1}\rrbracket,...,\llbracket T_{n}\rrbracket)$

In this paper, we use the term _abstraction_ for what is traditionally
referred to as a _model_. This is to avoid confusion as we consider the
semantics of various propositional logics in subsequent sections, where the
term _model_ will be significant.

######  Definition 3.7 (Abstraction).

An abstraction of an alphabet $\mathscr{A}$ is a pair
$\mathfrak{A}:=\langle\mathcal{S},\llbracket-\rrbracket\rangle$ in which
$\mathcal{S}$ is a structure and
$\llbracket-\rrbracket:\mathscr{A}\to\mathcal{S}$. $\triangleleft$

######  Definition 3.8 (Truth in an Abstraction).

Let $\mathscr{A}$ be an alphabet, let $\phi$ be a formula over $\mathscr{A}$,
and let $\mathfrak{A}=\langle\mathcal{S},\llbracket-\rrbracket\rangle$ be an
abstraction of $\mathscr{A}$. The formula $\phi$ is true in $\mathfrak{A}$ iff
$\mathfrak{A}\Vvdash\phi$, which is defined inductively by the clauses in
Figure 4. $\triangleleft$

$\begin{array}[]{lcl}\mathfrak{M}\Vvdash
R(T_{1},...,T_{n})&\qquad\mbox{iff}&\langle\llbracket
T_{1}\rrbracket,...,\llbracket T_{n}\rrbracket\rangle\in\llbracket
P\rrbracket\\\\[4.30554pt]
\mathfrak{M}\Vvdash\Phi\Rightarrow\Psi&\qquad\mbox{iff}&\mbox{not
$\mathfrak{M}\Vvdash\Phi$ or $\mathfrak{M}\Vvdash\Psi$}\\\\[4.30554pt]
\mathfrak{M}\Vvdash\Phi\with\Psi&\qquad\mbox{iff}&\mbox{$\mathfrak{M}\Vvdash\Phi$
and $\mathfrak{M}\Vvdash\Psi$}\\\\[4.30554pt]
\mathfrak{M}\Vvdash\Phi\parr\Psi&\qquad\mbox{iff}&\mbox{$\mathfrak{M}\Vvdash\Phi$
or $\mathfrak{M}\Vvdash\Psi$}\\\\[4.30554pt]
\mathfrak{M}\Vvdash\bot&\qquad\mbox{iff}&\mbox{never}\\\\[4.30554pt]
\mathfrak{M}\Vvdash\forall
X\Phi&\qquad\mbox{iff}&\mbox{$\mathfrak{M}\Vvdash\Phi[X\mapsto T]$ for any
$T\in\mathbb{TERM}(\mathscr{A})$}\\\\[4.30554pt] \mathfrak{M}\Vvdash\exists
X\Phi&\qquad\mbox{iff}&\mbox{$\mathfrak{M}\Vvdash\Phi[X\mapsto T]$ for some
$T\in\mathbb{TERM}(\mathscr{A})$ }\end{array}$

Figure 4: Truth in an Abstraction

We may extend the truth of formulae in an abstraction to the truth of
(multi-)sets of formulae by requiring that all the elements in the set are
true in the abstraction — that is, if $\mathfrak{A}$ is a model and $\Pi$ is a
multiset of formulae,

$\mathfrak{A}\Vvdash\Pi\qquad\mbox{ iff }\qquad\mathfrak{A}\Vvdash\Phi\mbox{
for every }\Phi\in\Pi$

Gödel [Godel] — see also van Dalen [vanDalen] — proved that abstractions
characterize FOL:

###### Proposition 3.9

Let $\Pi$ and $\Sigma$ be multisets of formulae,

$\begin{array}[]{lcl}\Pi\mathbin{{\scriptstyle\blacktriangleright}}\Sigma&\mbox{iff}&\mbox{
for any abstraction $\mathfrak{A}$, if $\mathfrak{A}\Vvdash\phi$ for any
$\phi\in\Pi$,}\\\ &&\mbox{then there is $\psi\in\Sigma$ such that
$\mathfrak{A}\Vvdash\psi$}\end{array}$

This concludes the summary of FOL.

###  3.2 Propositional Logic

There is no consensus in the literature on what propositional logic means.
This paper uses a relatively broad definition that captures the most common
propositional logics (e.g., classical propositional logic, intuitionistic
propositional logic, modal logics, linear logics, bunched logics, etc.). We
include context-formers explicitly as a part of the language of propositional
logics. More precisely, we include _data_ -formers as they may appear on
either the left or right of sequents for the propositional logics, and we use
‘context’ to refer to the left of sequents. This is useful for two reasons:
first, it enables us to move between the propositional logics without
ambiguity; second, it enables us to handle propositional logics that are
expressed in terms of more complex data structures of formulae than lists,
multisets, or sets, such as the family of relevance logics (see, for example,
Read [Read1988]) and the family of bunched logics (see, for example, work by
Docherty, O’Hearn and Pym [ohearn1999logic, Pym2003, Docherty2019]).
Throughout, we give a running example of normal modal logics, which relates
the work of this paper to that of Negri [Negri2005].

######  Definition 3.10 (Propositional Alphabet).

A propositional alphabet is a tuple of three elements
$\mathscr{P}:=\langle\mathbb{A},\mathbb{O},\mathbb{C}\rangle$ such that
$\mathbb{A}$, $\mathbb{O}$, and $\mathbb{C}$ are pairwise disjoint sets of
symbols such that $\mathbb{A}$ is countable and $\mathbb{O}$ and $\mathbb{C}$
are finite. The symbols in $\mathbb{O}$ and $\mathbb{C}$ have a fixed arity.
$\triangleleft$

The elements of $\mathbb{A}$ are _atomic propositions_ , the elements of
$\mathbb{O}$ are _operators_ , and the elements of $\mathbb{C}$ are _data-
constructors_. We use the term _operators_ to subsume ‘connectives’ and
‘modalities’ in the traditional terminology. Similarly, we use the term ‘data-
constructor’ as a neutral term for what is sometimes called a ‘context-former’
as we shall have data both on the left and right of sequents with possibly
different constructors and reserve the term ‘context’ for the left-hand side.

######  Definition 3.11 (Formula, Data, Sequent).

Let $\mathscr{P}:=\langle\mathbb{A},\mathbb{O},\mathbb{C}\rangle$ be a
propositional alphabet. The set of formulae, data, and sequents from
$\mathscr{P}$ are as follows:

  * -

The set of propositional formulae $\mathbb{FORM}(\mathscr{P})$ is the smallest
set containing $\mathbb{A}$ such that, for any
$\phi_{1},...,\phi_{k}\in\mathbb{FORM}(\mathscr{P})$ and $\circ\in\mathbb{O}$,
if $\circ$ has arity $n$, then
$\circ(\phi_{1},...,\phi_{n})\in\mathbb{FORM}(\mathscr{P})$

  * -

The set $\mathbb{DATA}({\mathscr{P}})$ is the smallest set containing
$\mathbb{FORM}(\mathscr{P})$ such that, for any
$\delta_{1},...,\delta_{n}\in\mathbb{DATA}(\mathscr{P})$ and
$\bullet\in\mathbb{C}$, if $\bullet$ has arity $n$, then
$\bullet(\delta_{1},...,\delta_{n})\in\mathbb{DATA}(\mathscr{P})$

  * -

A $\mathscr{P}$-sequent is a pair $\Gamma\triangleright\Delta$ in which
$\Gamma,\Delta\in\mathbb{DATA}(\mathscr{P})$.

$\triangleleft$

######  Example 3.12.

The basic modal alphabet is
$\mathscr{B}=\langle\mathbb{A},\\{\land,\lor,\neg,\square\\},\\{\varnothing,\fatcomma,\fatsemi\\}\rangle$.
The arities of $\land$, $\lor$, , and $\fatsemi$ is $2$; the arities of $\neg$
and $\square$ is $1$; and, the arity of $\varnothing$ is $0$. We may write
$\phi\supset\psi$ to abbreviate $\neg\phi\lor\psi$.

Let $\and{p}_{1},\and{p}_{2},\and{p}_{3}\in\mathbb{A}$. Using infix notation,
the following are examples of elements from $\mathbb{FORM}(\mathscr{B})$:

$\and{p_{3}}\qquad(\and{p}_{1}\land\and{p}_{2})\qquad(\and{p}_{3}\supset(\and{p}_{1}\land\and{p}_{1}))$

As well as being elements of $\mathbb{FORM}(\mathscr{B})$, they are also
elements in $\mathbb{DATA}(\mathscr{B})$.

Another example of an element from $\mathbb{DATA}(\mathscr{B})$ is the
following:

$\and{p_{3}}\fatcomma(\and{p}_{3}\supset(\and{p}_{1}\land\and{p}_{2}))$

The following is an example of a $\mathscr{B}$-sequent:

$\and{p}_{3}\fatcomma\and{p}_{3}\supset(\and{p}_{1}\land\and{p}_{2})\triangleright\and{p}_{1}\land\and{p}_{2}$

$\Diamond$

This completes the definition of the language of a propositional logic
generated by an alphabet. What makes language into a logic is a notion of
consequence.

######  Definition 3.13 (Propositional Logic).

Let $\mathscr{A}$ be a propositional alphabet. A propositional logic over
$\mathscr{A}$ is a relation $\vdash_{\mathsf{}}$ over $\mathscr{A}$-sequents.
$\triangleleft$

The relation $\vdash_{\mathsf{}}$ is called the _consequence judgment_ of the
logic; its elements are _consequences_. We write
$\Gamma\vdash_{\mathsf{}}\Delta$ to denote that the sequent
$\Gamma\triangleright\Delta$ is a consequence. This definition of
propositional logic needs more sophistication in many regards — for example,
nothing renders the operators of the alphabet as logical constants — but the
point is not to satisfy the doxastic interpretation of what constitutes a
logic. Interesting though that may be, it amounts to refining the current
definition. What is given here suffices for present purposes and encompasses
the vast array of propositional logics in the literature.

####  3.2.1 Proof Theory

In this paper, we are concerned about the proof-theoretic characterization of
a logic and what it tells us about that logic. Fix a propositional alphabet
$\mathscr{P}$.

######  Definition 3.14 (Sequent Calculus).

A rule $\mathsf{r}$ over $\mathscr{P}$-sequents is a (non-empty) relation on
$\mathscr{P}$-sequents; a rule with arity one is an axiom. A sequent calculus
is a set of rules at smallest one of which is an axiom. $\triangleleft$

Note that $\mathsf{LBI}_{\mathcal{B}}$ in Section 2 does not contain axioms
and is, therefore, not a sequent calculus according to this definition. This
is because we regard it as a _constraint system_ in which axioms are not
necessary — see Section 4.

We have not defined rules by rule-figures and do not assume they are
necessarily closed under substitution. This allows us to speak of rules with
side-conditions — see, for example, $\mathsf{e}\in\mathsf{LBI}$ in Section 2.
Of course, we will otherwise follow standard conventions — see, for example,
Troelstra and Schwichtenberg [troelstra2000basic].

Let $\mathsf{r}$ be a rule, the situation $\mathsf{r}(C,P_{1},...,P_{n})$ may
be denoted as follows:

$C\lx@proof@logical@and P_{1}\hdots P_{n}$

In such instances, the string $C$ is called the conclusion, and the strings
$P_{1},...,P_{n}$ are called the premisses.

######  Example 3.15 (Example 3.12 cont’d).

The rule $\mathsf{\land_{R}}$ over basic modal sequents is defined by the
following figure without any side-conditions:

$\mathrm{\Gamma}\triangleright\Delta\fatcomma\phi\land\psi\lx@proof@logical@and\mathrm{\Gamma}\triangleright\Delta\fatcomma\phi\mathrm{\Gamma}\triangleright\Delta\fatcomma\psi$

This rule is admissible for the normal modal logic $K$ — see Blackburn et al.
[Blackburn2001]. That is, let $\vdash_{\mathsf{K}}$ be the consequence
relation for $K$ (over the basic modal alphabet $\mathscr{B}$): if
$\mathrm{\Gamma}\vdash_{\mathsf{K}}\Delta\fatcomma\phi$ and
$\mathrm{\Gamma}\vdash_{\mathsf{K}}\Delta\fatcomma\psi$, then
$\mathrm{\Gamma}\vdash_{\mathsf{K}}\Delta\fatcomma\phi\land\psi$. $\Diamond$

######  Definition 3.16 (Derivation).

Let $\mathsf{L}$ be a sequent calculus. The set of $\mathsf{L}$-derivations is
defined inductively as follows:

  * -

Base Case. If $C$ is a $\mathscr{P}$-sequent, then the tree consisting of just
the node $C$ is an $\mathsf{L}$-derivation.

  * -

Inductive Step. Let $\mathcal{D}_{1},...,\mathcal{D}_{n}$ are
$\mathsf{L}$-derivations, with roots $P_{1},...,P_{n}$, respectively, and let
$\mathsf{r}\in\mathsf{L}$ be a rule such that $\mathsf{r}(C,P_{1},...,P_{n})$
obtains. The tree with root $C$ and immediate sub-trees
$\mathcal{D}_{1},...,\mathcal{D}_{n}$ is a $\mathsf{L}$-derivation.

$\triangleleft$

######  Definition 3.17 (Proof).

Let $\mathsf{L}$ be a sequent calculus. An $\mathsf{L}$-derivation
$\mathcal{D}$ is a proof iff the leaves of $\mathcal{D}$ are instances of
axioms of $\mathsf{L}$. $\triangleleft$

We write $\Gamma\vdash_{\mathsf{L}}\Delta$ to denote that there is a
$\mathsf{L}$-proof of the sequent $\Gamma\triangleright\Delta$. A sequent
calculus may have the following relationships to a propositional logic
($\vdash_{\mathsf{}}$):

  * -

Soundness: If $\Gamma\vdash_{\mathsf{L}}\Delta$, then
$\Gamma\vdash_{\mathsf{}}\Delta$.

  * -

Completeness: If $\Gamma\vdash_{\mathsf{}}\Delta$, then
$\Gamma\vdash_{\mathsf{L}}\Delta$.

In saying that $\mathsf{L}$ is a sequent calculus for a propositional logic
(i.e., that it characterizes that logic), we assert that $\mathsf{L}$ is sound
and complete for that logic.

######  Example 3.18 (Example 3.15 cont’d).

We may characterize modal logics, including $K$, by axiom systems — see, for
example, Blackburn et al. [Blackburn2001]. Each such system $\mathsf{A}$ is a
sequent calculus in the general sense of this paper. $\Diamond$

This concludes the proof-theoretic account of propositional logics in this
paper.

####  3.2.2 Model-theoretic Semantics

We now give a generic account of model-theoretic semantics (M-tS) that can
define a logic over a propositional language. By M-tS we mean a frame
semantics _à la_ Kripke [Kripke1963, kripke1965semantical] — see also Beth
[Beth1955]. We follow Blackburn et al. [Blackburn2001] in the approach for a
general account of M-tS.

######  Definition 3.19 (Type).

A type $\tau$ is a list of non-negative integers. $\triangleleft$

######  Definition 3.20 (Frame, Assignment, Pre-model).

Let $\tau:=\langle t_{1},...,t_{n}\rangle$ be a type. A $\tau$-frame is a
tuple $\langle\mathbb{U},k_{1},...,k_{n}\rangle$ in which $\mathbb{U}$ is a
set and $k_{i}$ is a relation on $\mathbb{U}$ of arity $t_{i}$. Let
$\mathscr{P}=\langle\mathbb{A},\mathbb{O},\mathbb{C}\rangle$ be a
propositional alphabet. An assignment of $\mathscr{P}$ to $\mathcal{F}$ is a
mapping from propositional atoms to sets of worlds,
$I:\mathbb{A}\to\wp(\mathbb{U})$. A $\tau$-pre-model over $\mathscr{P}$ is a
pair $\mathfrak{M}:=\langle\mathcal{F},I\rangle$, in which $\mathcal{F}$ is a
$\tau$-frame and $I$ is an assignment of $\mathscr{P}$ to $\mathcal{F}$.
$\triangleleft$

The elements of $\mathbb{U}$ are called possible worlds. One possible
objection to the definition of a frame is the absence of operators (i.e.,
endomorphisms $f:\mathbb{U}^{n}\to\mathbb{U}$). This is to simplify the setup
and is without loss of generality as operators may be regarded as particular
types of relations; that is, the operator $f:\mathbb{U}^{n}\to\mathbb{U}$
corresponds to the $(n+1)$-ary relation $R$ satisfying $R(w,u_{1},...,u_{n})$
iff $w=f(u_{1},...,u_{n})$.

Intuitively, a formula $\phi$ is true in a model $\mathfrak{M}$ at a world $w$
if the world $w$ satisfies the formulas.

######  Definition 3.21 (Satisfaction for a Type).

Let $\tau$ be a type and $\mathscr{P}$ a propositional alphabet. A
$\tau$-satisfaction relation for $\mathscr{P}$ is a relation $\Vdash$
parameterized by $\tau$-pre-models between worlds $w$ in the pre-models
$\mathfrak{M}=\langle\mathcal{F},I\rangle$ and $\mathscr{P}$-data such that
the following holds:

$\mathfrak{M},w\Vdash\and{p}\qquad\mbox{iff}\qquad w\in I(\and{p})$

$\triangleleft$

######  Definition 3.22 (Semantics).

Let $\tau$ be a type and $\mathscr{P}$ a propositional alphabet. A semantics
is a pair $\mathfrak{S}:=\langle\mathbb{M},\Vdash\rangle$ in which
$\mathbb{M}$ is a set of $\tau$-pre-models and $\mathbb{\Vdash}$ is a
$\tau$-satisfaction relation for $\mathscr{P}$. $\triangleleft$

######  Definition 3.23.

Let $\mathfrak{S}$ be a semantics. A sequent $\Gamma\triangleright\Delta$ is
valid in $\mathfrak{S}$ — denoted $\Gamma\vDash_{\mathfrak{S}}\Delta$ — iff,
for any $\mathfrak{M}\in\mathbb{M}$ and any $w\in\mathfrak{M}$, if
$\mathfrak{M},w\Vdash\Gamma$, then $\mathfrak{M},w\Vdash\Delta$.
$\triangleleft$

######  Example 3.24 (Example 3.18 cont’d).

Fix the type $\tau:=\langle 2\rangle$. An example of a $\tau$-frame is a pair
$\langle\\{x,y\\},R\rangle$ in which $R$ is a binary relation on $\\{x,y\\}$.
Partition the atoms $\mathbb{A}$ into two classes $\mathbb{A}_{1}$ and
$\mathbb{A}_{2}$; an example of an assignment $I:\mathbb{A}\to\wp(\\{x,y\\})$
is given as follows:

$I(\and{p}):=\cases{x}&\text{if}\and{p}\in\mathbb{A}_{1}\\\
y\text{if}\and{p}\in\mathbb{A}_{2}$

The pair $\mathfrak{M}:=\langle\mathcal{F},I\rangle$ is an example of a model
over the basic modal alphabet $\mathscr{B}$. The basic semantics
$\mathfrak{K}$ is the pair $\langle\mathbb{K},\Vdash\rangle$ in which
$\mathbb{K}$ is the set of all $\tau$-pre-models and $\Vdash$ is the smallest
relation satisfying the clauses in Figure 5 together with the following:

$\begin{array}[]{ccc}\mbox{$\mathfrak{M},w\Vdash\Delta\fatcomma\Delta^{\prime}$}&\qquad\mbox{iff}&\mbox{
$\mathfrak{M},w\Vdash\Delta$ and $\mathfrak{M},w\Vdash\Delta^{\prime}$}\\\
\mbox{$\mathfrak{M},w\Vdash\Delta\fatsemi\Delta^{\prime}$}&\qquad\mbox{iff}&\mbox{$\mathfrak{M},w\Vdash\Delta$
or $\mathfrak{M},w\Vdash\Delta^{\prime}$}\end{array}$

The validity judgment $\vDash_{\mathfrak{K}}$ defines the modal logic $K$ —
see, for example, Kripke [Kripke1963], Blackburn et al. [Blackburn2001], and
Fitting and Mendelsohn [Fitting1998].

$\Diamond$

$\begin{array}[]{lcl}\mathfrak{M},w\Vdash\and{p}&\qquad\mbox{iff}&w\in
I(\and{p})\\\\[4.30554pt]
\mathfrak{M},w\Vdash\phi\land\psi&\qquad\mbox{iff}&\mbox{$\mathfrak{M},w\Vdash\phi$
and $\mathfrak{M},w\Vdash\psi$}\\\\[4.30554pt]
\mathfrak{M},w\Vdash\phi\lor\psi&\qquad\mbox{iff}&\mbox{$\mathfrak{M},w\Vdash\phi$
or $\mathfrak{M},w\Vdash\psi$}\\\\[4.30554pt]
\mathfrak{M},w\Vdash\neg\phi&\qquad\mbox{iff}&\mbox{not
$\mathfrak{M},w\Vdash\phi$}\\\\[4.30554pt]
\mathfrak{M},w\Vdash\Box\phi&\qquad\mbox{iff}&\mbox{for any $u$, if $wRu$,
then $\mathfrak{M},u\Vdash\phi$}\end{array}$

Figure 5: Satisfaction for $K$

The significance of $\mathbb{M}$ in the definition of a semantics is that one
may not want to consider all pre-models but instead require them to satisfy a
specific condition — see, for example, the persistence condition for the
semantics of intuitionistic propositional logic in Section 6.

The notion of semantics in this paper is generous, including many relations
that one would not typically accept as semantics. This is to keep the
presentation simple and intuitive. In the next section, we restrict attention
to satisfaction relations that admit particular presentations that enable us
to analyse them, but doing so presently would obscure the setup.

Historically, the _a priori_ definition of a consequence-relation has been by
validity in a semantics. In this paper, we only work with logics for which we
assume there is a sequent calculus. Therefore, we may use the nomenclature of
Section 3.2 to relate entailment to consequence via provability. A sequent
calculus $\mathsf{L}$ may have the following relationship to a semantics
$\mathfrak{S}$:

  * -

Soundness: If $\Gamma\vdash_{\mathsf{L}}\Delta$, then
$\Gamma\vDash_{\mathfrak{S}}\Delta$.

  * -

Completeness: If $\Gamma\vDash_{\mathfrak{S}}\Delta$, then
$\Gamma\vdash_{\mathsf{L}}\Delta$.

This completes the summary of propositional logics. Moreover, it completes the
technical background to this paper. There are various judgments present, whose
relationship are important for the rest of the paper. In the beginning of the
next section we provide a brief summary of how all this background is used
before proceeding with the technical work.

##  4 Constraint Systems

This section provides a formal definition of constraint systems. Briefly, a
_constraint system_ is a sequent calculus in which the data may carry labels
representing expressions over some algebra. Rules may manipulate those
expressions or demand constraints on them. At the end of a construction in a
constraint system, one checks to see that the constraints are coherent and
admit an interpretation in the intended algebra. This generalizes the setup of
RDvBC in Section 2 to an arbitrary algebra and an arbitrary propositional
logic. In the next section (Section 5), we provide a method for producing
constraint systems in a modular way, and in the one after (Section 6), we
illustrate their use in studying model theory.

The work in this section is technical and abstract; therefore, we give a brief
overview summarizing the main ideas. We begin with a propositional logic
$\vdash_{\mathsf{}}$ over an alphabet $\mathscr{P}$ and a sequent calculus
$\mathsf{L}$ which has some desirable features but which is not immediately
related to the logic — for example, in Section 2, we had BI as the
propositional logic and $\mathsf{L}$ a version of $\mathsf{LJ}$ in which
contexts are maintained during reduction. We then introduce an algebra, which
we understand in terms of first-order structures $\mathcal{A}$, and present in
terms of a first-order alphabet $\mathscr{A}$ — for example, see the
presentation of Boolean algebra in Section 2. We fuse $\mathscr{P}$ and
$\mathscr{A}$ creating a language $\mathscr{P}\oplus\mathscr{A}$ in which the
algebra is used to label $\mathscr{P}$-data. We introduce a valuation map
$\nu_{I}$, parameterized by interpretations $I:\mathscr{A}\to\mathcal{A}$,
that maps $\mathscr{P}\oplus\mathscr{A}$-data to $\mathscr{P}$-data. This
defines the action the algebra has on the data. A constraint system is a
generalized notion of a sequent calculus of
$\mathscr{P}\oplus\mathscr{A}$-sequents, which may have $\mathscr{A}$
expressions as local or global constraints on the correctness of inferences —
see, for example, $\mathsf{LBI}_{\mathcal{B}}$ in Section 2. Finally, we give
correctness conditions for constraint systems: first, a constraint system
$\mathsf{C}$ is sound and complete, relative to $\nu_{I}$, for the logic
$\vdash_{\mathsf{}}$ iff its constructions witness all and only the
consequence of the logic; second, a constraint system $\mathsf{C}$ is faithful
and adequate, relative to $\nu_{I}$, for a sequent calculus
$\mathsf{L}^{\prime}$ iff its constructions witness all and only
$\mathsf{L}^{\prime}$-proofs. Throughout the rest of the paper, we illustrate
how constraint systems with these correctness conditions aid in studying
logic.

The section is composed of three parts. Section 4.1 explains the paradigmatic
shift necessary for constraint systems: one constructs proofs upward rather
than downward. In Section 4.2, we define constraint systems formally as the
enrichment of a sequent calculus by an algebra of constraints. Finally, in
Section 4.3, we define correctness conditions relating constraint systems to
logics and their proof-theoretic formulations with sequent calculi.

###  4.1 Reductive Logic

The traditional paradigm of logic proceeds by inferring a conclusion from
established premisses using an _inference rule_. This is the paradigm known as
_deductive logic_ :

$\text{Conclusion}\lx@proof<EMAIL_ADDRESS>
In contrast, the experience of the use of logic is often dual to deductive
logic in the sense that it proceeds from a putative conclusion to a collection
of premisses that suffice for the conclusion. This is the paradigm known as
_reductive logic_ :

$\text{PutativeConclusion}\lx@proof<EMAIL_ADDRESS>
Rules used backward in this way are called _reduction operators_. The objects
created using reduction operators are called _reductions_. We believe that
this idea of reduction was first explained in these terms by Kleene
[kleene2002mathematical]. There are many ways of studying reduction, and a
number of models have been considered, especially in the case of classical and
intuitionistic logic — see, for example, Pym and Ritter [Pym2004].

Historically, the deductive paradigm has dominated since it exactly captures
the meaning of truth relative to some set of axioms and inference rules, and
therefore is the natural point of view when considering _foundations of
mathematics_. However, it is the reductive paradigm from which much of
computational logic derives, including various instances of automated
reasoning — see, for example, Kowalski [Kowalski1971], Bundy [Bundy1983], and
Milner [Milner1984].

Constraint systems (e.g., $\mathsf{LBI}_{\mathcal{B}}$) sit more naturally
within the reductive perspective, with the intuition that one generates
constraints as one applies rules backwards. Therefore, in constraint systems,
when we _use_ a rule we mean it in the reductive of sense.

Having given the overall paradigm on logic in which constraint systems are
situated, we are now able to define them formally and uniformly.

###  4.2 Expressions, Constraints, and Reductions

In Section 3.2, we defined what we mean by propositional logic. Recall that we
may say _algebra_ to mean a first-order structure (see Section 3.1). In this
context, what we mean by expressions and constraints are terms and formulae,
respectively, from an alphabet in which that algebra is interpreted.

Let $\mathscr{A}$ be a (first-order) alphabet.

######  Definition 4.1 (Expression).

An $\mathscr{A}$-expression is a term over $\mathscr{A}$ — that is, an element
of $\mathbb{TERM}(\mathscr{A})$ $\triangleleft$

######  Definition 4.2 (Constraint).

An $\mathscr{A}$-constraint is a formula over $\mathscr{A}$ — that is, an
element of $\mathbb{WFF}(\mathscr{A})$ $\triangleleft$

When it is clear that an alphabet has been fixed, we may elide it alphabet
when discussing labelled formulae, labelled data, and enriched sequents. We
use the terms ‘expression’ and ‘constraint’ to draw attention to the fact that
we have a certain algebra in mind and a certain way that the constants and
functions of the alphabet are meant to be interpreted. For example, in Section
2, we always take symbol $+$ to always be interpreted as Boolean addition.
What may change is the interpretation of variables. In short, we have some set
of intended interpretations that are _coherent_.

######  Definition 4.3 (Coherent Interpretations).

Let $\mathbb{I}$ be a set of interpretations of an algebra $\mathcal{A}$ in
$\mathscr{A}$. The set $\mathbb{I}$ is coherent iff, for any
$I_{1},I_{2}\in\mathbb{I}$, they behave the same except possibly for atoms.
$\triangleleft$

Typically, the set of intended interpretations is maximal in the sense that
any interpretation of the algebra in the alphabet is either in the set or is
not a variant of an interpretation in the set.

We use expressions to enrich the language of the propositional logic and
thereby express meta-theoretic conditions on formulae and sequents. Let
$\mathscr{P}$ be a propositional alphabet.

######  Definition 4.4 (Labelled Data).

The set of labelled $\mathscr{P}$-data is defined inductively as follows:

  * -

Base Case. If $\phi$ is a formula and $e$ is an $\mathscr{A}$-expression, then
$\phi\cdot e$ is a $\mathscr{A}$-labelled $\mathscr{P}$-datum.

  * -

Inductive Step. If $\delta_{1}$, … , $\delta_{n}$ are labelled
$\mathscr{P}$-data, $\bullet$ is a data-constructor in $\mathscr{P}$ with
arity $n$, and $e$ is an $\mathscr{A}$-expression, then
$\bullet(\delta_{1},...,\delta_{n})\cdot e$ is a $\mathscr{A}$-labelled
$\mathscr{P}$-datum.

$\triangleleft$

######  Definition 4.5 (Enriched Sequent).

An $\mathscr{A}$-enriched $\mathscr{P}$-sequent is a pair
$\Pi\triangleright\Sigma$, in which $\Pi$ and $\Sigma$ are multisets of
$\mathscr{A}$-labelled $\mathscr{P}$-data and constraints. $\triangleleft$

We may suppress $\mathscr{A}$ and $\mathscr{P}$ when it is clear what alphabet
for what algebra is labeling what propositional language. Observe that we have
shifted from the object-logic to the meta-logic; that is enriched sequents are
a restricted form of meta-logic sequents that encapsulate object-logic
sequents with conditions expressed by expressions from the algebra. This setup
differs slightly from the presentation of RDvBC in Section 2 to simplify
presentation of the general case. Recall that data is the general name for
contexts in the propositional logic, which may be bunches. Consequently, the
presentation of RDvBC in terms of enriched sequents would consist of pairs of
multisets each of which contain only one element, the labelled bunch.

######  Example 4.6.

The are various enriched sequents in RDvBC — see Section 2. An additional
example is as follows:

$\and{p}\cdot x\fatcomma(q\fatsemi r)\cdot
y\triangleright(\and{p}\land\and{q})\cdot x$

$\Diamond$

A _constraint system_ is a generalization of sequent calculus that uses
enriched sequents and constraints. The constructions of a constraint system
are generated co-recursively on enriched sequents, producing constraints along
the way along.

######  Definition 4.7 (Constraint System).

A constraint rule is a relation between an enriched sequents and a list of
enriched sequents and constraints. A constraint system is a set of constraint
rules. $\triangleleft$

We use the same notation as in Section 3.2 for constraint rules; that is, that
$\mathsf{r}(C,P_{1},...,P_{n})$ obtains may be expressed as follows:

$C\lx@proof@logical@and P_{1}...P_{n}$

In this case, $C$ is an enriched sequent and $P_{1},...,P_{n}$ are either
enriched sequents or constraints. The terms _premiss_ and _conclusion_ are
analogous to those employed for sequent calculus rules in Section 3.2. We
assume the convention of putting constraints after enriched sequents in the
list of premisses.

######  Example 4.8 (Example 4.6 cont’d).

System $\mathsf{LBI}_{\mathcal{B}}$ in Section 2 is a constraint system.
Therefore, any rule in it is an example of a constraint rule. We shall
consider two examples.

The following is a constraint rule:

$\Delta\fatcomma\Delta^{\prime}\triangleright\phi*\psi\lx@proof@logical@and\Delta\cdot
V\triangleright\phi\Delta^{\prime}\cdot\bar{V}\triangleright\psi$

If $e$ is a label on $\Delta$, then $\Delta\cdot V$ denotes the result of
replacing $e$ by a product of $e$ and $V$. The following inference is an
instance of the rule:

$\and{p}\cdot 1\fatcomma(q\fatsemi r)\cdot
1\triangleright(\and{p}\ast\and{q})\cdot
1\lx@proof@logical@and\and{p}\cdot(1x)\fatcomma(q\fatsemi
r)\cdot(1y)\triangleright\and{p}\cdot
1\and{p}\cdot(1\bar{x})\fatcomma(q\fatsemi
r)\cdot(1\bar{y})\triangleright\and{q}\cdot 1$

Another example of a constraint rule is as follows:

$\phi\cdot y\fatcomma\Delta\cdot V\triangleright\phi\cdot 1y=1\land V=0$

Here $V$ are all the labels on $\Delta$ and $V=0$ denotes
$x_{1}=0\with....\with x_{n}=0$ if $V$ is the list $x_{1},...,x_{n}$. An
instance of the rule is the following:

$p\cdot(1x)\fatcomma(q\fatsemi r)\cdot 1y\triangleright p\cdot
1\lx@proof@logical@and 1x=11y=0$

Intuitively, this corresponds to an _axiom_ of a sequent calculus as it
reduces to constraints which, when solved, state weather or not the sequent in
the conclusion is a consequence of BI. $\Diamond$

Unlike sequent calculi, a constraint system does not necessarily contain
axioms. This is possible because the set of things generated by a constraint
system is defined co-inductively, so the restriction is unnecessary. We define
reductions co-inductively because constraint systems sit within the paradigm
of reductive logic. The reductions in this paper are all finite.

######  Definition 4.9 (Reduction in a Constraint System).

Let $\mathsf{C}$ be a constraint system and let $S$ be an enriched sequent. A
tree of enriched sequents $\mathcal{R}$ is a $\mathsf{C}$-reduction of $S$ iff
there is a rule $\mathsf{r}\in\mathsf{C}$ such that
$\mathsf{r}(S,P_{1},..,P_{n})$ obtains and the immediate sub-trees
$\mathsf{R}_{i}$, with root $P_{i}$, are as follows: if $P_{i}$ is an enriched
sequent, it is a $\mathsf{C}$-reduction of $P_{i}$; the single node $P_{i}$,
otherwise (i.e., if $P_{i}$ is a constraint). $\triangleleft$

######  Example 4.10 (Example 4.8 cont’d).

A reduction in a constraint system (the system $\mathsf{LBI}_{\mathcal{B}}$)
is given in Example 2.2. $\Diamond$

This concludes the definition of a constraint system and reduction from it. It
remains to give conditions defining how it relates to logics.

###  4.3 Correctness Conditions

The distinguishing feature of reductions in a constraint system is the
constraints. These constraints are understood as correctness conditions in two
ways. They are _global_ correctness conditions when they determine that a
completed reduction is a valid certificate witnessing that some sequent is the
consequence of a logic; this is _soundness_ and _completeness_. They are
_local_ correctness conditions when they determine that each reduction step
corresponds to a valid inference (i.e., an admissible inference) in the logic;
this is faithfulness and adequacy for some sequent calculus for the logic. Of
course, local correctness implies global correctness. In either reading, we
regard constraints in using rules as side-conditions on the reduction.

######  Definition 4.11 (Side-condition).

Let $\mathsf{C}$ be a constraint system and let $\mathcal{R}$ be a
$\mathsf{C}$-reduction. A side-condition of $\mathcal{R}$ is a constraint that
is a leaf of $\mathcal{R}$. $\triangleleft$

The side-conditions are global constraints on the reduction, determining the
conditions for which the structure is meaningful.

######  Definition 4.12 (Coherent Reduction).

Let $\mathsf{C}$ be a constraint system, let $\mathcal{R}$ be a
$\mathsf{C}$-reduction, and let $\mathbb{S}$ be the set of side-conditions of
$\mathcal{R}$. The set $\mathbb{S}$ is coherent iff there is an interpretation
in which all of the side-conditions in $\mathbb{S}$ are valid; the reduction
$\mathcal{R}$ is coherent iff $\mathbb{S}$ is coherent. $\triangleleft$

We may regard coherent reductions as proofs of certain sequents, but this
requires a method of reading what sequent of the propositional logic the
reduction asserts.

######  Definition 4.13 (Ergo).

An ergo is a map $\nu_{I}$, parameterized by intended interpretations, from
enriched sequents to sequents. $\triangleleft$

Let $\mathsf{C}$ be a constraint system and $\nu$ an ergo. We write
$\Gamma\vdash_{\mathsf{C}}^{\nu}\Delta$ to denote that there is a coherent
$\mathsf{C}$-reduction $\mathcal{R}$ of an enriched sequent $S$ such that
$\nu_{I}(S)=\Gamma\triangleright\Delta$, where $I$ is an interpretation
satisfying all the side-conditions of $\mathcal{R}$. An example of this is the
valuation given for RDvBC in Section 2 that deletes formulae and bunches
labelled by an expression that evaluates to $0$ and keeps those that evaluate
to $1$.

######  Definition 4.14 (Soundness and Completeness of Constraint Systems).

A constraint system $\mathsf{C}$ may have the following relationships to a
propositional logic:

  * -

Soundness: If $\Gamma\vdash_{\mathsf{C}}^{\nu}\Delta$, then
$\Gamma\vdash_{\mathsf{}}\Delta$.

  * -

Completeness: If $\Gamma\vdash_{\mathsf{}}\Delta$, then
$\Gamma\vdash_{\mathsf{C}}^{\nu}\Delta$.

$\triangleleft$

This defines constraint systems and their relationship to logics. Observe that
soundness and completeness is a _global_ correctness condition on reductions
in the sense that only once the reduction has been completed and one has
generated all of the constraints and solved them to find an interpretation
does one know whether or not the reduction witnesses the validity of some
sequent in the logic. In other words, a partial reduction (i.e., a reduction
to which one may still apply rules) does not necessarily contain any proof-
theoretic information about the logic.

In contrast, one may consider a _local_ correctness conditions in which
applying a reduction operator from a constraint system corresponds to using
some rules of inference in a sequent calculus for the logic. This is stronger
than the global correctness condition as when the reduction is completed, and
the constraints are solved, the resulting interpretations that allow one to
read a reduction in a constraint system as a proof in a sequent calculus for
the logic, and thus as a certificate for the validity of some sequent.

Fix a propositional alphabet $\mathscr{P}$, an algebra $\mathcal{A}$, an
alphabet $\mathscr{A}$ for that algebra, and a set $\mathbb{I}$ of intended
interpretations of $\mathscr{A}$ in $\mathcal{A}$. Fix a constraint system
$\mathsf{C}$ and an ergo $\nu$. The ergo extends to $\mathsf{C}$-reductions by
pointwise application to the enriched sequents in the tree and by deleting all
the constraints.

Using this extension, constraint systems are computational devices capturing
sequent calculi. For this reason, we do not use the terms _soundness_ and
_completeness_ , but rather use the more computational terms of _faithfulness_
and _adequacy_.

######  Definition 4.15 (Faithful & Adequate).

Let $\mathsf{C}$ be a constraint system, let $\mathsf{L}$ be a sequent
calculus, and let $\nu$ be a valuation.

  * -

System $\mathsf{C}$ is _faithful_ to $\mathsf{L}$ if, for any
$\mathsf{C}$-reduction $\mathcal{R}$ and interpretation $I$ satisfying the
constraints of $\mathcal{R}$, the application $\nu_{I}(\mathcal{R})$ is an
$\mathsf{L}$-proof.

  * -

System $\mathsf{C}$ is _adequate_ for $\mathsf{L}$ if, for any
$\mathsf{L}$-proof $\mathcal{D}$, there is a $\mathsf{C}$-reduction
$\mathcal{R}$ and an interpretation $I$ satisfying the constraints of
$\mathsf{R}$ such that $\nu_{I}(\mathcal{R})=\mathcal{D}$.

$\triangleleft$

Intuitively, constraint systems for a logic (more precisely, constraint
systems that are faithful and adequate with respect to a sequent calculus for
a logic) separate combinatorial and idiosyncratic aspects of that logic. The
former refers to how rules manipulate the data in sequents, while the latter
refers to the constraints generated by the rules. Note that this gives a
_local_ correctness condition of reductions from a constraint system as each
reductive inference in the constraint system corresponds to some reductive
inference in a sequent calculus for the logic.

In the next section (Section 5), we provide sufficient conditions for a
propositional logic to have a constraint system that evaluates to a sequent
calculus for that logic. The conditions are quite encompassing and
automatically give soundness and completeness for the sequent calculus for a
semantics for the logic. Attempting a total characterization (i.e., precisely
defining the properties a logic must satisfy in order for it to have a
constraint system and a valuation to a sequent calculus for the logic) is
unrealistic. The reason is that propositional logics, constraints systems,
algebras, and valuations, have so many degrees of freedom that one could not
plainly present their dependencies at once. Instead, one should consider such
a classification relative to a fixed structure of propositional logics (e.g.,
substructural logics with data comprising multisets of formulae), for a fixed
algebra (e.g., Boolean algebra), and fixed valuations (i.e., keeping formulae
whose label evaluate to $1$ and deleting formulae whose label evaluate to
$0$).

Significantly, having constructed a reduction in a constraint system, one must
solve the constraints before one knows what ‘proof’ the reduction represents
for the target logic. This may be challenging depending on the algebra over
which the constraint take place. Nonetheless, with even relatively simple
algebras one may have relatively useful constraint systems; for example RDvBC
uses Boolean algebra, which admits algorithmic solvers, that means one can
outsource the solving of constraints for
$\mathsf{LBI}_{\mathcal{B}}$-reductions. However, the point of constraint
systems is not to _do_ proof-search but to _study_ proof-search. In this way,
how the constraints are solved is less important than how they can be
interpreted in terms of control during proof-search in the object-logic.

##  5 Example: Relational Calculi

The relational calculi introduced by Negri [Negri2005] can be viewed as
constraint systems; that is, the _constraint algebra_ is provided by a first-
order theory capturing an M-tS for a logic, and the labelling action captures
satisfaction in that semantics. Traditionally, $x:\phi$ is used in place of
$\phi\cdot x$ for relational calculi, and we shall adopted this notation for
this section to be consistent with the existing work. The change in notation
is a _aide-mémoire_ that we are working with a particular form of constraint
systems.

This section gives sufficient conditions for a sequent calculus to admit a
relational calculus. We further give conditions under which these relational
calculi (regarded as constraint systems) are faithful and adequate for a
sequent calculus for the logic. We continue the study of the modal logic $K$
in Section 3.2 as a running example.

First, we define what it means for a semantics of a propositional logic to be
first-order definable; this is a pre-condition for producing relational
calculi that express the semantics. We call the propositional logic we are
studying the _object-logic_ ; and, we call FOL the _meta-logic_. For clarity,
we use the convention prefixing _meta_ \- for structures at the level of the
meta-logic where the terminology might otherwise overlap; for example,
_formulae_ are syntactic construction at the object level, and _meta-formulae_
are syntactic construction in the meta-logic.

Second, we give a sufficient condition, called _tractability_ , for us to take
a first-order definition $\Omega$ of a semantics and produce a relational
calculus from it. Essentially, the condition amounts to unfolding $\Omega$
within $\mathsf{G3c}$ so that we can suppress all the logical structures from
the meta-logic, leaving only a labelled calculus for the propositional logic —
namely, the relational calculus.

Third, we give a method for transforming tractable definitions into sequent
calculi and prove that the result is sound and complete for the semantics.

###  5.1 Tractable Propositional Logics

Relational calculi for a logic work by internalizing a semantics of that
logic. In work by Negri [Negri2005] on relational calculi for normal modal
logics, the basic atomic formulae over which the relational calculi operate
come in two forms: they are either of the form $(x:\phi)$, in which $x$ is a
variable denoting an arbitrary world, $\phi$ is a formula, and $:$ is a
pairing symbol intuitively saying that $\phi$ is satisfied at $x$; or, they
are of the form $xRy$, in which $x$ and $y$ are variables denoting worlds and
$R$ is a relation denoting the accessibility relation of the frame semantics.
Therefore, we begin by fusing the language $\mathscr{P}$ of the object-logic
with a first-order language $\mathscr{F}$, able to express frames for the
semantics, into the first-order language we use for the relational calculi.

######  Definition 5.1 (Fusion).

Let $\mathscr{F}:=\langle\mathbb{R},\varnothing,\mathbb{K},\mathbb{V}\rangle$
be a first-order alphabet and let
$\mathscr{P}:=\langle\mathbb{A},\mathbb{O},\mathbb{C}\rangle$. The fusion
$\mathscr{F}\otimes\mathscr{P}$ is the first-order alphabet
$\langle\mathbb{R}\cup\\{:\\},\mathbb{O}\cup\mathbb{C},\mathbb{K}\cup\mathbb{A},\mathbb{V}\rangle$
$\triangleleft$

Observe that $\mathscr{P}$-formulae and $\mathscr{F}$-terms both becomes terms
in $\mathscr{F}\oplus\mathscr{P}$, and $:$ is a relation. In particular, the
object-logic operators (i.e., connectives, modalities) are function-symbols in
the fusion. Further note that $(x:\phi)$ and $(\phi:x)$ are well-formed
formulae in the fusion; the former is desirable, and the latter is not. We
require a _model theory_ $\Omega$ over the fused language such that $:$ is
interpreted as satisfaction in the semantics. Relative to such a theory, while
well-formed, the meta-formulae $(\phi:x)$ are nonsense. To aid readability, we
shall use the convention of writing $\hat{\phi}$ for meta-variables that we
intend to be interpreted as object-formulae and $\hat{\Gamma}$ or
$\hat{\Delta}$ for meta-variables that we intend to be interpreted as object-
data.

######  Definition 5.2 (Definition of a Semantics).

Let $\Omega$ be a set of sentences from a fusion
$\mathscr{F}\otimes\mathscr{P}$ and let $\mathfrak{S}$ be a semantics over
$\mathscr{P}$. The set $\Omega$ defines the semantics $\mathfrak{S}$ iff the
following holds: $\Omega,(x:\Gamma)\vdash_{\mathsf{}}(x:\Delta)$ iff
$\Gamma\vDash\Delta$. $\triangleleft$

Such theories $\Omega$ may at first appear obscure, but in practice they can
be fairly systematically constructed. Intuitively, the abstractions of
$\Omega$ are composed of models from the semantics together with an
interpretation of the satisfaction relation. Thus, $\Omega$ is typically
composed of two theories $\Omega_{1}$ and $\Omega_{2}$. The theory
$\Omega_{1}$ captures frames; for example, in modal logic, if the
accessibility relation is transitive, then $\Omega_{1}$ contains $\forall
x,y,z(xRy\with yRz\Rightarrow xRz)$. The theory $\Omega_{2}$ captures the
conditions of the satisfaction relation; for example, if the object-logic
contains an additive conjunction $\land$, then $\Omega$ may contain $\forall
x,\hat{\phi},\hat{\psi}((x:\hat{\phi}\land\hat{\psi})\Rightarrow(x:\hat{\phi})\with(x:\hat{\psi}))$
and $\forall
x,\hat{\phi},\hat{\psi}((x:\hat{\phi})\with(x:\hat{\psi})\Rightarrow(x:\hat{\phi}\land\hat{\psi}))$.
For an illustration of how $\Omega$ can be constructed according to this
intuition in even relatively complex settings, see work on the logic of
Bunched Implications by Gheorghiu and Pym [Alex:BI_Semantics].

######  Example 5.3.

By the universal closure of $(\Phi\iff\Psi)$ we mean the meta-formulae
$\Theta$ and $\Theta^{\prime}$ in which $\Theta$ is the universal closure of
$\Phi\Rightarrow\Psi$ and $\Theta^{\prime}$ is the universal closure of
$\Psi\Rightarrow\Phi$. Consider the semantics
$\mathfrak{K}=\langle\mathbb{M},\Vdash\rangle$ in Example 3.24. It is defined
by the universal closures of the formulae in Figure 6, which merits comparison
with Figure 5, together with the universal closure of the following:

$\begin{array}[]{ccc}(x:\hat{\Gamma}\fatcomma\hat{\Delta})&\iff&(x:\hat{\Gamma})\with(x:\hat{\Delta})\\\
(x:\hat{\Gamma}\fatsemi\hat{\Delta})&\iff&(x:\hat{\Gamma})\parr(x:\hat{\Delta})\end{array}$

Every model in $\mathbb{M}$ intuitively gives an abstraction of these formulas
since they simply give a formal expression of the clauses defining
satisfaction.

Notably, there is no meta-formula corresponding to atomic satisfaction — that
is, $(w:\and{p})$ — because it is handled by the structure of meta-sequents.
That is, it follows from working with validity directly (i.e., without passing
though truth-in-a-model): atomic satisfaction is captured by an atomic
tautology, $\Omega,(x:\and{p})\triangleright(x:\and{p})$. $\Diamond$

$\begin{array}[]{lcl}(w:\hat{\phi}\land\hat{\psi})&\iff&(w:\hat{\phi})\with(w:\hat{\psi})\\\\[4.30554pt]
(w:\hat{\phi}\lor\hat{\psi})&\iff&(w:\hat{\phi})\parr(w:\hat{\psi})\\\\[4.30554pt]
(w:\neg\hat{\phi})&\iff&\big{(}(w:\hat{\phi})\Rightarrow\bot\big{)}\\\\[4.30554pt]
(w:\Box\hat{\phi})&\iff&\forall u(wRu\Rightarrow(u:\hat{\phi}))\end{array}$

Figure 6: Satisfaction for Modal Logic $K$ (Symbolic)

We may use the meta-logic to characterize those propositional logics whose
semantics is particularly amenable to analysis; first-order definability is,
perhaps, the most general condition we may demand. What are some other
properties of $\Omega$ that may be useful? Since we are interested in a
_computational_ analysis of the semantics, we require that it is finite, among
other things. In particular, we restrict the structure of the theory to
something amenable to proof-theoretic analysis according to $\mathsf{G3c}$.

There is literature on generating proof systems for propositional logics
defined axiomatically; see, for example, work by Ciabattoni et al.
[Ciabattoni2008, Ciabattoni2009, CIABATTONI2012]. Within this tradition, Marin
et al. [Marin2022] have used _focusing_ in intuitionistic and classical logic,
conceived of as a meta-logic, as a general tool to uniformly express an
algorithm for turning axioms into rules applicable across different domains.
We use a similar method and, therefore, polarize the syntax for the meta-
logic.

Let $\mathbb{MA}$ be the set of meta-atoms. The _positive_ meta-formulae $P$
and _negative_ meta-formulae $N$ are defined as follows:

$\begin{array}[]{lcl}P&::=&A\in\mathbb{MA}\mid\bot\mid P\with P\mid
N\Rightarrow P\mid P\parr P\mid\exists XP\\\ N&::=&A\in\mathbb{MA}\mid N\with
N\mid P\Rightarrow N\mid\forall XN\end{array}$

This taxonomy arises from behaviour; specifically,using this taxonomy we can
define a class of formulae that we can systematically transform them into
_synthetic rules_ using focusing in $\mathsf{G3c}$. While closely related to
the taxonomy used by Marin et al. [Marin2022] it is not the same as they work
over a syntax that has positive and negative connectives.

######  Definition 5.4 (Polarity Alternation).

The number of _polarity alternations_ in a polarised formula $\Phi$ is
$\pi(\Phi)$ defined as follows:

$\pi(\Phi):=\cases{0}&\text{if}\Phi\in\mathbb{MA}\\\
\max\\{\pi(\Phi_{1}),\pi(\Phi_{2})\\}\text{if}\Phi=\Phi_{1}\circ\Phi_{2}\text{and}\circ\in\\{\with,\parr\\}\\\
\pi(\Phi_{1})\text{if}\Phi=QX\Psi\text{and}Q\in\\{\forall,\exists\\}\\\
1+\max\\{\pi(\Phi_{1}),\pi(\Phi_{2})\\}\text{if}\Phi=\Phi_{1}\Rightarrow\Phi_{2}$

$\triangleleft$

######  Definition 5.5 (Tractable Meta-formula).

A meta-formula $\Phi$ is tractable iff $\Phi$ is negative and $\pi(\Phi)\leq
2$, or $\Phi$ is positive and $\pi(\Phi)\leq 1$.

$\triangleleft$

The class of _geometric implications_ studied by Negri [negri2003contraction]
for the systematic generation of sequent calculus rules from axioms defining
propositional logics is a subset of the tractable formulae. A meta-formula
$\Theta$ is a geometric implication iff $\Theta$ is the universal closure of a
meta-formula of the form $(\Phi_{1}\with...\with\Phi_{m})\Rightarrow(\exists
Y_{1}\Psi_{1}\parr...\parr\exists Y_{n}\Psi_{n})$ such that
$\Psi_{i}:=\Psi_{1}^{i}\with...\with\Psi^{i}_{m_{i}}$, with the $\Psi_{j}^{i}$
meta-atoms for $1\leq j\leq m_{i}$ and $1\leq i\leq n$, and $\Phi_{i}$ meta-
atoms for $1\leq i\leq m$. To see this, observe that geometric implications
are of the form $N\Rightarrow P$ in which $N$ is the conjunction of atoms and
$P$ is the disjunction of (positive) formulae of existentially quantified
conjunctions — that is, formulae of the form $\exists P^{\prime}$, where
$P^{\prime}$ is a conjunction of atoms. Docherty and Pym [Docherty2018,
Docherty2019] have used this notion of meta-formulae to give a uniform account
of proof systems internalizing semantics for the family of bunched logics,
with application to separation logics.

The motivation for tractability is to make a certain step in the generation of
relational calculi possible, as seen in the proof of Proposition 5.9.

######  Definition 5.6 (Tractable Theory, Semantics, Logic).

A set of meta-formulae $\Omega$ is a tractable theory iff $\Omega$ is finite
and any $\Phi\in\Omega$ is a negative tractable meta-sentence. A semantics
$\mathfrak{S}$ is tractable iff it is defined by a tractable theory $\Omega$.
A propositional logic is tractable iff it admits a tractable semantics
$\mathfrak{S}$. $\triangleleft$

######  Example 5.7.

The semantics for modal logic in Example 3.24 is tractable, as witnessed by
the tractable definition in Example 5.3. $\Diamond$

It remains to give an algorithm that generates a relational calculus given a
tractable definition and to prove correctness of that algorithm. Fix a
semantics $\mathfrak{S}:=\langle\mathbb{M},\Vdash\rangle$ with a tractable
definition $\Omega$. Recall that $\Gamma\vDash\Delta$ obtains iff
$\Omega,(x:\Gamma)\vdash_{\mathsf{}}(x:\Delta)$ obtains. The relational
calculus we generate is a meta-sequent calculus $\mathsf{R}$ for the meta-
logic expressive enough to capture all instances
$\Omega,(x:\Gamma)\vdash_{\mathsf{}}(x:\Delta)$ but sufficiently restricted
such that all the meta-connectives and quantifiers may be suppressed.

###  5.2 Generating Relational Calculi

By _generic hereditary reduction_ on a meta-formula $\Phi$ we mean the
indefinite use of reduction operators from $\mathsf{G3c}$ on $\Phi$ and the
generated sub-formulae, until they are meta-atoms, beginning with a meta-
sequent $\Phi,\Pi\triangleright\Sigma$, with generic $\Pi$ and $\Sigma$. For
example, the following is a generic hereditary reduction for $(A\with
B)\parr(C\with D)$ with $A$, $B$, $C$, and $D$ as meta-atoms:

$(A\with B)\parr(C\with D),\Pi\triangleright\Sigma\lx@proof@logical@and(A\with
B),\Pi\triangleright\Sigma A,B,\Pi\triangleright\Sigma(C\with
D),\Pi\triangleright\Sigma C,D,\Pi\triangleright\Sigma$

Such reductions are collapsed into _synthetic_ rules, which is the rule-
relation taking the putative conclusion to the premisses. The above instance
collapses to the following:

$(A\with B)\parr(C\with D),\Pi\triangleright\Sigma\lx@proof@logical@and
A,B,\Pi\triangleright\Sigma C,D,\Pi\triangleright\Sigma$

The quantifier rules have side-conditions in order to be applicable, and we
assert these conditions in the synthetic rule. For example, when using
$\mathsf{\forall_{L}}$ when doing generic hereditary reduction on $\forall
X\Phi$, we require that the term $T$ for which the variable $X$ is substituted
in $\Phi$ is already present in the meta-sequent; for example let
$\Phi:=(A(X)\with B(X))\parr(C(X)\with D(X))$, we have the following synthetic
rule for $\forall X\Phi$ with the side condition that $T$ occurs in either
$\Pi$ or $\Sigma$:

$\forall X(A(X)\with B(X)\parr(C(X)\with
D(X)),\Pi\triangleright\Sigma\lx@proof@logical@and
A(T),B(T),\Pi\triangleright\Sigma C(T),D(T),\Pi\triangleright\Sigma$

######  Definition 5.8 (Sequent Calculus for a Tractable Theory).

Let $\Omega$ be a tractable theory. The sequent calculus
$\mathsf{G3c}(\Omega)$ is composed of
$\mathsf{ax},\bot,\mathsf{\mathsf{c}_{L}}$, $\mathsf{\mathsf{c}_{R}}$, and the
synthetic rules for the meta-formulae in $\Omega$. $\triangleleft$

The tractability condition is designed such that the following holds:

###### Proposition 5.9

Let $\Omega$ be a tractable definition and let $\Pi$ and $\Sigma$ be multisets
of meta-atoms,

$\Omega,\Pi\vdash_{\mathsf{G3c}}\Sigma\qquad\mbox{iff}\qquad\Omega,\Pi\vdash_{\mathsf{\mathsf{G3c}(\Omega)}}\Sigma$

###### Proof.

Assume $\Omega,\Pi\vdash_{\mathsf{G3c}}\Sigma$. Without loss of generality
(see, for example, Liang and Miller [LIANG20094747] and Marin [Marin2022]),
there is a focused
$\mathsf{G3c}+\mathsf{\mathsf{c}_{R}}+\mathsf{\mathsf{c}_{L}}$-proof
$\mathcal{D}$ of $\Omega,\Pi\triangleright\Sigma$. We can assume that
$\mathcal{D}$ is _focused_ up to possibly using instance of $\mathsf{c_{L}}$
or $\mathsf{c_{R}}$. That is, $\mathcal{D}$ is structured by sections of
alternating phases of the following kind:

  * -

an instance of $\mathsf{c_{L}}$ or $\mathsf{c_{R}}$

  * -

hereditary reduction on positive meta-formulae on the right and negative meta-
formulae on the left

  * -

eager reduction on negative meta-formulae on the right and positive meta-
formulae on the left.

Since $\Pi$ and $\Sigma$ are composed of meta-atoms and $\Omega$ is composed
of negative meta-formulae, $\mathcal{D}$ begins by a contraction and then
hereditary reducing on some $\Phi\in\Omega$. Since $\Phi$ is tractable, this
section in $\mathcal{D}$ may be replaced by the synthetic rule for $\Phi$.
Doing this to all the phases in $\mathcal{D}$ yields a tree of sequents
$\mathcal{D}^{\prime}$ which is a
$\Omega,\Pi\vdash_{\mathsf{\mathsf{G3c}(\Omega)}}\Sigma$.

Assume $\Omega,\Pi\vdash_{\mathsf{\mathsf{G3c}(\Omega)}}\Sigma$. Since all the
rules in $\mathsf{G3c}(\Omega)$ are admissible in $\mathsf{G3c}$, we
immediately have $\Omega,\Pi\vdash_{\mathsf{\mathsf{G3c}}}\Sigma$. ∎

######  Example 5.10.

Consider the tractable theory $\Omega_{\mathfrak{K}}$ in Example 5.3. The
sequent calculus $\mathsf{G3c}(\Omega_{\mathfrak{K}})$ contains, among other
things, the following rules corresponding to the clause for $\land$ in Figure
6 in which $w$, $\phi$, and $\psi$ already occur in $\Omega$, $\Pi$, or
$\Sigma$:

$\Omega,\Pi\triangleright\Sigma\lx@proof@logical@and\Omega,\Pi\triangleright\Sigma,(w:\phi\land\psi)\Omega,(w:\phi),(w:\psi),\Pi\triangleright\Sigma$
$\Omega,\Pi\triangleright\Sigma\lx@proof@logical@and\Omega,\Pi,(w:\phi\land\psi)\triangleright\Sigma\Omega,\Pi\triangleright\Sigma,(w:\phi)\Omega,\Pi\triangleright\Sigma,(w:\psi)$

In practice, one does not use the rules in this format. Rather, one would only
apply the rules if one already knew that the left-branch would terminate; that
is, one uses the following:

$\Omega,(w:\phi\land\psi),\Pi\triangleright\Sigma\Omega,(w:\phi),(w:\psi),(w:\phi\land\psi),\Pi\triangleright\Sigma$
$\Omega,\Pi\triangleright\Sigma,(w:\phi\land\psi)\lx@proof@logical@and\Omega,\Pi\triangleright\Sigma,(w:\phi\land\psi),(w:\phi)\Omega,\Pi\triangleright\Sigma,(w:\phi\land\psi),(w:\psi)$

This simplification can be made systematically according to the shape of the
meta-formula generating the rules; it corresponds to _forward-chaining_ and
_back-chaining_ in the proof-theoretic analysis of the meta-formula — see, for
example, Marin et al.[Marin2022].

One desires a systematic account of the transformation of rules of arbitrary
shape into rules of other (more desirable) shape. This remains to be
considered in the context of relational calculi and demands further analysis
on the structure of $\Omega$. Some results of such transformations for
arbitrary sequent calculi have been provided by Indrzejczak
[indrzejczak2021sequents]. $\Diamond$

The calculus $\mathsf{G3c}(\Omega)$ is a restriction of $\mathsf{G3c}$
precisely encapsulating the proof-theoretic behaviours of the meta-formulae in
$\Omega$. It remains to suppress the logical constants of the meta-logic
entirely, and thereby yield a relational calculus expressed as a labelled
sequent calculus for the propositional logic.

######  Definition 5.11 (Relational Calculus for a Tractable Theory).

Let $\Omega$ be a tractable theory. The relational calculus for $\Omega$ is
the sequent calculus $\mathsf{R}(\Omega)$ that results from
$\mathsf{G3c}(\Omega)$ by suppressing $\Omega$. $\triangleleft$

######  Theorem 5.12 (Soundness & Completeness)

Let $\mathfrak{S}$ be a tractable semantics and let $\Omega$ be a tractable
definition for $\mathfrak{S}$.

$\Gamma\vDash_{\mathfrak{S}}\Delta\qquad\mbox{iff}\qquad(x:\Gamma)\vdash_{\mathsf{R(\Omega)}}(x:\Delta)$

###### Proof.

We have the following:

$\begin{array}[]{cclr}\Gamma\vDash_{\mathfrak{S}}\Delta&\qquad\mbox{iff}&\Omega,(x:\Gamma)\vdash_{\mathsf{}}(x:\Delta)&\qquad\mbox{(Definition~{}\ref{def:tractable:theory})}\\\
&\qquad\mbox{iff}&\Omega,(x:\Gamma)\vdash_{\mathsf{G3c}}(x:\Delta)&\qquad\mbox{(Proposition~{}\ref{lem:snc:G3c})}\\\
&\qquad\mbox{iff}&\Omega,(x:\Gamma)\vdash_{\mathsf{G3c(\Omega)}}(x:\Delta)&\qquad\mbox{(Proposition~{}\ref{lem:calculus:tractable})}\end{array}$

It remains to show that
$\Omega,(x:\Gamma)\vdash_{\mathsf{G3c(\Omega)}}(x:\Delta)$ iff
$(x:\Gamma)\vdash_{\mathsf{R(\Omega)}}(x:\Delta)$.

Let $\mathcal{D}$ be a $\mathsf{G3c}(\Omega)$-proof of
$\Omega,(x:\Gamma)\triangleright(x:\Delta)$, and let $\mathcal{D}^{\prime}$ be
the result of removing $\Omega$ from every meta-sequent in $\mathcal{D}$. By
Definition 5.11, we have that $\mathcal{D}^{\prime}$ is a
$\mathsf{R}(\Omega)$-proof of $(x:\Gamma)\triangleright(x:\Delta)$. Thus,
$\Omega,(x:\Gamma)\vdash_{\mathsf{G3c(\Omega)}}(x:\Delta)$ implies
$(x:\Gamma)\vdash_{\mathsf{R(\Omega)}}(x:\Delta)$.

Let $\mathcal{D}$ be a $\mathsf{R}(\Omega)$-proof of
$(x:\Gamma)\triangleright(x:\Delta)$, and let $\mathcal{D}^{\prime}$ be the
result of putting $\Omega$ in every meta-sequent in $\mathcal{D}$. By
Definition 5.11, we have that $\mathcal{D}^{\prime}$ is a
$\mathsf{G3c}(\Omega)$-proof of $\Omega,(x:\Gamma)\triangleright(x:\Delta)$.
Thus, $(x:\Gamma)\vdash_{\mathsf{R(\Omega)}}(x:\Delta)$ implies
$\Omega,(x:\Gamma)\vdash_{\mathsf{G3c(\Omega)}}(x:\Delta)$. ∎

######  Example 5.13.

The sequent calculus in Example 5.10 becomes a relational calculus
$\mathsf{R}(\Omega_{\mathfrak{K}})$ by suppressing $\Omega$ in the rules; for
example,

$\Omega,\Pi\triangleright\Sigma\lx@proof@logical@and\Omega,\Pi\triangleright\Sigma,(w:\phi\land\psi)\Omega,(w:\phi),(w:\psi),\Pi\triangleright\Sigma$

becomes

$\Pi\triangleright\Sigma\lx@proof@logical@and\Pi\triangleright\Sigma,(w:\phi\land\psi)(w:\phi),(w:\psi),\Pi\triangleright\Sigma$

Abbreviating $\neg\Box\neg\phi$ by $\Diamond\phi$ and doing some proof-
theoretic analysis on $\mathsf{R}(\Omega_{\mathfrak{K}})$, we have the
simplified system $\mathsf{RK}$ in Figure 7 — $\Phi$ denotes a meta-formula,
$\Pi$ and $\Sigma$ denote multiset of meta-formulae, $x$ and $y$ denote world-
variables, $\Delta$ denotes object-logic data, $\phi$ and $\psi$ denote
object-logic formulae. This is, essentially, the relational calculus for $K$
introduced by Negri [Negri2005]. $\Diamond$

$\begin{array}[]{cc}\Phi,\Pi\triangleright\Sigma,\Phi&\bot,\Pi\triangleright\Sigma\\\\[6.45831pt]
(x:\phi\land\psi),\Pi\triangleright\Sigma(x:\phi),(x:\psi),\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,(x:\phi\land\psi)\lx@proof@logical@and\Pi\triangleright\Sigma,(x:\phi)\Pi\triangleright\Sigma,(x:\psi)\\\\[6.45831pt]
(x:\phi\lor\psi),\Pi\triangleright\Sigma\lx@proof@logical@and(x:\phi),\Pi\triangleright\Sigma(x:\psi),\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,(x:\phi\lor\psi)\Pi\triangleright\Sigma,(x:\phi),(x:\psi)\\\\[6.45831pt]
(x:\Box\phi),xRy,\Pi\triangleright\Sigma(y:\phi),(x:\Box\phi),xRy,\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,(x:\Box\phi)xRy,\Pi\triangleright\Sigma,(y:\phi)\\\\[6.45831pt]
(x:\Diamond\phi),\Pi\triangleright\Sigma
xRy,(y:\phi),\Pi\triangleright\Sigma&xRy,\Pi\triangleright\Sigma,(x:\Diamond\phi)xRy,\Pi\triangleright\Sigma,(x:\Diamond\phi),(y:\phi)\\\\[6.45831pt]
(x:\bot),\Pi\triangleright\Sigma\bot,\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,(x:\bot)\bot,\Pi\triangleright\Sigma,\bot\\\\[6.45831pt]
(x:\Gamma\fatcomma\Gamma^{\prime}),\Pi\triangleright\Sigma(x:\Gamma),(x:\Gamma^{\prime}),\Pi\triangleright\Sigma&\Pi\triangleright\Sigma,(x:\Delta\fatsemi\Delta^{\prime})\Pi\triangleright\Sigma,(x:\Delta),(x:\Delta^{\prime})\end{array}$

Figure 7: Relational Calculus $\mathsf{RK}$

While we have effectively transformed (tractable) semantics into relational
calculi, giving a general, uniform, and systematic proof theory to an ample
space of logics, significant analysis remains to be done. In Example 5.13, we
showed that under relatively mild conditions, one expects the relational
calculus to have a particularly good shape. This begs for further
characterization of the definitions of semantics and what properties one may
expect the resulting relational calculus to have; the beginnings of such an
analysis are given below Definition 5.2 in which we require $\Omega$ to
contain a first-order definition of frames together with an inductive
definition of the semantics.

We have presented a general account of relational calculi, but certain
specific families of logics ought to be studied in particular. For example,
Negri [Negri2005] demonstrated that relational calculi for modal logics are
particularly simple. An adjacent class is the family of hybrid logics — see,
for example, Blackburn et al. [Blackburn2001, blackburn1995hybrid], Areces and
ten Cate [Areces], Bräuner [brauner2001hybrid], and Indrzejczak
[indrzejczak2011natural]. Indeed, one may regard the meta-logics for
propositional logics (i.e., the fused language) as hybrid logics — see, for
example, Blackburn [blackburn2000].

###  5.3 Faithfulness & Adequacy

In this section, we give sufficient conditions for faithfulness and adequacy
of a relational calculus with respect to a sequent calculus. More precisely,
we give conditions under which one may transform a relational calculus into a
sequent calculus for the object-logic. The result is immediate proof of
soundness and completeness for the sequent calculus concerning the semantics;
significantly, it bypasses term- or counter-model construction. This idea has
already been implemented for the logic of Bunched Implications by Gheorghiu
and Pym [Alex:BI_Semantics].

While the work of the preceding section generates a relational calculus, one
may require some proof theory to yield a relational calculus that meets the
conditions in this section faithfulness and adequacy. Likewise, one may
require proof theory on the generated sequent calculus to yield a sequent
calculus one recognizes as sound and complete concerning a logic of interest.
We do not consider these problems here, but they are addressed explicitly for
BI in the previous work by the authors.

Our objective is to systematically transform (co-)inferences in the relational
calculus into (co-)inferences of the propositional logic. Regarded as
constraint systems, relational calculi do not have any side-conditions on
inferences; instead, all of the constraints are carried within sequents. Thus
we do not need to worry about assignments and aim only to develop a valuation
$\nu$. We shall define $\nu$ by its action on sequents and extend it to
reductions like in Section 4.3.

Fix a propositional logic $\vdash_{\mathsf{}}$ and relational calculus
$\mathsf{R}$. We assume the propositional logic has data-constructors $\circ$
and $\bullet$ such that

$\Gamma\circ\Gamma^{\prime}\vdash_{\mathsf{}}\Delta$ iff
$(w:\Gamma)\with(w:\Gamma^{\prime})\vdash_{\mathsf{R}}(w:\Delta)$

and

$\Gamma\vdash_{\mathsf{}}\Delta\bullet\Delta^{\prime}$ iff
$(w:\Gamma)\vdash_{\mathsf{R}}(w:\Delta)\parr(w:\Delta^{\prime})$

This means that the weakening, contraction, and exchange structural rules are
admissible for $\circ$ and $\bullet$ on the left and right, respectively. In
particular, these data-constructors behave like classical conjunction and
disjunction, respectively.

######  Example 5.14.

The logic with relational calculus $\mathsf{RK}$ satisfies the data-
constructor condition — specifically, is conjunctive and $\fatsemi$ is
disjunctive. $\Diamond$

A list of meta-formulae is _monomundic_ iff it only contains one world-
variable (but possibly many occurrences of that world-variable; we write
$\Pi^{w}$ or $\Sigma^{w}$ to denote monomundic lists contain the world-
variable $w$. A monomundic list is _basic_ iff it only contains meta-atoms of
the form $(w:\Gamma)$, which is denoted $\bar{\Pi}^{w}$ or $\bar{\Sigma}^{w}$.

######  Definition 5.15 (Basic Validity Sequent).

A basic validity sequent (BVS) is a pair of basic monomundic lists,
$\bar{\Pi}^{w}\triangleright\bar{\Sigma}^{w}$. $\triangleleft$

######  Definition 5.16 (Basic Rule).

A rule in a relational calculus is basic iff it is a rule over BVSs — that is,
it has the following form:

$\bar{\Pi}^{w}\triangleright\Sigma^{w}\lx@proof<EMAIL_ADDRESS>
$\triangleleft$

######  Definition 5.17 (Basic Relational Calculus).

A relational calculus $\mathsf{r}$ is basic iff it is composed of basic rules.
$\triangleleft$

Using the data-structures $\bullet$ and $\circ$, a BVS intuitively corresponds
to a sequent in the propositional logic. Define $\lfloor-\rfloor_{\circ}$ and
$\lfloor-\rfloor_{\bullet}$ on basic monomundic lists as follows:

$\lfloor(w:\Gamma_{1}),...,(w:\Gamma_{m})\rfloor_{\circ}:=\Gamma_{1}\circ...\circ\Gamma_{m}\qquad\lfloor(w:\Delta_{1}),...,(w:\Delta_{n})\rfloor_{\bullet}:=\Delta_{1}\bullet...\bullet\Delta_{n}$

We can define $\nu$ on BVSs by this encoding,

$\nu(\bar{\Pi}^{w}\triangleright\bar{\Sigma}^{w}):=\lfloor\bar{\Pi}^{w}\rfloor\triangleright\lfloor\bar{\Sigma}^{w}\rfloor$

The significance is that whatever inference is made in the semantics using
BVSs immediately yields an inference it terms of propositional sequents.

Let $\mathsf{r}$ be a basic rule, its propositional encoding $\nu(\mathsf{r})$
is the following:

$\nu(\bar{\Pi}^{w}\triangleright\Sigma^{w})\lx@proof@logical@and\nu(\bar{\Pi}_{1}^{w_{1}}\triangleright\Sigma_{1}^{w_{1}})...\nu(\bar{\Pi}_{n}^{w_{n}}\triangleright\Sigma_{n}^{w_{n}})$

This extends to basic relational calculi pointwise,

$\nu(\mathsf{R}):=\\{\nu(\mathsf{r})\mid\mathsf{r}\in\mathsf{R}\\}$

Despite their restrictive shape, basic rules are quite typical. For example,
if the body of a clause is composed of only conjunctions and disjunctions of
assertions, the rules generated by the algorithm presented above will be
basic. Sets of basic rules can sometimes replace more complex rules in
relational calculi to yield a basic relational calculus from a non-basic
relational calculus — see Section 6 for an example.

We are thus in a situation where the rules of a reduction system intuitively
correspond to the rules of a sequent calculus. The formal statement of this is
below.

###### Theorem 5.18

A basic relational calculus $\mathsf{R}$ is faithful and adequate with respect
to its propositional encoding $\nu(\mathsf{R})$.

###### Proof.

The result follows by Definition 4.15 because a valuation of an instance of a
rule in $\mathsf{R}$ corresponds to an instance of a rule of $\mathsf{R}$ on
the states of the sequents involved.

Faithfulness follows by application of $\nu$ on $\mathsf{R}$-proofs. That is,
for any $\mathsf{R}$-reduction $\mathcal{D}$, one produces a corresponding
$\nu(\mathcal{R})$-proof by apply $\nu$ to each sequent in $\mathcal{D}$.

Adequacy follows by introducing arbitrary world-variables into a
$\nu(\mathsf{R})$-proof. Let $\mathcal{D}$ be a $\nu(\mathsf{R})$-proof, it
concludes by an inference of the following form:

$\nu(\bar{\Pi}^{w}\triangleright\Sigma^{w})\lx@proof@logical@and\nu(\bar{\Pi}_{1}^{w_{1}}\triangleright\Sigma_{1}^{w_{1}})\mathcal{D}_{1}...\nu(\bar{\Pi}_{n}^{w_{n}}\triangleright\Sigma_{n}^{w_{n}})\mathcal{D}_{n}$

We can co-inductively define a corresponding $\mathsf{R}$-with the following
co-recursive step in which $\mathcal{R}_{i}$ is the reduction corresponding to
$\mathcal{D}_{i}$:

$\bar{\Pi}^{w}\triangleright\Sigma^{w}\lx@proof<EMAIL_ADDRESS>
Hence, for any $\nu(\mathsf{R})$-proof, there is a $\mathsf{R}$-reduction
$\mathcal{R}$ such that $\nu(\mathcal{R})=\mathcal{D}$, as required. ∎

Of course, despite basic rules being relatively typical, many relational
calculi are not comprised of _only_ basic rules. Nonetheless, the phenomenon
does occur for even quite complex logic. It can be used for the semantical
analysis of that logic in those instances — see, for example, Gheorghiu and
Pym [Alex:BI_Semantics] for an example of this in the case of the logic of
Bunched Implications. Significantly, this approach to soundness and
completeness differs from the standard term-model approach and has the
advantage of bypassing truth-in-a-model (i.e., satisfaction).

##  6 Example: Intuitionistic Propositional Logic

In Section 5, we gave a general, uniform, and systematic procedure for
generating proof systems for logics that have model-theoretic semantics
satisfying certain conditions. What about the reverse problem? That is, given
a proof-theoretic characterization of a propositional logic, can we _derive_ a
model-theoretic semantics for it (in the sense of Section 3.2)? This chapter
provides an example of this for intuitionistic propositional logic (IPL).

We begin from a naive position on IPL. Our _definition_ of IPL is by
$\mathsf{LJ}$ — see Gentzen [Gentzen1969]. We choose this over other systems
(e.g., $\mathsf{G3i}$ — see Troelstra and Schwichtenberg [troelstra2000basic])
because we assume that we do not even known much about its proof theory so
that we may explain through the analysis what we require. In the end, we
recover the model-theoretic semantics by Kripke [Kripke1963] using constraint
systems as the enabling technology. Of course, for the purposes of this
chapter we shall imagine that we do not know about the semantics.

Reflecting on Section 5, we expect that the semantics we synthesize for IPL
will be tractable. Therefore, we intend to build a relational calculus to
bridge the proof theory and semantics of IPL as in Section 5, but this time we
build it from the proof theory side. Recall that relational calculi are
fragments of proof systems for FOL (i.e., the meta-logic); therefore, we begin
in Section 6.1 by building a constraint system for IPL that is _classical_ in
shape. The system is derived in a principled way from this desire, but it is
only sound and complete for IPL. We require it to be _faithful_ and _adequate_
for $\mathsf{LJ}$ because we hope to generate clause governing each connective
from its rules. Hence, in Section 6.2, we analyse the constraint system to
recover a faithful and adequate constraint system for IPL. In Section 6.3, we
study the reductive behaviour of connectives of IPL in this constraint systems
and write tractable FOL-formulae that capture the same behaviour in
$\mathsf{G3c}$. The resulting theory $\Omega$ determines a model-theoretic
semantics for IPL, as shown in Section 6.4.

###  6.1 Multiple-conclusions via Boolean Constraints

We begin by defining IPL naively — that is, from $\mathsf{LJ}$ (see Gentnzen
[Gentzen1969]). We do it in the style of Section 3.2 to keep it consistent
with the treatment of propositional logics in the rest of this paper.

######  Definition 6.1 (Alphabet $\mathscr{J}$).

The alphabet is
$\mathscr{J}:=\langle\mathbb{P},\\{\land,\lor,\to,\neg\\},\\{\fatcomma,\fatsemi,\varnothing\\}\rangle$,
in which symbols $\land,\lor,\to,\fatcomma,\fatsemi$ have arity $2$, the
symbol $\neg$ has arity $1$, and $\varnothing$ has arity $0$. $\triangleleft$

Let $\equiv$ be the smallest relation satisfying commutative monoid equations
for and $\fatsemi$ with unit $\varnothing$.

######  Definition 6.2 (System $\mathsf{LJ}$).

Sequent calculus $\mathsf{LJ}$ is comprised of the rules in Figure 8, in which
$\Delta$ is either a $\mathscr{J}$-formula $\phi$ or $\varnothing$, and
$\Gamma\equiv\Gamma^{\prime}$ and $\Delta\equiv\Delta^{\prime}$ in
$\mathsf{e}$. $\triangleleft$

$\begin{array}[]{c}\phi\fatcomma\Gamma\triangleright\Delta\Gamma\triangleright\Delta\quad\Gamma\triangleright\phi\Gamma\triangleright\varnothing\quad\phi\fatcomma\Gamma\triangleright\Delta\phi\fatcomma\phi\fatcomma\Gamma\triangleright\Delta\quad\Gamma\triangleright\Delta\Gamma^{\prime}\triangleright\Delta^{\prime}\\\\[6.45831pt]
\Gamma\triangleright\phi\land\psi\lx@proof<EMAIL_ADDRESS>\phi\lor\psi\fatcomma\Gamma\triangleright\Delta\lx@proof<EMAIL_ADDRESS>\Gamma\triangleright\phi\to\psi\phi\fatcomma\Gamma\triangleright\psi\quad\phi\to\psi\fatcomma\Gamma_{1}\fatcomma\Gamma_{2}\triangleright\Delta\lx@proof@logical@and\Gamma_{1}\triangleright\phi\psi\fatcomma\Gamma_{2}\triangleright\Delta\quad\phi\triangleright\phi\end{array}$

Figure 8: Sequent Calculus $\mathsf{LJ}$

In this section, $\mathsf{LJ}$-provability $\vdash_{\mathsf{LJ}}$ _defines_
the judgment relation for IPL. Our task is to derive a model-theoretic
characterization of IPL. As we saw in Section 5, the logic in which semantics
is defined is classical. Therefore, our strategy is to use the constraint to
present IPL in a sequent calculus with a classical shape; that is, the
constraint informs precisely where the semantics of IPL diverge from those of
FOL. This tells us how the semantic clauses of FOL need to be augmented to
define the connectives of IPL. The calculus in question is Gentzen’s
$\mathsf{LK}$ [Gentzen1969].

The essential point of distinction between $\mathsf{LJ}$ and $\mathsf{LK}$ is
in $\mathsf{c_{R}}$, $\mathsf{\to_{L}}$, and $\mathsf{\neg_{L}}$ as it is
these rules that enable multiple-conclusioned sequents to appear in the latter
but not the former. To bring these behaviours closer, we introduce a
constraints constraint system for IPL whose combinatorial behaviour is like
$\mathsf{LK}$, but for which we have constraints to recover $\mathsf{LJ}$.

The algebra of the constraint system is Boolean algebra — see Section 2.

######  Example 6.3.

The following is an enriched $\mathscr{J}$-sequent.

$(\Gamma\cdot 1)\fatcomma(\phi\cdot
x)\triangleright(\Delta\cdot\bar{x})\fatsemi(\psi\cdot x)$

$\Diamond$

For the rules that are the same across both systems, the expressions are
inherited from the justifying sub-formulae of the conclusion; for example, in
the case of conjunction, one has the following:

$\Gamma\triangleright\phi\land\psi\lx@proof<EMAIL_ADDRESS>becomes }\quad\Gamma\triangleright\Delta\fatsemi(\phi\land\psi\cdot
x)\lx@proof@logical@and\Gamma\triangleright\Delta\fatsemi(\phi\cdot
x)\Gamma\triangleright\Delta\fatsemi(\psi\cdot x)$

For readability, we may suppress the Boolean expressions on these rules.

######  Definition 6.4 (System $\mathsf{LK}\oplus\mathcal{B}$).

Sequent calculus $\mathsf{LK}\oplus\mathcal{B}$ is comprised of the rules in
Figure 9, in which $\Gamma$ and $\Delta$ are enriched $\mathscr{J}$-datum, and
$\Gamma\equiv\Gamma^{\prime}$ and $\Delta\equiv\Delta^{\prime}$ in
$\mathsf{e}^{\mathcal{B}}$. $\triangleleft$

$\begin{array}[]{c}\phi\fatcomma\Gamma\triangleright\Delta\Gamma\triangleright\Delta\quad\Gamma\triangleright\Delta\fatcomma\phi\Gamma\triangleright\Delta\quad\phi\fatcomma\Gamma\triangleright\Delta\phi\fatcomma\phi\fatcomma\Gamma\triangleright\Delta\quad\Gamma\triangleright\Delta\fatsemi\phi\Gamma\triangleright\Delta\fatsemi\phi\cdot
x\fatsemi\phi\cdot\bar{x}\\\\[6.45831pt]
\Gamma\triangleright\Delta\Gamma^{\prime}\triangleright\Delta^{\prime}\qquad\phi\cdot
x\triangleright\phi\cdot
yx=y=1\qquad\neg\phi\fatcomma\Gamma\triangleright\Delta\Gamma\triangleright\Delta\cdot\bar{x}\fatcomma\phi\cdot
x\qquad\Gamma\triangleright\Delta\fatsemi\neg\phi\phi\fatcomma\Gamma\triangleright\Delta\end{array}$

$\begin{array}[]{c@{\qquad}c}\Gamma\triangleright\Delta\fatsemi\phi\land\psi\lx@proof<EMAIL_ADDRESS>\phi\lor\psi\fatcomma\Gamma\triangleright\Delta\lx@proof<EMAIL_ADDRESS>\Gamma\triangleright\Delta\fatsemi\phi\to\psi\phi\fatcomma\Gamma\triangleright\Delta\fatsemi\psi&\phi\to\psi\fatcomma\Gamma_{1}\fatcomma\Gamma_{2}\triangleright\Delta_{1}\fatsemi\Delta_{2}\lx@proof@logical@and\Gamma_{1}\triangleright\Delta_{1}\cdot\bar{x}\fatcomma\phi\cdot
x\psi\fatcomma\Gamma_{2}\triangleright\Delta_{2}\end{array}$

Figure 9: Constraint System $\mathsf{LK}\oplus\mathcal{B}$

The ergo rendering $\mathsf{LK}\oplus\mathcal{B}$ sound and complete for IPL
is precisely the demand for one to choose which of the formulae in the
succedent of a sequent to assert as a consequence of the context. This reading
is closely related to the semantics of intuitionistic proof-search provided by
Pym and Ritter [Pym2005games].

######  Definition 6.5 (Choice Ergo).

Let $I:X\to\mathcal{B}$ be an interpretation of the language of the Boolean
algebra. The choice ergo is the function $\sigma_{I}$ which acts on
$\mathscr{J}$-formulae as follows:

$\sigma_{I}(\phi)\mapsto\cases{\phi}&\text{if}\phi\text{unlabelled}\\\
\sigma_{I}(\psi)\text{if}I(x)=1\text{and}\phi=\psi\cdot x\\\
\varnothing\text{if}I(x)=0\text{and}\phi=\psi\cdot x$

The choice ergo acts on enriched $\mathscr{J}$-data by acting point-wise on
the formulae; and it acts on enriched sequents by acting on each component
independently — that is,
$\sigma_{I}(\Gamma\triangleright\Delta)=\sigma_{I}(\Gamma)\triangleright\sigma_{I}(\Delta)$.
$\triangleleft$

######  Example 6.6.

Let $S$ be the sequent in Example 6.3. If $I(x)=1$, then
$\sigma_{I}(S)=\Gamma\fatcomma\phi\triangleright\psi$ $\Diamond$

###### Proposition 6.7

System $\mathsf{LK}\oplus\mathcal{B}$, with the choice ergo $\sigma$, is sound
and complete for IPL,

$\Gamma\vdash_{\mathsf{LK}\oplus\mathcal{B}}^{\sigma}\Delta\qquad\mbox{iff}\qquad\Gamma\vdash_{\mathsf{LJ}}\Delta$

###### Proof of Soundness.

Suppose $\Gamma\vdash_{\mathsf{LK}\oplus\mathcal{B}}^{\sigma}\Delta$, then
there is a coherent $\mathsf{LK}\oplus\mathcal{B}$-reduction $\mathcal{R}$ of
an enriched sequent $S$ such that $\sigma_{I}(S):=\Gamma\triangleright\Delta$,
where $I$ is any assignment satisfying $\mathcal{R}$. It follows that $S$ is
equivalent (up to exchange) to the sequent
$\Gamma^{\prime}\fatcomma\Pi\triangleright\Sigma\fatsemi\Delta^{\prime}$ in
which $\Gamma^{\prime}$ and $\Delta^{\prime}$ are like $\Gamma$ and $\Delta$
but with labelled data and $I$ applied to the expressions in $\Pi$ and
$\Sigma$ evaluates to $0$ but applied to expressions in $\Gamma^{\prime}$ and
$\Delta^{\prime}$ evaluates to $1$. We proceed by induction $n$ on the height
of $\mathcal{R}$ — that is, the maximal number of reductive inferences in a
branch of the tree.

Base Case. If $n=1$, then
$\Gamma^{\prime},\Pi\triangleright\Sigma,\Delta^{\prime}$ is an instances of
$\mathsf{ax}^{\mathcal{B}}$. But then $S=\phi\cdot x\triangleright\phi\cdot
y$, for some formula $\phi$. We have $\phi\vdash_{\mathsf{LJ}}\phi$ by
$\mathsf{ax}$.

Inductive Step. The induction hypothesis (IH) is as follows: if
$\Gamma^{\prime}\vdash_{\mathsf{LK}\oplus\mathcal{B}}^{\sigma}\Delta^{\prime}$
is witnessed by $\mathsf{LK}\oplus\mathcal{B}$-reductions of $k\leq n$, then
$\Gamma\vdash_{\mathsf{LJ}}\Delta$.

Suppose that the shortest reduction witnessing
$\Gamma^{\prime}\vdash_{\mathsf{LK}\oplus\mathcal{B}}^{\sigma}\Delta^{\prime}$
is of height $n+1$. Let $\mathcal{R}$ be such a reduction. Without loss of
generality, we assume the root of $\mathcal{R}$ is of the form
$\Gamma^{\prime}\fatcomma\Pi\triangleright\Sigma\fatsemi\Delta^{\prime}$, as
above. It follows by case analysis on the final inferences of $\mathcal{R}$
(i.e., reductive inferences applied to the root) that
$\Gamma\vdash_{\mathsf{LJ}}\Delta$. We show two cases, the rest being similar.

  * -

Suppose the last inference of $\mathcal{R}$ was by
$\mathsf{c_{R}}^{\mathcal{B}}$. In this case, $\mathcal{R}$ has an immediate
sub-tree $\mathcal{R}^{\prime}$ that is a coherent
$\mathsf{LK}\oplus\mathcal{B}$-reduction of either
$\Gamma^{\prime}\fatcomma\Sigma\triangleright\Sigma^{\prime}\fatsemi\Delta^{\prime}$
or
$\Gamma^{\prime}\fatcomma\Sigma\triangleright\Sigma^{\prime}\fatsemi\Delta^{\prime\prime}$,
in which $\Sigma^{\prime}$ and $\Delta^{\prime\prime}$ are like $\Sigma$ and
$\Delta^{\prime}$, respectively, but with some formula repeated such that one
occurrence carries an additional expression $x$ and the other occurrence with
an $\bar{x}$. The coherent assignment of $\mathcal{R}$ are the same as those
$\mathcal{R}^{\prime}$ since the two reductions have the same constraints. We
observe that under these coherent assignment $\mathcal{R}^{\prime}$ witnesses
$\Gamma^{\prime}\vdash_{\mathsf{LK}\oplus\mathcal{B}}^{\sigma}\Delta^{\prime}$.
By the IH, since $\mathcal{R}^{\prime}$ is of height $n$, it follows that
$\Gamma\vdash_{\mathsf{LJ}}\Delta$.

  * -

Suppose the last inference of $\mathcal{R}$ was by
$\mathsf{\to_{R}}^{\mathcal{B}}$. In this case, $\mathcal{R}$ has an immediate
sub-tree $\mathcal{R}^{\prime}$. If the principal formula of the inference is
not in $\Delta^{\prime}$, then $\mathcal{R}^{\prime}$ witnesses
$\Gamma^{\prime}\vdash_{\mathsf{LK}\oplus\mathcal{B}}^{\sigma}\Delta^{\prime}$.
Hence, by the IH, we conclude $\Gamma\vdash_{\mathsf{LJ}}\Delta$. If the
principal formula of the inference is in $\Delta^{\prime}$, then
$\mathcal{R}^{\prime}$ is a proof of
$\phi\fatcomma\Gamma^{\prime}\fatcomma\Pi\triangleright\Sigma\fatsemi\Delta^{\prime\prime}\fatsemi\psi$,
where $\Delta^{\prime}:=\Delta^{\prime\prime}\fatsemi\phi\to\psi$. It follows,
by the IH, that
$\phi,\Gamma^{\prime}\vdash_{\mathsf{LJ}}\Delta^{\prime\prime}\fatsemi\psi$.
By the $\mathsf{\to_{R}}$-rule in $\mathsf{LJ}$, we have
$\Gamma\vdash_{\mathsf{LJ}}\phi\to\psi$ — that is,
$\Gamma\vdash_{\mathsf{LJ}}\Delta$, as required.

Of course, since we are working with $\mathsf{LJ}$, we know that $\Delta$
contains only one formula. This distinction was not important for the proof,
so we have left with the more general notation. ∎

###### Proof of Completeness.

This follows immediately from the fact that all the rules of $\mathsf{LJ}$ may
be simulated in $\mathsf{LK}\oplus\mathcal{B}$. ∎

The point of this work is that $\mathsf{LK}\oplus\mathcal{B}$ characterizes
IPL in a way that is combinatorially comparable to FOL. This is significant as
the semantics of IPL is given classically, hence
$\mathsf{LK}\oplus\mathcal{B}$ bridges the proof-theoretic and model-theoretic
characterizations of IPL.

###  6.2 Faithfulness & Adequacy

Though we may use $\mathsf{LK}\oplus\mathcal{B}$ to reason about IPL with
classical combinatorics, the system does not immediately reveal the meaning of
the connectives of IPL in terms of their counterparts in FOL. The problem is
that $\mathsf{LK}\oplus\mathcal{B}$-proofs are only _globally_ valid for IPL,
with respect to the choice ergo $\sigma$. Therefore, to conduct a semantical
analysis of IPL in terms of FOL, we require a constraint system based on FOL
whose proofs are _locally_ valid — that is, a system which is not only sound
and complete for IPL, but _faithful_ and _adequate_. In this section, we
analyze the relationship between $\mathsf{LK}\oplus\mathcal{B}$ and
$\mathsf{LJ}$ to produce such a system.

A significant difference between $\mathsf{LK}$ and $\mathsf{LJ}$ is the use of
richer data-structures for the succedent in the former than in the latter
(i.e., list or multisets verses formulae). Intuitively, the data-constructor
in the succedent acts as a meta-level disjunction, thus we may investigate how
$\mathsf{LK}\oplus\mathcal{B}$ captures IPL by considering how
$\mathsf{\mathsf{c}^{\mathcal{B}}_{R}}$ interacts with
$\mathsf{\lor^{\mathcal{B}}_{R}}$. We may restrict attention to interactions
of the following form:

$\Gamma\triangleright\Delta\fatsemi\phi\lor\psi\Gamma\triangleright\Delta\fatsemi(\phi\lor\psi\cdot
x)\fatsemi(\phi\lor\psi\cdot\bar{x})\Gamma\triangleright\Delta\fatsemi(\phi\cdot
x)\fatsemi(\phi\lor\psi\cdot\bar{x})\Gamma\triangleright\Delta\fatsemi(\phi\cdot
x)\fatsemi(\psi\cdot\bar{x})$

These may be collapsed into single inference rules,

$\Gamma\triangleright\phi\lor\psi\cdot
x\fatcomma\Delta\Gamma\triangleright\phi\cdot xy\fatsemi\psi\cdot
x\bar{y}\fatsemi\Delta$

The other connectives either make use of constraints, and therefore have no
significant interaction with disjunction, or simply can be permuted without
loss of generality — for example, a typical interaction between
$\mathsf{\mathsf{c}^{\mathcal{B}}_{R}}$ and
$\mathsf{\land^{\mathcal{B}}_{R}}$,

$\Gamma\triangleright\Delta_{1}\fatsemi\Delta_{2}\fatsemi\Delta_{3}\fatsemi\phi\land\psi\Gamma\triangleright\Delta_{1}\fatsemi\Delta_{2}\fatsemi\Delta_{3}\fatsemi\phi\land\psi\fatsemi\phi\land\psi\lx@proof@logical@and\Gamma\triangleright\Delta_{1}\fatsemi\Delta_{2}\fatsemi\phi\land\psi\fatsemi\phi\Gamma\triangleright\Delta_{1}\fatsemi\Delta_{2}\fatsemi\phi\fatsemi\phi\land\psi\lx@proof@logical@and\Gamma\triangleright\Delta_{1}\fatsemi\phi\fatsemi\phi\Gamma\triangleright\Delta_{2}\fatsemi\phi\fatsemi\psi\Gamma\triangleright\Delta_{3}\fatsemi\psi$

may be replaced by the derivation, which permutes the inferences,

$\Gamma\triangleright\Delta_{1}\fatsemi\Delta_{2}\fatsemi\Delta_{3}\fatsemi\phi\land\psi\lx@proof@logical@and\Gamma\triangleright\Delta_{1}\fatsemi\Delta_{2}\fatsemi\phi\Gamma\triangleright\Delta_{1}\fatsemi\Delta_{2}\fatsemi\phi\fatsemi\phi\Gamma\triangleright\Delta_{1}\fatsemi\phi\fatsemi\Delta_{2}\fatsemi\phi\Gamma\triangleright\Delta_{1}\fatsemi\phi\fatsemi\phi\fatsemi\Delta_{2}\Gamma\triangleright\Delta_{1}\fatsemi\phi\fatsemi\phi\Gamma\triangleright\Delta_{3}\fatsemi\psi$

This analysis allows us to eliminate $\mathsf{\mathsf{c}^{\mathcal{B}}_{R}}$
as it is captured wherever it is needed by the augmented rule for disjunction;
similarly, we may eliminate $\mathsf{\mathsf{c}^{\mathcal{B}}_{L}}$ by
incorporating it in the other rules. In total, this yields a new constraint
system, $\mathsf{LK}^{+}\oplus\mathcal{B}$.

######  Definition 6.8 (System $\mathsf{LK^{+}}\oplus\mathcal{B}$).

System $\mathsf{LK^{+}}\oplus\mathcal{B}$ is given in Figure 10, in which
$\Gamma$ and $\Delta$ are enriched $\mathscr{J}$-datum, and
$\Gamma\equiv\Gamma$ and $\Delta\equiv\Delta^{\prime}$ in $\mathsf{e}$.
$\triangleleft$

$\phi\fatcomma\Gamma\triangleright\Delta\fatsemi\phi\quad\phi\fatcomma\Gamma\triangleright\Delta\Gamma\triangleright\Delta\quad\Gamma\triangleright\Delta\fatsemi\phi\Gamma\triangleright\Delta\quad\phi\fatcomma\Gamma\triangleright\Delta\phi\fatcomma\phi\fatcomma\Gamma\triangleright\Delta\quad\Gamma\triangleright\Delta\Gamma^{\prime}\triangleright\Delta^{\prime}$

$\begin{array}[]{c@{\qquad}c}\neg\phi\fatsemi\Gamma\triangleright\Delta\Gamma\triangleright\Delta\fatsemi\phi&\Gamma\triangleright\Delta\fatsemi\neg\phi\cdot
x\lx@proof@logical@and\phi\cdot xy\fatcomma\Gamma\triangleright\Delta
xy=1\\\\[6.45831pt]
\phi\land\psi\fatcomma\Gamma\triangleright\Delta\phi\fatcomma\psi\fatcomma\Gamma\vdash_{\mathsf{}}\Delta&\Gamma\triangleright\Delta\fatsemi\phi\land\psi\lx@proof<EMAIL_ADDRESS>\phi\lor\psi\fatcomma\Gamma\triangleright\Delta\lx@proof@logical@and\phi\fatcomma\Gamma\triangleright\Delta\psi\fatcomma\Gamma\triangleright\Delta&\Gamma\triangleright\phi\lor\psi\cdot
x\fatsemi\Delta\Gamma\triangleright\phi\cdot xy\fatsemi\psi\cdot
x\bar{y}\fatsemi\Delta\\\\[6.45831pt]
\phi\to\psi\fatcomma\Gamma\triangleright\Delta\lx@proof@logical@and\Gamma\triangleright\Delta\fatsemi\phi\psi\fatcomma\Gamma\triangleright\Delta&\Gamma\triangleright\phi\to\psi\cdot
x\fatsemi\Delta\lx@proof@logical@and\Gamma\fatcomma\phi\cdot
xy\triangleright\psi\cdot xy\fatsemi\Delta xy=1\end{array}$

Figure 10: Constraint System $\mathsf{LK^{+}}\oplus\mathcal{B}$

System $\mathsf{LK^{+}}\oplus\mathcal{B}$ characterizes IPL locally — that is,
it is faithful and adequate with respect to _some_ sequent calculus for IPL.
That sequent calculus, however, is not $\mathsf{LJ}$, but rather a multiple-
conclusioned system $\mathsf{LJ}^{+}$. Essentially, $\mathsf{LJ^{+}}$ is the
multiple-conclusioned sequent calculus introduced by Dummett [Dummett2000]
with certain instances of the structural rules incorporated into the
operational rules.

######  Definition 6.9 (Sequent Calculus $\mathsf{LJ^{+}}$).

Sequent calculus $\mathsf{LJ^{+}}$ is given by the rules in Figure 11, in
which $\Gamma$ and $\Delta$ are $\mathscr{J}$-datum, and
$\Gamma\equiv\Gamma^{\prime}$ and $\Delta\equiv\Delta^{\prime}$ in
$\mathsf{e}$. $\triangleleft$

$\phi\fatcomma\Gamma\triangleright\Delta\fatsemi\phi\quad\phi\fatcomma\Gamma\triangleright\Delta\Gamma\triangleright\Delta\quad\Gamma\triangleright\Delta\fatsemi\phi\Gamma\triangleright\Delta\quad\phi\fatcomma\Gamma\triangleright\Delta\phi\fatcomma\phi\fatcomma\Gamma\triangleright\Delta\quad\Gamma\triangleright\Delta\Gamma^{\prime}\triangleright\Delta^{\prime}$