# Proof-theoretic Semantics and Tactical Proof

Alexander V. Gheorghiu  University College London
<EMAIL_ADDRESS>and  David J. Pym  University College London
& Institute of Philosophy, University of London<EMAIL_ADDRESS>
###### Abstract.

The use of logical systems for problem-solving may be as diverse as in proving
theorems in mathematics or in figuring out how to meet up with a friend. In
either case, the problem solving activity is captured by the search for an
_argument_ , broadly conceived as a certificate for a solution to the problem.
Crucially, for such a certificate to be a solution, it has be _valid_ , and
what makes it valid is that they are well-constructed according to a notion of
inference for the underlying logical system. We provide a general framework
uniformly describing the use of logic as a mathematics of reasoning in the
above sense. We use proof-theoretic validity in the Dummett-Prawitz tradition
to define validity of arguments, and use the theory of tactical proof to
relate arguments, inference, and search.

##  1\. Introduction

The definition of a system of logic may be given _proof-theoretically_ as a
collection of rules of inference that, when composed in specified ways,
determine _proofs_ ; that is, formal constructions that establish that a
conclusion is a consequence of some assumptions or axioms. In other words,
proofs are objects regulated by rules of a system that determine the inference
of a conclusion from premisses that have been established:

$\frac{\mathrm{Established\;Premiss}_{1}\quad\ldots\quad\mathrm{Established\;Premiss}_{k}}{\mathrm{Conclusion}}{\big{\Downarrow}}$

We call this proof-theoretic formulation _deductive logic_.

Deductive logic is useful as a way of defining what proofs are, but it does
not reflect either how logic is typically used in practical reasoning problems
or the method by which proofs are found. In practice, proofs are typically
constructed by starting with a desired, or putative, conclusion and applying
the rules of inference _backward_. Read from conclusion to premisses, the
rules are sometimes called _reduction operators_ , and denoted

$\frac{\mathrm{Sufficient\;Premiss}_{1}\quad\ldots\quad\mathrm{Sufficient\;Premiss}_{k}}{\mathrm{Putative\;Conclusion}}{\big{\Uparrow}}$

We call the constructions in a system of reduction operators _reductions_.
Crucially, the space of reductions contains proofs and objects that are not
proofs — specifically, reductions that cannot be continued in a way that
eventually reaches a proof. This proof-theoretic formulation has been dubbed
_reductive logic_ [33].

Reductive logic more closely resemble what mathematicians do when proving
theorems and, more generally, how people solve problems using formal
representations. It is also the paradigm on logic used for diverse
applications in informatics and other systems-oriented sciences, including,
but not limited to, areas such as program and systems verification, natural
language processing, and knowledge representation. Indeed, it is the reductive
perspective that underpins the use of logic in proof assistants — for example,
LCF, HOL, Isabelle, Coq, Mizar, Twelf, and more [45]. More generally, it is
the paradigm capturing the deployment of logic in the context of capturing
human reasoning, which is discussed extensively in, for example, the work of
Kowalski [23] and Bundy [6].

There are semantics of proofs, which give abstract accounts of object that
certify a statement as being valid in a logic, with a prime example given by
the categorical treatment of the BHK interpretation of intuitionistic logic.
But, importantly, reductive logic is concerned not only with what proofs but
more generally with things that may be continued to form proofs through
reduction. The semantics of proofs do not treat this bigger space of objects,
but these are central in the use of logic as a mathematics of reasoning.
Therefore, given the widespread application of reductive logic as a reasoning
technology, we require a semantic framework explicating the meaning of
reductions in the context of reasoning. Reciprocally, we require a general
framework stating what _valid_ reasoning is relative to a certain problem
domain. Such a framework would provide a basis for understanding and analyzing
the aforementioned wide-ranging applications of logic in practical reasoning
tasks, which is analogous to the use of semantics for programming languages.

A general framework supporting the mechanization of reductive logic is the
theory of _tactical proof_ introduced by Milner [28]. While little developed
mathematically, the theory is sufficiently general to encompass as diverse
reasoning activities as proving a formula in a formal system and seeking to
meet a friend before noon on Saturday. It does not concern finding the _best_
way to reason about a goal (e.g., minimizing the prospect of failure), though
these things are important, instead it makes precise how concepts used during
reasoning — such as ‘goal,’ ‘strategy,’ ‘achievement,’ ‘failure,’ etc. —relate
to one another. Crucially, the theory of tactical proof is a very general
meta-theoretic framework that subsumes specific procedures such as focusing,
uniform proof-search, resolution, matrix methods, and so on. It is tactical
proof that delivers systematically the various proof-assistants mentioned
above.

In this paper, we use the theory of tactical proof to give a general account
of the relationship between arguments — that is, abstract entities
representing reasoning — and inference in a logic. In so doing, we provide a
semantic framework for logic in practical reasoning problems, as witnessed by
tactical proof. Importantly, we do not say that this framework is how one
_should_ go about using logic as a mathematics of reasoning, but rather we aim
to _describe_ how logic is typically used in the literature. We justify the
framework by some coherence theorems relating arguments, reductive reasoning
(witnessed by tactics), and inference, and then give a series of examples
where the framework is implicit in the literature. While tactical proof
connects inference and arguments, the semantics of reasoning is given in the
paradigm of _proof-theoretic semantics_ (P-tS).

Introduced by Dummett [13] (based on results by Prawitz [32]) and developed by
Schroeder-Heister [35, 37], proof-theoretic validity is a semantics of
derivations (i.e., objects constructed inductively using rules of a formal
system) in Gentzen’s $\mathsf{NJ}$ [40]. A derivation in $\mathsf{NJ}$ is
(proof-theoretically) valid if and only if every closure — the result of
substituting its open assumption for proofs — of it reduces _á la_ Prawitz
[32] to a normal proof. The priority of normal proofs is justified according
to the principle that the introduction rules of Gentzen’s $\mathsf{NJ}$ act as
definitions of the logical constants they introduce — see Schroeder-Heister
[37] for a discussion. The details are given in Section 3. In this paper, we
generalize the notion of proof-theoretic validity to accommodate the full
potential of the theory of tactical proof.

The philosophy on which P-tS is based is _inferentialism_ , the view that
rules of inference confer meaning to expressions — see Brandom [4]). This
background renders P-tS the appropriate way (i.e., in contrast to, for
example, model-theoretic semantics) for understanding reductive logic and
reasoning because it ensures that the meaning of a reduction depends on the
accepted use within the activity of reasoning.

The paper begins in Section 2 with a terse but complete introduction to the
setup of logic needed in this this paper. It continues with a definition of
proof-theoretic validity for intuitionistic propositional logic, which
motivates later work. Following this, we present the theory of tactical proof
and discuss its application to logic. In Section 5, we briefly explain what
semantics of proofs have so far achieved and the way in which they are limited
for understanding the use of logic as a reasoning technology. In Section 6, we
propose a semantic framework that consider the entire space of reductions,
which proceeds through a general account of proof-theoretic validity. We
justify the framework by a correctness theorem and through a series of
examples from the literature in which it is implicit. The paper concludes in
Section 7 with a summary of results.

##  2\. Logic as Consequence

In this paper, we study logics generally, which is to say that instead of
considering a specific logic, we develop a general framework uniformly
applicable across logics. This requires us first to define what we mean by _a
logic_. Doing this is controversial. We choose to err on the side of being
over-encompassing, so almost any logic in the literature is readily captured.

Moreover, we also require a notion of inference. There are many paradigms we
may consider, such as _inter alia_ , natural deduction systems, axiomatic
systems (i.e., Hilbert calculi), and tableaux systems. The sequent calculus
format is sufficiently expressive to capture all these and is, therefore, the
paradigm used in this paper.

###  2.1. Consequence

A logic is captured by a relation called _consequence_ over data structures
called _sequents_. We will insist on nothing about these structures, and we do
not impose any particular properties of the consequence relation. Additional
restrictions are often helpful in practice but are not required for the
general framework presented herein.

Fix a set $\mathbb{S}$ of data-structures called _sequents_.

######  Definition 1 (Consequence).

A consequence relation is a predicate on a set of sequents.

We think of consequence as a judgement asserting that a certain sequent is
valid in the logic. Typically, such as in Example 2, sequents can be thought
of as tuples of data structures so that we may refer to consequence as a
relation between these structures.

######  Example 2 (Intuitionistic Sequents).

Fix a set of atomic propositions $\mathbb{P}$. The set of formulas
$\mathbb{F}$ (over $\mathbb{P}$) is constructed by the following grammar:

$\phi::=\rm
p\in\mathbb{P}\mid\phi\lor\phi\mid\phi\land\phi\mid\phi\to\phi\mid\bot$

An intuitionistic sequent is a pair $\Gamma\triangleright\phi$ in which
$\Gamma$ is a list of formulas and $\phi$ is a formula.

We have presented a definition of consequence that is, perhaps, overly
generous. Nonetheless, this definition means we readily capture any logic
within the literature. Refining the definition is challenging because logics
may have quite diverse data-structures, ranging from the familiar
list/multiset/set contexts of classical and intuitionistic logics, to the
structurally complex bunched contexts of relevance logics, and beyond,
rendering refinements quite subtle in order to not be arbitrarily exclusive.
The more substantial point is that we do not require such refinement. Hence,
restricting our notion of consequence according to some ideological principle
would be excessive and needless. Crucially, the definition of consequence
coheres naturally with the level of generality offered by the theory of
tactical proof (see Section 4), which is the framework we use in this paper to
capture the deployment of logic as a reasoning technology.

It is all very well to have a logic. It remains to define what reasoning steps
the logic supports. In this paper, what we mean by reasoning step is
_inference_ in a calculus for consequence.

###  2.2. Sequent Calculi

Taking the perspective on logic in Section 2, an inference is the process of
beginning with some sequents — thought of as a putative consequence of a logic
— and ending with another sequent — thought of as being entailed, according to
our logic, by the original sequents. These inferences are understood as
instances of rules.

######  Definition 3 (Rule).

A rule is a relation $\mathsf{r}$ on sequents.

That $\mathsf{r}(s,s_{1},\ldots,s_{n})$ obtains may be denoted by inference
schemas:

$\dfrac{s_{1}\ldots s_{n}}{s}\,r$

The sequent $s$ is said to be _conclusion_ and the sequents
$s_{1},\ldots,s_{n}$ the _premisses_. A rule that has no premisses (i.e., a
predicate on sequents) is called an _axiom_ -rule.

With this notion of rule, we give the standard treatment of sequent calculi
proofs — see, for example, Troestra and Schwichtenberg [42].

######  Definition 4 (Calculus).

A calculus is a set of rules containing at least one axiom-rule.

######  Definition 5 (Proof).

Let $\mathsf{L}$ be a calculus. The set of $\mathsf{L}$-proofs is the set of
rooted trees of sequents inductively constructed as follows:

Base Case. If there is an axiom-rule $\mathsf{a}\in\mathsf{L}$ such that
$\mathsf{a}(s)$, then the tree of just the node $s$ is an $\mathsf{L}$-proof.

Induction Step. If $\mathcal{P}_{1},\ldots,\mathcal{P}_{n}$ are
$\mathsf{L}$-proofs with roots $s_{1},\ldots,s_{n}$, respectively, and there
is a sequent $s$ and a rule $\mathsf{r}\in\mathsf{L}$ such that
$\mathsf{r}(s,s_{1},\ldots.,s_{n})$ obtains, then the argument $\mathcal{P}$
with root $s$ and immediate sub-trees $\mathcal{P}_{1},\ldots,\mathcal{P}_{n}$
is a proof.

The notion of proof from a calculus induces a notion of provability from the
calculus, which is a consequence relation:

######  Definition 6 (Provability).

A sequent is $\mathsf{L}$-provable iff there is a $\mathsf{L}$-proof that
concludes it.

We say that a calculus $\mathsf{L}$ _characterizes_ a logic when
$\mathsf{L}$-provability coincides with the consequence relation of the logic.
To be precise, this coincidence has two directions: _soundness_ and
_completeness_. The calculus is _sound_ for the logic when it only proves the
consequences of the logic, and it is _complete_ when it can prove all of the
consequences of the logic.

######  Definition 7 (Soundness and Completeness).

Let $\vdash$ be a consequence relation and $\mathsf{L}$ be a calculus.

  * -

Calculus $\mathsf{L}$ is _sound_ for $\vdash$ iff, for any $s\in\mathbb{S}$,
if $\vdash_{\mathsf{L}}s$, then $\vdash s$.

  * -

Calculus $\mathsf{L}$ is _complete_ for $\vdash$ iff, for any
$s\in\mathbb{S}$, if $\vdash s$, then $\vdash_{\mathsf{L}}s$.

Of course, several different calculi may characterize a logic, some of which
may differ substantially. One way to generate new calculi from old is by
including rules that are conservative over provability. Such rules are said to
be _admissible_ — that is, $\mathsf{r}$ is admissible in $\mathsf{L}$ iff
$\vdash_{\mathsf{L}\cup\\{\mathsf{r}\\}}$ is sound with respect to
$\vdash_{\mathsf{L}}$. More generally, a rule can be admissible for a logic
when it preserves validity in the logic — that is, that is, $\mathsf{r}$ is
admissible for $\vdash$ iff, for any $s,s_{1},...,s_{n}\in\mathbb{S}$, if
$\mathsf{r}(s,s_{1},...,s_{n})$ obtains and $\vdash s_{1}$, $\ldots$ , $\vdash
s_{n}$, then $\vdash s$. Observe that if $\mathsf{L}$ is sound for $\vdash$,
then it is necessarily the case that all the rules in $\mathsf{L}$ are
admissible for $\vdash$.

######  Example 8 (Example 2 cont’d).

Calculus $\mathsf{LJ}$ is given by the rules of Figure 1, in which $\Gamma$
and $\Gamma^{\prime}$ are understood to be permutations of each other as
lists. This calculus characterizes intuitionistic logic (IPL) — that is, an
intuitionistic sequent $\Gamma\triangleright\phi$ is a consequence in IPL iff
it is $\mathsf{LJ}$-provable. Gentzen [40] proved that the following rules is
admissible for IPL:

$\Delta,\Gamma\triangleright\chi\lx@proof@logical@and\Delta\triangleright\phi\phi,\Gamma\triangleright\chi$

$\phi,\Gamma\triangleright\Delta\Gamma\triangleright\Delta\quad\Gamma\triangleright\phi\Gamma\triangleright\varnothing\quad\phi,\Gamma\triangleright\Delta\phi,\phi,\Gamma\triangleright\Delta\quad\Gamma\triangleright\Delta\Gamma^{\prime}\triangleright\Delta^{\prime}$
$\Gamma\triangleright\phi\land\psi\lx@proof@logical@and\Gamma\triangleright\phi\Gamma\triangleright\psi\quad\phi\land\psi,\Gamma\triangleright\Delta\phi,\Gamma\triangleright\Delta\quad\phi\land\psi,\Gamma\triangleright\Delta\psi,\Gamma\triangleright\Delta\quad\Gamma\triangleright\neg\phi\phi,\Gamma\triangleright\varnothing$
$\phi\lor\psi,\Gamma\triangleright\Delta\lx@proof@logical@and\phi,\Gamma\triangleright\Delta\psi,\Gamma\triangleright\Delta\quad\Gamma\triangleright\phi\lor\psi\Gamma\triangleright\phi\quad\Gamma\triangleright\phi\lor\psi\Gamma\triangleright\psi\quad\neg\phi,\Gamma\triangleright\varnothing\Gamma\triangleright\phi$
$\quad\Gamma\triangleright\phi\to\psi\phi,\Gamma\triangleright\psi\quad\phi\to\psi,\Gamma_{1},\Gamma_{2}\triangleright\Delta\lx@proof@logical@and\Gamma_{1}\triangleright\phi\psi,\Gamma_{2}\triangleright\Delta\quad\phi\triangleright\phi$

Figure 1. System $\mathsf{LJ}$

This concludes a terse but complete account of a general perspective of logic
and its proof-theoretic formulation as required in this paper.

Our position is that the objects constructed in various paradigms of
argumentation (e.g., natural deduction, dialogue games, etc.) are meaningful
precisely to the extent that they represent reasoning in a logic. In this
paper, we take ‘reasoning in a logic’ that to mean proof in a sequent calculus
characterizing a logic. For example, consider the tree-like constructions from
Gentzen’s $\mathsf{NJ}$ (see Section 3), which are supposed to represent
intuitionistic reasoning — indeed, we may say that they are a _natural_
representation of reasoning (see, for example, Tennant [41]). We take the view
that what makes them valid in intuitionistic logic is their relationship to
intuitionistic consequence, as captured by the relationship to Gentzen’s
$\mathsf{LJ}$. We use the theory of tactical proof to make this idea of the
relationship between reasoning and logic precise.

##  3\. Proof-theoretic Validity for Intuitionistic Propositional Logic

Central to this paper is the paradigm of _proof-theoretic semantics_ (P-tS).
We defer an explanation of the relevance of P-tS to the problem of this paper
to Section 5, and presently give an account of it for intuitionistic
propositional logic (IPL). This will facilitate the more general discussion of
the subject below and motivate later work.

####  3.0.1. Intuitionistic Propositional Logic

We begin by fixing the terminology for IPL as used in this paper; this extends
the setup of Example 2 and Example 8.

######  Definition 9 (IPL Formula).

Fix a set of atomic propositions $\mathbb{P}$. The set of IPL formulas
$\mathbb{F}$ (over $\mathbb{P}$) is constructed by the following grammar:

$\phi::={\rm
p}\in\mathbb{P}\mid\phi\lor\phi\mid\phi\land\phi\mid\phi\to\phi\mid\bot$

We use the following abbreviations:

$\hat{\Gamma}:=\bigwedge_{\phi\in\Gamma}\phi\qquad\neg\phi:=\phi\to\bot$

######  Definition 10 (IPL Sequent).

An IPL sequent is a pair $\Gamma\triangleright\phi$ in which $\Gamma$ is a set
of formulas and $\phi$ is a formula.

We will characterize the consequence relation for IPL by proof in Gentzen’s
$\mathsf{NJ}$ [40]. To this end, we introduce some terminology for the
paradigm of argument known as _natural deduction_.

######  Definition 11 (Natural Deduction Argument).

A natural deduction argument is a rooted tree of formulas in which some
(possibly no) leaves are marked as discharged.

An argument is open if it has undischarged assumptions; otherwise, it is
closed.

In this section we will simply say _argument_ to mean natural deduction
argument. The leaves of an argument are its _assumptions_ , the root is its
_conclusion_. That $\mathcal{A}$ has open assumptions $\Gamma$, closed
assumptions $\Delta$, and conclusion $\phi$ may be denoted as follows:

$\phi\mathcal{A}\qquad\mathcal{A}\Gamma,[\Delta]\qquad\phi\mathcal{A}\Gamma,[\Delta]$

Intuitively, an argument $\mathcal{A}$ with open assumptions $\Gamma$ and
conclusion $\phi$, is an argument _for_ the sequent
$\Gamma\triangleright\phi$. We call this sequent the consequence of the
argument. We use a system of natural deduction to define a class of arguments
whose consequence precisely coincide with consequences of IPL.

A natural deduction system is given by rules governing the composition of
arguments. We follow the standard treatments (see, for example, van Dalen [44]
or Troelstra and Schwichtenberg [42]), doubtless already familiar.

######  Definition 12 (Natural Deduction System $\mathsf{NJ}$).

The natural deduction system $\mathsf{NJ}$ is composed of the rules in Figure
2.

$\phi\land\psi\lx@proof@logical@and\phi\psi\qquad\phi\phi\land\psi\quad\psi\phi\land\psi\qquad\phi\to\psi\phi[\psi]\qquad\phi\bot$
$\phi\lor\psi\phi\quad\phi\lor\psi\psi\qquad\chi\lx@proof@logical@and\phi\lor\psi\chi[\phi]\chi[\psi]\qquad\phi\lx@proof@logical@and\phi\phi\to\psi$

Figure 2. Calculus $\mathsf{NJ}$

######  Definition 13 ($\mathsf{NJ}$-Derivation).

The set of $\mathsf{NJ}$-derivations is defined inductively as follows:

Base Case. If $\phi$ is a formula, then the one element tree $\phi$ is a
$\mathsf{NJ}$-derivation.

Inductive Step. Let $\mathsf{r}$ be a rule in $\mathsf{NJ}$ and
$\mathcal{D}_{1},...,\mathcal{D}_{n}$ be $\mathsf{NJ}$-derivations. If
$\mathcal{D}$ is an argument arising from applying $\mathsf{r}$ to
$\mathcal{D}_{1},...,\mathcal{D}_{n}$, then $\mathcal{D}$ is an
$\mathsf{NJ}$-derivation.

A _closed $\mathsf{NJ}$-derivation_ in a calculus is an $\mathsf{NJ}$-_proof_.
The existence of such proofs characterizes IPL.

######  Proposition 14 (Gentzen [40]).

There is an $\mathsf{NJ}$-derivation of $\Gamma\triangleright\phi$ iff
$\Gamma\vdash\phi$.

To give an account of proof-theoretic validity for IPL in the Dummett-Prawitz
tradition, we require some auxiliary definitions.

The rules of $\mathsf{NJ}$ with subscripts $\mathsf{I}$ and $\mathsf{E}$ are
the _introduction rules_ ($I$-rules) and _elimination rules_ ($E$-rules),
respectively.

######  Definition 15 (Detour).

A _detour_ in a derivation is a sub-derivation in which a formula is obtained
by an $I$-rule and is then the major premise of the corresponding $E$-rule.

######  Example 16.

The following is a detour for conjunction:

$\psi\lx@proof@logical@and\phi\mathcal{D}_{1}\phi\to\psi\psi\mathcal{D}_{2}[\phi]$

######  Definition 17 (Canonical Derivation).

A derivation is canonical iff it contains no detours.

Prawitz [32] proved that canonical $\mathsf{NJ}$-proofs are complete for IPL.
The argument uses a reduction relation $\rightsquigarrow$ that precisely
eliminates detours; for example, detours with implication are reduced as
follows:

$\psi\lx@proof<EMAIL_ADDRESS>
The reflexive and transitive closure of $\rightsquigarrow$ is denoted
$\rightsquigarrow^{\ast}$. This reduction relation is normalizing and its
normal forms are canonical derivations.

######  Proposition 18 (Prawitz [32]).

There is a canonical $\mathsf{NJ}$-derivation of $\Gamma\triangleright\phi$
iff $\Gamma\vdash\phi$.

This establishes the relevant syntax and proof theory required for IPL in this
paper. In following subsection, we present proof-theoretic validity for
natural deduction.

####  3.0.2. Proof-theoretic Validity

It was Dummett [13] who first realized the philosophical significance of the
normalization result by Prawitz [32] (i.e., Proposition 18). This begins the
development of proof-theoretic validity as a semantics of arguments. We follow
the account given by Schroeder-Heister [35].

When introducing natural deduction, Gentzen [40] offered the following
remarks:

> The introductions represent, as it were, the ‘definitions’ of the symbols
> concerned, and the eliminations are no more, in the final analysis, than the
> consequences of these definitions. This fact may be expressed as follows: In
> eliminating a symbol, we may use the formula with whose terminal symbol we
> are dealing only ‘in the sense afforded it by the introduction of that
> symbol’.

The following corollary of the normalization result (Proposition 18) supports
this view:

######  Corollary 19.

There is a canonical $\mathsf{NJ}$-derivation of $\Gamma\triangleright\phi$
concluding with an introduction rule iff $\Gamma\vdash\phi$.

Together, the above suggest an inferentialist semantics of arguments according
to the following principals:

  * -

canonical proofs are _a priori_ valid

  * -

closed derivations are valid as a consequence of them reducing to canonical
proofs

  * -

open derivations are regarded as placeholders for closed derivations according
to their possible closures.

What we are calling proof-theoretic validity is a specific realization of this
semantic brief. To definite it, we must define what is meant by the _closure_
of a derivation.

The idea is that we substitute open assumptions for closed derivations.
However, an argument may contain open assumptions that are not consequences of
IPL and thus (by Proposition 14) do not admit $\mathsf{NJ}$-proofs. How are
such things closed? Therefore, to form the semantics, we consider validity in
possible extensions of $\mathsf{NJ}$ that can handle such assumptions.

If the open assumptions of an argument are complex formulas, then one may use
rules of $\mathsf{NJ}$ to produce something simpler. What remains to consider
is the case where the open assumptions are atomic propositions. In this case,
their meaning is supplied by an atomic _base_.

######  Definition 20 (Base).

A base is a finite set of rules over atomic propositions,

${\rm c}\lx@proof@logical@and{\rm p}_{1}...{\rm p}_{n}$

The premisses of the rule may be empty; that is, the rule may be an axiom.

The atomic rules are not necessarily closed under substitution. To see how
they confer meaning to atomic propositions, consider the statement ‘Tammy is a
vixen’. What does it mean? Intuitively, it means, somehow, that ‘Tammy is a
vixen’ _and_ ‘Tammy is a fox’. In the current setup, this is to say that we
have base containing the following rules:

${\small\begin{array}[]{c}\text{Tammy is a
vixen}\lx@proof@logical@and\text{Tammy is a fox}\text{Tammy is
female}\qquad\text{Tammy is female}\text{Tammy is a vixen}\qquad\text{Tammy is
a fox}\text{Tammy is a vixen}\\\ \end{array}}$

This is because the sense of ‘and’ in the above heuristic is made precise by
the inferential semantics of $\land$, defined by the rules
$\mathsf{\land_{I}}$, $\mathsf{\land^{1}_{E}}$, and $\mathsf{\land^{2}_{E}}$,
which are emulated by the above rules.

######  Definition 21 (Derivation in a Base).

Let $\mathscr{B}$ be a base. The set of $\mathscr{B}$-derivations is
inductively defined as follows:

Base Case. If ${\rm p}\in\mathbb{P}$ is an atom, then the one element tree
consisting of ${\rm p}$ is a $\mathscr{B}$-derivation.

Inductive Step. Let $\mathsf{r}$ be a rule in $\mathscr{B}$ and
$\mathcal{D}_{1},...,\mathcal{D}_{n}$ be $\mathscr{B}$-derivations. If
$\mathcal{D}$ is an argument arising from applying $\mathsf{r}$ to
$\mathcal{D}_{1},...,\mathcal{D}_{n}$, then $\mathcal{D}$ is a
$\mathscr{B}$-derivation.

Relative to a base (including the empty base) one has a simple proof-theoretic
semantics for the formulas of IPL: a formula is valid (relative to the base)
iff it admits a valid argument (relative to the base).

######  Definition 22 (Validity Natural Deduciton Argument).

Let $\mathscr{B}$ be a base. The $\mathscr{B}$-valid of an argument
$\mathcal{A}$ is inductively defined as follows:

  * -

$\mathcal{A}$ is a closed $\mathscr{B}$-derivation

  * -

$\mathcal{A}$ is a closed canonical $\mathsf{NJ}\cup\mathscr{B}$-derivation
whose immediate sub-derivations $\mathcal{A}_{1},...\mathcal{A}_{n}$ are
$\mathscr{B}$-valid

  * -

$\mathcal{A}$ is a closed non-canonical
$\mathsf{NJ}\cup\mathscr{B}$-derivation that reduces to a $\mathscr{B}$-valid
canonical derivation $\mathcal{A}^{\prime}$

  * -

$\mathcal{A}$ is an open derivation and, for every
$\mathscr{C}\supseteq\mathscr{B}$, any extension of $\mathcal{A}$ by
$\mathscr{C}$-valid arguments of the assumptions
$\mathcal{C}_{1}....,\mathcal{C}_{n}$ is a $\mathscr{C}$-valid argument.

An argument is valid iff it is $\mathscr{B}$-valid for every base
$\mathscr{B}$.

Schroeder-Heister [35] has relativized this definition to the atomic system
considered and to the set of justifications (proof reductions) considered. In
Section 6.1, we go further and relativize it to the notion of argument too.

This concludes the definition of proof-theoretic validity for IPL. In the next
section, we explain what it has to do with _reasoning_ in IPL and the rôle of
tactics in relating natural deduction to consequence for the logic.

Intuitively, the rules of $\mathsf{NJ}$ are instructions for constructing
arguments. When _reasoning_ in $\mathsf{NJ}$, we begin with an argument for a
putative conclusion and use the rules of $\mathsf{NJ}$ backwards to construct
a closed $\mathsf{NJ}$-derivation. What makes each reasoning step valid is
that an admissible rules witness it. The relationship suggested here between
$\mathsf{NJ}$\- and $\mathsf{LJ}$-proofs justifying this is, of course, well-
known — see, for example, Gentzen [40]. It may be summarized as saying that
constructions in $\mathsf{NJ}$ are intuitionistic _proofs_ and constructions
in $\mathsf{LJ}$ are _constructions of intuitionistic proofs_. We use the
theory of tactical proof to make this idea precise.

##  4\. The Theory of Tactical Proof

The theory of tactical proof is a meta-theoretic framework supporting
reductive logic and its mechanization. Indeed, tactical proof is sufficiently
general to encompass diverse reasoning activities at various levels of
formality, which may be as widely different as proving a theorem in a
mathematical theory, seeking to win at chess, and arranging to meet a friend
before noon on Saturday. The point is that all such reasoning activities,
different in domain and formality, can be articulated in terms of a uniform
language that a user may express insight into reasoning methods and delegate
routine, but error-prone, work to a machine. In the words of Milner [28]:

> Here it is a matter of taste whether the human prover wishes to see this
> performance done by the machine, in all its frequently repulsive detail, or
> wishes only to see the highlights, or is merely content to let the machine
> announce the result (a theorem!).

Following Milner [28], we introduce the theory at the full level of generality
at first and then concentrate on it in the context of proof-search in logics.

###  4.1. Tactics and Tacticals

One has two classes of prime entities: _goals_ and _events_. The two classes
are carried by the sets $\mathbb{GOALS}$ and $\mathbb{EVENTS}$, respectively.
The goals and events are related by a notion of _achievement_
$\propto\,\subseteq\mathbb{GOALS}\times\mathbb{EVENTS}$ that determines what
events witness what goals. The idea is that an event $\mathscr{E}$ achieves
goal $G$ as it satisfies the description that the goal has
designated.Heuristically, an event achieves a goal when it satisfies the
description that the goal has designated. For example, the goal $G$ that Alice
and Bob meet before noon on Saturday is achieved by the event $\mathscr{E}$ is
that Alice and Bob meet under the clock at Waterloo station at 11:53 on
Saturday.

We take reasoning about a goal as the process of replacing it with new goals
that suffice to produce the original. In the nomenclature of reductive logic,
such replacements are captured by _reduction operators_ , which may be taken
as a partial function from goals to lists of goals:

$\rho:\mathbb{GOALS}\rightharpoonup\textsc{list}(\mathbb{GOALS})$

The goals produced by applying a reduction operator to a given goal are said
to be _subgoals_.

What renders a reduction from a goal to a list of subgoals valid is that any
events possibly witnessing the subgoals yield an event possibly witnessing the
original goal. This justification is witnessed by a _procedure_ ,

$\pi:\textsc{list}(\mathbb{EVENTS})\rightharpoonup\mathbb{EVENTS}$

Returning to the example above concerning Alice and Bob, the goal $G$ may be
reduced to the following sub-goals:

$\begin{array}[]{ccl}G_{1}&:&\text{Alice arrives under the clock at Waterloo
Station before noon on Saturday }\\\ G_{2}&:&\text{Bob arrives under the clock
at Waterloo Station before noon on Saturday.}\end{array}$

This reduction is justified by the fact that $G_{1}$ and $G_{2}$ are achieved
by the following events, respectively, which yield $\mathscr{E}$ through the
procedure of _waiting_ :

$\begin{array}[]{ccl}\mathscr{E}_{1}&:&\text{Alice arrives at Waterloo Station
at 11:57 on Saturday }\\\ \mathscr{E}_{2}&:&\text{Bob arrives at Waterloo
Station at 11:53 on Saturday.}\end{array}$

Thus, one step of reasoning amounts to applying a (partial) mapping takings
goals to subgoals together with a procedure,

$\tau:G\mapsto\langle[G_{1},\ldots,G_{n}],\pi\rangle$

These mappings are called _tactics_. According to the above discussion, we
have the following notion of validity:

######  Definition 23 (Valid Tactic).

Let $\propto$ be a notion of achievement. A tactic $\tau$ is $\propto$-valid
iff, for any $G,G_{1},\ldots,G_{n}\in\mathbb{GOALS}$ and
$\mathscr{E},\mathscr{E}_{1},\ldots,\mathscr{E}_{n}\in\mathbb{EVENTS}$, if
$\tau:G\mapsto\langle[G_{1},\ldots,G_{n}],\pi\rangle$ and
$\mathscr{E}:=\pi(\mathscr{E}_{1},\ldots,\mathscr{E}_{n})$, and
$\mathscr{E}_{i}\propto G_{i}$ obtains for $1\leq i\leq n$, then
$\mathscr{E}\propto G$ obtains.

Of course, a goal typically requires several iterations of reasoning of the
above form such that subgoals are resolved into further subgoals, and so on.
For example, suppose Alice starts from Andover and Bob starts from Birmingham;
then, to reason about $G$, one requires many component tactics that
collectively bridge the distance both physical and temporal — for instance,
one may have the subgoal $G_{1}^{\prime}$ for $G_{1}$ that ‘Bob takes the tube
to Waterloo Station from Euston Station’, which is witnessed by the event ‘Bob
takes the 11:46 southbound Norther Line service from Euston to Waterloo on
Saturday.’ Hence, we require a notion of composition of tactics.

A composition of tactics is called a _tactical_. A tactical is valid when it
preserves the validity of the tactics it combines:

######  Definition 24 (Valid Tactical).

A tactical is valid iff it preserves the validity of tactics; that is, if
$\circ$ is a tactical and $\tau_{1}$,…,$\tau_{n}$ are $\propto$-valid, then
$\circ(\tau_{1},\ldots,\tau_{n})$ are $\propto$-valid.

The foregoing is a complete account of tactical reasoning as introduced by
Milner [28]. To be precise in the semantics presented in this paper, we
supplement the above with some additional definitions.

######  Definition 25 (Tactical System).

A tactical system $\mathsf{T}$ is a collection of tactics and tacticals that
are valid relative to some notion of achievement.

We have opted to present the theory in its full generality. In the sequel, we
apply it to the context of the use of logic as a reasoning technology. We
follow the account in Milner [28], which is the basis of many automated
reasoning technologies using logic, such as the proof assistants mentioned in
Section 1.

Let $\vdash$ be the consequence relation for IPL — see Section 3. We have the
following setup:

  * -

a goal is a sequent $\Gamma\triangleright\phi$ in which $\Gamma$ is a list of
formulas and $\phi$ is a formula

  * -

an event is a consequence $\Delta\vdash\psi$

  * -

the achievement relation $\propto$ is as follows:

$(\Delta\triangleright\psi)\propto(\Gamma\triangleright\phi)\qquad\text{ iff
}\qquad\phi=\psi\text{ and }\Delta\sqsubseteq\Gamma\text{ and
}\Delta\vdash\psi$

(We write $\Delta\sqsubseteq\Gamma$ to denote that the set of elements in
$\Delta$ is a subset of the set of elements of $\Gamma$)

In this context, a tactic is valid iff it corresponds to an admissible rule
for IPL. For example, in $\mathsf{NJ}$ the $\mathsf{\land_{I}}$-rule
determines the tactic $\tau_{\mathsf{\land_{I}}}$ which has the following
components:

$\underbrace{\Gamma\triangleright\phi\land\psi\lx@proof@logical@and\Gamma\triangleright\phi\Gamma\triangleright\psi}_{\text{reduction
operator}}\qquad\underbrace{\Delta_{1},\Delta_{2}\vdash\phi\land\psi\lx@proof@logical@and\Delta_{1}\vdash\phi\Delta_{2}\vdash\psi}_{\text{procedure}}$

This concludes the overview of the theory of tactical proof as used in this
paper. What has not been given here is an account of exactly what _argument_
is constructed by a tactic, which we defer to Section 6.

###  4.2. Tactical Proof and Intuitionistic Propositional Logic

Having presented the theory of tactics as a metatheoretical framework in which
one studies reasoning — the construction of arguments — in its full
generality, it is informative to consider how it applies in the concrete
setting of natural deduction for IPL.

In Section 4.1, we witnessed the following tactic corresponding to the
$\mathsf{\land_{I}}$ rule:

$\tau_{\land}:(\Gamma\triangleright\phi\land\psi)\mapsto\langle[(\Gamma\triangleright\phi),(\Gamma\triangleright\psi)],\mathsf{\land_{R}}\rangle$

The analogous treatment of $\mathsf{\to_{I}}$ yields the following:

$\tau_{\to}:(\Gamma\triangleright\phi\to\psi)\mapsto\left\langle[(\phi,\Gamma\triangleright\psi)],\mathsf{\to_{R}}\right\rangle$

These individual reasoning steps are combined with a _tactical_ $\fatsemi$
that corresponds to the sequential application of rules in natural deduction:

$\tau_{\land}\fatsemi\tau_{\to}:\big{(}\Gamma\triangleright\chi\land(\phi\to\psi)\big{)}\mapsto\langle[(\Gamma\triangleright\chi),(\phi,\Gamma\triangleright\psi)],\mathsf{\land_{R}}\otimes\mathsf{\to_{R}}\rangle$

The procedure $\mathsf{\land_{R}}\otimes\mathsf{\to_{R}}$ is the product of
the procedures for $\mathsf{\land_{R}}$ and $\mathsf{\to_{R}}$.

We have thus related natural deduction and consequence using tactics. And yet,
something is missing in this setup. What argument does
$\tau_{\land}\fatsemi\tau_{\to}$ witness? This question demands an
interpretation of tactics as arguments, understood as abstract entities such
as natural deduction arguments.

Moreover, the justification for proof-theoretic validity came from the idea
that the introduction rules are definitional. That is all very well, but it
isn’t the only choice. Depending on various desiderata, we are left with
various answers to the question, _what is a valid argument?_ By framing the
relationship between arguments and consequence in the theory of tactical
proof, we can define various notions of validity on arguments according to the
priority, by fiat, of some sequent calculus characterizing consequence and
some transformations of arguments. Furthermore, there is nothing about tactics
that pertains, in particular, to natural deduction, so the notion of argument
herein can be generalized to other paradigms too. These generalizations
deliver the semantic framework for logic as a reasoning technology that this
paper is about.

###  4.3. Tactical Proof and Logic

The theory of tactical proof is an engine relating the search for arguments.
It is, essentially, a system of reduction operators that are step-wise
justified by rules in a sequent calculus. That is how we regard them in this
paper. The application of tactics drives the computation of arguments, which
is to say the _search_ for arguments, and a sequent calculus (in the sense of
Section 2) provides procedures. As such, supplying a sequent calculus amounts
to supplying a notion of _inference_ against which the computation of an
argument is justified. This is captured in the semantic framework of this
paper in Section 6

The dichotomy between proof and search actually predates the tactical proof.
The components were historically called _analysis_ and _synthesis_ ,
respectively — see Pólya [31] for a general discussion of this study for
mathematical practice. In _analysis_ , one repeatedly asks from what
conditions could the desired result, which is to say goal, be obtained; during
_synthesis_ , one derives from the analysis a solution to the problem.

In this paper, the shift from analysis to synthesis (i.e., the shift from
computing subgoals to using procedures, from reduction to deduction) is
captured by a _synthesizer_.

######  Definition 26 (Synthesizer).

Let $\mathsf{L}$ be a sequent calculus and $\mathsf{T}$ be tactical system
with achievement $\propto$ whose events are $\mathsf{L}$-sequents. The
achievement $\propto$ is an $\mathsf{L}$-synthesizer for $\mathsf{T}$ iff the
procedures of $\mathsf{T}$ are the rules of $\mathsf{L}$.

An example of a synthesizer is offered at the end of Section 4.1. Here the
reduction operators correspond to $\mathsf{NJ}$ rules, and the procedures
correspond to $\mathsf{LJ}$ rules.

In the same way that tactics are implicit in much of the literature on logic,
synthesizers also appear implicitly anywhere one considers the inferential
content within arguments in a certain space. The running case of natural
deduction for IPL discussed above is a key example; we give some others in
Section 6.3.

##  5\. The Semantics of Proofs

On the one hand, we have structures called arguments that represent evidence
for a consequence of a logic — for example, natural deduction proofs _à la_
Gentzen [40], _à la_ Fitch [14], _à la_ Lemmon [25], and so on. On the other
hand, we have a formal account of _inference_ supplied by fixing a sequent
calculus for a logic. We use the theory of tactical proof introduced by Milner
[28] to relate the two. We desire a framework able to explain these
connections because reductive logic is central within the practice of logic as
a mathematics of reasoning, especially within system-oriented science (e.g.,
in the use of logic for program and systems verification, natural language
processing, and proof assistants). Hence, we require a semantics of proofs to
determine _valid_ arguments and to consider their construction.

Of course, semantics of proofs for particular logics have been very
substantially developed for particular logics. Intuitionism, as defined by
Brouwer [5], is the view that an argument is valid when it provides sufficient
evidence for its conclusion. This defines intuitionistic logic (IL). A
consequence is that IL differs from classical logic by rejecting _tertium non
datur_ — that is, the ability to assert a proposition for the rejection of its
negation — as such an inference does not constitute sufficient evidence for
its conclusion. Heyting [18] and Kolmogorov [22] provided a semantics for
intuitionistic proof, which captures the evidential character of intuitionism,
called the Brouwer-Heyting-Kolmogorov (BHK) interpretation of IL. It is now
the standard explanation of the logic — see, for example, van Atten [43].
Proof-theoretic validity (P-tV) for IPL (see Section 3) is, of course,
strongly related to BHK — see Schroeder-Heister [36].

The _propositions-as-types_ correspondence — see Howard [20] — gives an
standard way of instantiating the denotation of proofs in the BHK
interpretation of intuitionistic propositional logic (IPL) as terms in the
simply-typed $\lambda$-calculus. Technically, the setup can be sketched as
follows: a judgement that $\Phi$ is an $\mathsf{NJ}$-proof of the sequent
$\phi_{1},\ldots,\phi_{k}\triangleright\phi$ corresponds to a typing judgement

$x_{1}:A_{1},\ldots,x_{k}:A_{k}\vdash M(x_{1},\ldots,x_{k}):A$

where the $A_{i}$s are types corresponding to the $\phi_{i}$s, the $x_{i}$s
correspond to placeholders for proofs of the $\phi_{i}$s, the $\lambda$-term
$M(x_{1},\ldots,x_{k})$ corresponds to $\Phi$, and the type $A$ corresponds to
$\phi$.

Lambek [24] gave a more abstract account by showing that simply-typed
$\lambda$-calculus is the internal language of cartesian closed categories
(CCCs), thereby giving a categorical semantics of proofs for IPL. In this
setup, a morphism

$\llbracket\phi_{1}\rrbracket\times\ldots\times\llbracket\phi_{k}\rrbracket\stackrel{{\scriptstyle\llbracket\Phi\rrbracket}}{{\longrightarrow}}\llbracket\phi\rrbracket$

in a CCC (where $\times$ denotes cartesian product) that interprets the
$\mathsf{NJ}$-proof $\Phi$ of $\phi_{1},\ldots,\phi_{k}\triangleright\phi$
also interprets the term $M$, where the $\llbracket\phi_{i}\rrbracket$s
interpret also the $A_{i}$s and $\llbracket\phi\rrbracket$ also interprets
$A$.

To generalize to full IL (and beyond), Seely [38] modified this categorical
setup and introduced _hyperdoctrines_ — indexed categories of CCCs with
coproducts over a base with finite products. Martin-Löf [26] gave a formulae-
as-types correspondence for predicate logic using dependent type theory.
Barendregt [3] gave a systematic treatment of type systems and the
propositions-as-types correspondence. A categorical treatment of dependent
types came with Cartmell [7] — see also, for examples among many, work by
Streicher [39], Pavlović [30], Jacobs [21], and Hofmann [19]. In total, this
gives a semantic account of _proof_ for first- and higher-order predicate
intuitionistic logic based on the BHK interpretation.

That is all very well as explaining what a proof is for IL, but the space of
objects considered when finding an argument also contains things that are not
proofs and cannot be continued to form proofs. Constructed by backward
inference, we call these objects _reductions_. In IPL, an example of a
reduction that fails to be a proof is an $\mathsf{NJ}$-derivation whose open
assumptions are not theorems of IPL. While such an argument is well-
constructed according to intuitionism, it is not valid since it is not closed
and cannot be closed (i.e., the open assumptions cannot be substituted for
proofs). We desire a semantics of proofs able to treat the entire space of
reductions as the latter are central to the use of logic within practical
reasoning. In Section 3, we saw that proof-theoretic semantics could account
for such arguments, which are beyond the scope of BHK. Pym and Ritter [33]
have provided a general semantics of reductive logic in the context of
classical and intuitionistic logic through polynomial categories; that is, by
extending the categories in which arrows denote proofs for a logic by
additional arrows that supply ‘proofs’ for propositions that do not have
proofs but appear during reduction.

This paper aims to provide a uniform framework for describing the relationship
between argument, reduction, and inference. Taking the view that what makes an
argument valid for a logic is that it respects a notion of inference for that
logic, we subscribe to _inferentialism_ (see Brandom [4]). We generalize
proof-theoretic validity such that we can handle an arbitrary notion of
argument (i.e., not just natural deduction _à la_ Gentzen [40]) for an
arbitrary logic (i.e., not just IPL). This is the subject of Section 6.

##  6\. Proof-theoretic Semantics and Tactical Proof

In this section, we address the problems raised in Section 5 and present a
uniform framework relating arguments, tactical proof (reductive reasoning),
and sequent calculi (inference) based on inferentialism. We do this through a
generalized view of proof-theoretic validity (see Section 3), using the theory
of tactical proof as the engine of computation through which inference and
argument are related. This work is intended to be descriptive in that it is a
uniform metatheoretical platform witnessing how these things are typically
related in the literature.

###  6.1. Proof-theoretic Validity, generalized

We begin with a space of _arguments_ $\mathbb{A}$. Within this space, there is
a subset $\mathbb{P}\subseteq\mathbb{A}$ arguments that are _a priori_ valid;
these are called _canonical proofs_. These canonical proofs for the basis on
which the validity of all the other arguments is derived.

A given argument $\mathcal{A}\in\mathbb{A}$ may represent another argument
$\mathcal{A}^{\prime}\in\mathbb{A}$ in some way. For example, in the setting
of natural deduction (Section 3), an argument containing a detour can be
thought of as representing a natural deduction argument arising reduction _à
la_ Prawtiz [32]. Thus, we take the space of arguments to be equipped with
some _justification operators_ of the form
$j:\mathbb{A}\rightharpoonup\mathbb{A}$ that transform one argument to
another.

It may be that arguments are left _open_ in some sense. The idea is that the
argument contains all the suasive content they require but have left something
unsaid, which can be arbitrarily filled in. Returning to the case of natural
deduction (Section 3), this was the state of open derivations, which have left
the justification of their open assumptions unstated (by the very fact of them
being open). Therefore, we further equip the space of arguments with _closure
operators_ of the form $c:\mathbb{A}\rightharpoonup\mathbb{A}$, mapping
arguments to arguments.

To summarize:

######  Definition 27 (Argument Space).

An argument space is a tuple
$\mathfrak{A}:=\langle\mathbb{A},\mathbb{P},\mathcal{J},\mathcal{C}\rangle$ in
which $\mathbb{A}$ is the set of arguments, $\mathbb{P}$ is the set of proofs,
$\mathcal{J}$ is the set of justification operators
$j:\mathbb{A}\rightharpoonup\mathbb{A}$, and $\mathcal{C}$ is the set of
closure operators $c:\mathbb{A}\rightharpoonup\mathbb{A}$.

A notion of proof-theoretic validity precisely analogous to the treatment of
IPL in Section 3 follows immediately:

######  Definition 28 (Proof-theoretic Validity).

Let
$\mathfrak{A}:=\langle\mathbb{A},\mathbb{P},\mathcal{J},\mathcal{C}\rangle$ be
an argument space. An argument $\mathcal{A}$ is $\mathfrak{A}$-valid iff one
of the following holds:

  * -

it is a canonical proof — $\mathcal{A}\in\mathbb{P}$;

  * -

there is $j\in\mathcal{J}$ such that $j(\mathcal{A})$ is $\mathfrak{A}$-valid;

  * -

for any $c\in\mathcal{C}$, the closure $c(\mathcal{A})$ is
$\mathfrak{A}$-valid.

######  Example 29 (Proof-theoretic Validity for IPL).

Consider the arguments space
$\mathfrak{N}:=\langle\mathbb{A},\mathbb{D},\mathbb{P},\mathcal{J},\mathcal{C}\rangle$
in which the components are as follows:

  * $\mathbb{A}$ \-

Comprises natural deduction arguments

  * $\mathbb{P}$ \-

Comprises canonical $\mathsf{NJ}$-proofs

  * $\mathcal{J}$ \-

Comprises the reduction transformations by Prawitz [32]

  * $\mathcal{C}$ \-

Comprises maps that substitute open assumptions for derivation in a base.

The validity condition from Definition 28 instantiated to $\mathfrak{N}$ is
precisely Definition 22.

Of course, the point of the generalization of proof-theoretic validity in this
section is that other examples may be captured too.

######  Example 30 (Proof-search Games).

Consider the game-semantics of proof-search for IPL by Pym and Ritter [34];
see also work by Miller and Saurin [27]. Succinctly, a (partial) strategy is a
(partial) function that extends plays — sequences of moves — that end on an
opponent move, which satisfy certain conditions. Each strategy represents an
attempt at proof-search in $\mathsf{LJ}$. A _winning_ strategy (i.e., a
strategy satisfying certain conditions) represent a successful proof-search —
that is, proof-search that actually finds an $\mathsf{LJ}$-proof — but it may
include backtracking. We have the argument space
$\mathfrak{S}=\langle\mathbb{A},\mathbb{D},\mathbb{P},\mathcal{J},\mathcal{C}\rangle$
in which the components are as follows:

  * $\mathbb{A}$ \-

Arguments are partial strategies

  * $\mathbb{P}$ \-

Canonical proofs are winning strategies without backtracking

  * $\mathcal{J}$ \-

The justification operators collapse backtracking sections of strategies

  * $\mathcal{C}$ \-

The closure operators extends partial strategies to total strategies.

The validity condition from Definition 28 instantiated to $\mathcal{L}$
renders a strategy valid when it represents an $\mathsf{LJ}$-proof.

Suppose one has a logic and a notion of argument for that logic; for example,
IPL and natural deduction. The setup of argument spaces does not yet allow us
to relate the two. As in the case-study of Section 3, we require a function
that determines what sequents are witness by a certain argument in the space.

######  Definition 31 (Ergo).

Let $\mathfrak{A}$ be an argument space with arguments $\mathbb{A}$. An ergo
is a map from arguments to sequents, $\textsf{e}:\mathbb{A}\to\mathbb{S}$.

######  Definition 32 (Logical Argument Space).

A logical argument space (LAS) is a pair
$\mathcal{L}:=\langle\mathfrak{A},\textsf{e}\rangle$ in which $\mathfrak{A}$
is an argument space and e is an ergo.

Observe that it is the use of an ergo that turns proof-theoretic validity from
a _semantics of proofs_ into a _semantics in terms of proofs_. In Section 3,
we saw that a natural deduction argument with open assumptions $\Gamma$ and
conclusion $\phi$ has the consequence $\Gamma\triangleright\phi$; this
describes an ergo. The notion of validity of arguments renders a LAS a
characterize of _some_ logic; namely, the logic whose consequence relation
consists of all those sequents admitting valid arguments. Given a LAS
$\mathcal{L}=\langle\mathfrak{A},\textsf{e}\rangle$, we write
$\vdash_{\mathcal{L}}$ to denote the consequence relation of the logic it
induces — that is,

$\vdash_{\mathcal{L}}s\qquad\mbox{iff}\qquad\mbox{there is an
$\mathfrak{A}$-valid argument $\mathcal{A}$ such that
$\textsf{e}(\mathcal{A})=s$}$

Recall that we take logics to be characterized by sequent calculi, generally
conceived (see Section 2). The relationship between the proof-theoretic
semantics and the logic is then captured by standard soundness and
completeness conditions:

######  Definition 33 (Soundness and Completeness of Sequent Calculi).

Let $\mathcal{L}$ be a LAS and let $\mathsf{L}$ be a sequent calculus over
sequents $\mathbb{S}$.

  1. -

The calculus $\mathsf{L}$ is _sound_ for $\mathcal{L}$ iff, for any sequent
$s\in\mathbb{S}$, if $\vdash_{\mathsf{L}}s$, then $\vdash_{\mathcal{L}}s$.

  2. -

The calculus $\mathsf{L}$ is _complete_ for $\mathcal{L}$ iff for any sequent
$s\in\mathbb{S}$, if $\vdash_{\mathcal{L}}s$, then $\vdash_{\mathsf{L}}s$.

Indeed, Definition 33 is just an instance of Definition 7 by taking the logic
in the latter as the one defined by the LAS.

This relates logics to argument spaces in general. It remains to relate
tactics to argument spaces. This addresses the question at the end of Section
4.2, what argument does a tactic represent? We have an interpretation from a
system of tactics to a space of arguments.

######  Definition 34 (Interpretation).

Call a functions from $\mathbb{A}$ to $\textsc{LIST}(\mathbb{A})$ an _abstract
reduction operator_ (ARO).

An interpretation of is a function $\llbracket-\rrbracket$ that maps goals to
arguments, tactics to AROs, and tacticals to functions from AROs to AROs, such
that $\tau:G\mapsto\langle[G_{1},...,G_{n}],\pi\rangle$, then
$\llbracket\tau\rrbracket(\llbracket G\rrbracket)\mapsto[\llbracket
G_{1}\rrbracket,...,\llbracket G_{n}\rrbracket]$.

######  Example 35.

Let $\tau_{\land}$ and $\tau_{\to}$ and $\fatsemi$ be as in Section 4.2. To
this setup we add the interpretation $\llbracket-\rrbracket$ which answers the
questions of what arguments are represented by what tactics.

The interpretation $\llbracket-\rrbracket$ acts on goals (i.e., IPL sequents)
$\Gamma\triangleright\phi$ by mapping them to the natural deduction argument
consisting of nodes of formulas from $\Gamma$ going directly to a node for
$\phi$. It maps tactics to their actions on arguments: For example,

$\llbracket\tau_{\to}\rrbracket(\phi\to\psi)\mapsto\raisebox{-4.30554pt}{$\psi\phi$}$

The tactical $\fatsemi$ interprets composition of rules, respecting also
discharge. Thus, we have the overall composite action:

$\llbracket\tau_{\land}\fatsemi\tau_{\to}\rrbracket(\chi\land(\phi\to\psi))=\raisebox{-12.91663pt}{
$\chi\land(\phi\to\psi)\lx@proof@logical@and\chi\phi\to\psi\psi[\phi]$ }$

This completes the framework of this paper. We have arguments and logics and
tactics, which are pairwise connected in simple, intuitive ways, faithful to
mathematical practices, but presented generally. In the next section, we
demonstrate that validity, tactical proof, and consequence are coherent
throughout the framework.

###  6.2. The Correctness Theorems

We have thus presented a tripartite framework for logic as a mathematics of
reasoning: arguments, sequent calculi, and tactics. Above we defined their
relationships. It is summarized in the following diagram:

$\textstyle{\mathcal{L}}$ValiditySoundness &
Completeness$\textstyle{\mathsf{T}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\llbracket-\rrbracket}$$\scriptstyle{\sigma}$$\textstyle{\mathsf{L}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$eProvability

Heuristically, tactics $\mathsf{T}$ represent (through an interpretation
$\llbracket-\rrbracket)$ the constructions of arguments $\mathcal{L}$ that
assert (through an ergo e) sequents of a logic and that the reasoning steps
involved are justified (through a synthesizer $\sigma)$ by the rules of a
sequent calculus $\mathsf{L}$.

By fixing a sequent calculus, we declare a notion of inference for a logic.
This notion of inference justifies a system of tactics if there is a
synthesizer. The following coherence result captures this:

######  Theorem 36.

Let $\mathsf{L}$ be a sequent calculus; let
$\mathcal{L}=\langle\mathfrak{A},\textsf{e}\rangle$ be a LAS; and let
$\mathsf{T}$ be a tactical system with achievement $\propto$. Let
$\llbracket-\rrbracket$ be an interpretation of $\mathsf{T}$ in $\mathfrak{A}$
and let $\propto$ satisfy the following coherence condition:

$\textsf{e}\llbracket G\rrbracket\propto G$

Let be $\propto$ be an $\mathsf{L}$-synthesizer for $\mathsf{T}$, then the
application of a tactic corresponds precisely to an inference in $\mathsf{L}$
— that is, if $\llbracket\tau\rrbracket:\llbracket
G\rrbracket\mapsto[\llbracket G_{1}\rrbracket,...,\llbracket
G_{n}\rrbracket]$, then there is an $\mathsf{L}$-rule witnessing the
following:

$\textsf{e}\llbracket G\rrbracket\lx@proof@logical@and\textsf{e}\llbracket
G_{1}\rrbracket\ldots\textsf{e}\llbracket G_{n}\rrbracket$

###### Proof.

By Definition 34, if $\tau:G\mapsto\langle[G_{1},...,G_{n}],\pi\rangle$, then
$\llbracket\tau\rrbracket:\llbracket G\rrbracket\mapsto[\llbracket
G_{1}\rrbracket,...,\llbracket G_{n}\rrbracket]$. By the coherence condition:
$\pi:[\textsf{e}\llbracket G_{1}\rrbracket,...,\textsf{e}\llbracket
G_{n}\rrbracket]\mapsto\textsf{e}\llbracket G\rrbracket$. Since $\propto$ is a
synthesizer, the result follows from Definition 26. ∎

######  Corollary 37.

Calculus $\mathsf{L}$ is sound for $\mathcal{L}$.

###### Proof.

Theorem 36 states that every rule in $\mathsf{L}$ is admissible for the logic
induced by $\mathcal{A}$, which is the soundness condition in Definition 33. ∎

In this way, a sequent calculus characterizes inference, and a tactical system
characterizes the construction of arguments. This means that the notion of
inference for a logic can be as rough or as refined as one desires. For
example, one may take the trivial sequent calculus for a consequence relation,
which has the consequence of the logic as axioms, but then one admits no
tactics. Importantly, one has no way of constructing arguments. Though
permissible, this situation is quite degenerate. Instead, one may use some
notion of argument to inform what inferences are to be permitted.

We have thus shown that the tripartite framework captured by tactical proof
and proof-theoretic semantics is coherent in the sense that arguments, sequent
calculi, and tactics have the expected relationship. As stated in Section 1,
this framework does not arise from doxastic considerations of what these
things should be but rather from how they are used in practice. We have so far
been led by a heuristic account and now justify it by a series of examples
drawn from the literature on logic.

###  6.3. Examples of the Framework

We provide a brief survey of how various proof-search activities in the
literature are instances of the framework in this paper. This survey is far
from complete and left at a quite high level as it only illustrates the
descriptive power of the framework we have presented — namely, the
relationship between proof-theoretic validity of arguments and inference as
witnessed through the reductive logic carried by tactical proof. Of course, in
addition, there are also the examples of natural deduction (Example 29)
dialogue games (Example 30) in Section 6.1.

######  Example 38 (Focused Systems).

The problem of proof-search is handling the various choices involved, such as,
_inter alia_ , the choice of a rule to use and the choice of an instance of
that rule. This problem motivates the concept of _focused_ proof-search,
introduced by Andreoli [1], where these things are largely determined. We
review a typical approach (see, for example, Chaudhuri [9, 8] and Gheorghiu
and Marin [16]) for studying focusing.

One begins a sequent calculus $\mathsf{L}$ for which one wishes to establish
the focusing property (i.e., that the class of focused proofs is complete for
the logic). One introduces an augmented version $\mathsf{FL}$, called the
focused system, which arises from enriching the original calculus with control
structures and introducing $\mathsf{cut}$. In the framework of this paper, we
can describe the situation as follows: one has a system of tactics
$\mathsf{T}$ that is validated by $\mathsf{L}$ (i.e., one has a synthesizer
from $\mathsf{T}$ to $\mathsf{L}$) such that a tactic is interpreted as an
$\mathsf{FL}$-proof. The space of arguments contains all $\mathsf{FL}$-proofs,
and the justification operators are given by cut-reduction. This is set up
such that the canonical proofs then represent _focused_ $\mathsf{L}$-proofs.

######  Example 39 (Hyper-sequent Calculi).

Reasoning in substructural and modal logics is often difficult because they
seemingly do not admit analytic sequent calculi that do not have extra-logical
structures (e.g., labels). Many such logics do admit _hyper_ -sequent calculi;
that is, calculi over finite multisets of sequents — see, for example, Baaz et
al. [2] and Ciabattoni et al. [10]. We can use the framework of this paper to
describe the relationship of hyper-sequent calculi to the logic.

One has a system of tactics $\mathsf{T}$ of goals that are hyper-sequents such
that the tactics are interpreted as reductions in the hyper-sequent calculus.
These tactics are valid relative to a notion of achievement defined as
follows: a consequence of the logic achieves a hyper-seqeunt iff it is among
the sequents in the multiset.

######  Example 40 (Analytic Tableaux).

Analytic tableaux give a computationally useful paradigm of proof in logic. It
has been extensively treated for modal logic (see, for example, Fitting and
Mendelsohn [15]) and has been used to provide a uniform and modular proof
theory for the family of bunched logics (see Docherty and Pym [12, 11]).
Typically, these systems make use of prefixed signed formulas. The framework
of this paper can be used to describe the relationship between a tableaux
system and a logic.

One has a system of tactics $\mathsf{T}$ whose goals are prefix signed
formulas and whose tactics represent expansion rules for the system, and
tacticals are sequential composition. These tactics are interpreted in the
space of arguments containing the tableaux, in which the canonical proofs are
closed tableaux, possibly satisfying a particular expansion scheme. The
tactical system is valid relative to a notion of inference supplied by a
_relational_ sequent calculus in the form of Negri [29] and Gheorghiu and Pym
[17].

##  7\. Conclusion

Typically, when logics are used as a reasoning technology in informatics and
other systems-oriented sciences — for example, the use of logic in program and
system verification, natural language processing, knowledge representation,
and proof assistants — it is through the paradigm of reductive logic. That is,
when logic is employed in these fields, it is by reducing a putative
conclusion to some sufficient premisses (as opposed to the deductive view in
which a logic is understood as stating that a conclusion may be inferred from
some established premisses).

We declare a notion of inference by fixing a sequent calculus characterizing
that logic. What one constructs during backward reasoning is a certificate
which we call an _argument_. In general, these arguments are abstract
mathematical entities with dynamic and static properties that can be studied
in their own right. How is backward reasoning and inference in the logic
related? This question is, of course, answered in each use-case; for example,
in Section 3, we saw how (the construction of) a natural deduction argument
can be understood in terms of a sequent calculus. In this paper, we provide a
meta-theoretic framework that _uniformly_ describes these answers, thereby
showing how different deployments of logic as a reasoning tool exercise the
same underlying principles.

The essential criterion for whatever notion of _validity_ one has for a space
of arguments is that the valid arguments are precisely those that certify the
consequences of the logic. However, we are concerned about constructing
arguments according to backward inference. From this perspective, an argument
is valid because it respects a notion of inference for the logic. We use
proof-theoretic semantics in the Dummett-Prawitz tradition, grounded in
inferentialism, to give a formal definition of soundness and completeness that
captures these ideas.

The theory of tactical proof introduced by Milner [28] is a widely deployed
metalogical framework supporting reductive logic. We use tactics to represent
the construction of arguments. Specifically, each tactics represents a
backward inference step and is interpreted as an argument. A tactic is valid
(in a sense given by Milner) precisely when they respect the sequent calculus
characterizing the logic in question. This way, tactical proof formally and
generally relates arguments and inferences within reductive logic.

In summary, we have a tripartite framework for describing the use of logic as
a reasoning tool: there are arguments, sequent calculi, and tactics, and they
are related through various validity conditions. This descriptive framework is
correct in the sense that these validity conditions, which arise independently
according to how the aspects typically relate to one another, cohere. Its
descriptive power is illustrated by a series of seemingly disparate examples
that are represented uniformly.

Within the framework, we can express other semantics of reductive logic it
(e.g., the game semantics for proof-search in IPL — see Example 30), but it
remains to conduct such a study in general. Moreover, proof-search arises from
reductive logic by introducing control structures that determine what
reduction is made at what time. While the framework can witness specific
control structures in specific systems (see, for example, the treatment of
focused systems in Example 38), can it give an abstract account of what
control is? These questions remain to be studied.

### Acknowledgements

We are grateful Tao Gu and the reviewers of an earlier version of this paper
for their comments and feedback, which have helped to produce the present
paper.

## References

  * [1] J.-M. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of logic and Computation, 2 (1992), pp. 297–347.
  * [2] M. Baaz, A. Ciabattoni, and C. G. Fermüller, Hypersequent Calculi for Gödel Logics — A Survey, Journal of Logic and Computation, 13 (2003), pp. 835–861.
  * [3] H. Barendregt, Introduction to generalized type systems, Journal of Functional Programming, 1 (1991), pp. 125–154.
  * [4] R. Brandom, Articulating Reasons: An Introduction to Inferentialism, Harvard University Press, 2000.
  * [5] L. E. J. Brouwer, Intuitionism and Formalism, Bulletin of the American Mathematical Society, 20 (1913), pp. 81–96.
  * [6] A. Bundy, The Computer Modelling of Mathematical Reasoning, Academic Press Professional, Inc., 1985.
  * [7] J. Cartmell, Generalised Algebraic Theories and Contextual Categories, PhD thesis, Oxford University, 1978.
  * [8] K. Chaudhuri, S. Marin, and L. Straßburger, Focused and Synthetic Nested Sequents, in International Conference Foundations of Software Science and Computation Structures — FoSSaCS, B. Jacobs and C. Löding, eds., Eindhoven, Netherlands, 2016, Springer.
  * [9] K. Chaudhuri, S. Marin, and L. Straßburger, Modular Focused Proof Systems for Intuitionistic Modal Logics, in International Conference on Formal Structures for Computation and Deduction — FSCD, Schloss Dagstuhl \- Leibniz-Zentrum fuer Informatik, 2016.
  * [10] A. Ciabattoni, N. Galatos, and K. Terui, From Axioms to Analytic Rules in Nonclassical Logics, in Symposium on Logic in Computer Science — LICS, 2008, pp. 229–240.
  * [11] S. Docherty, Bunched logics: A Uniform Approach, PhD thesis, University College London, 2019.
  * [12] S. Docherty and D. Pym, Modular Tableaux Calculi for Separation Theories, in International Conference on Foundations of Software Science and Computation Structures — FoSSaCS, Springer, 2018, pp. 441–458.
  * [13] M. Dummett, The Logical Basis of Metaphysics, Harvard University Press, 1991.
  * [14] F. B. Fitch, Symbolic Logic: An Introduction, Ronald Press Co, 1952\.
  * [15] M. Fitting and R. L. Mendelsohn, First-order Modal Logic, Springer, 2012\.
  * [16] A. Gheorghiu and S. Marin, Focused Proof-search in the Logic of Bunched Implications, in Foundations of Software Science and Computation Structures — FoSSaCS, S. Kiefer and C. Tasson, eds., Springer, 2021, pp. 247–267.
  * [17] A. V. Gheorghiu and D. J. Pym, Defining Logical Systems via Algebraic Constraints on Proofs.  https://arxiv.org/abs/2301.02125, 2023.
  * [18] A. Heyting, Intuitionism: An Introduction, Cambridge University Press, 1989.
  * [19] M. Hofmann, Syntax and semantics of dependent types, in Semantics and Logics of Computation, A. M. Pitts and P. Dybjer, eds., Publications of the Newton Institute, Cambridge University Press, 1997, p. 79–130.
  * [20] W. A. Howard, The Formulae-as-Types Notion of Construction, in To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, vol. 44, Academic Press London, 1980, pp. 479–490.
  * [21] B. Jacobs, Categorical Type Theory, PhD thesis, The University of Nijmegen, 1991.
  * [22] A. Kolmogorov, Zur deutung der intuitionistischen logik, Mathematische Zeitschift, 35 (1932).
  * [23] R. Kowalski, Logic for Problem-Solving, North-Holland Publishing Co., 1986.
  * [24] J. Lambek, From $\lambda$-calculus to Cartesian Closed Categories, in To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press London, 1980, pp. 375–402.
  * [25] E. J. Lemmon, Beginning Logic, Hackett Publishing, 1978.
  * [26] P. Martin-Löf, An Intuitionistic Theory of Types: Predicative Part , in Studies in Logic and the Foundations of Mathematics, vol. 80, Elsevier, 1975, pp. 73–118.
  * [27] D. Miller and A. Saurin, A Game Semantics for Proof Search: Preliminary Results, in Proceedings of the Conference on Mathematical Foundations of Programming Semantics — MFPS, vol. 155, Elsevier, 2006, pp. 543–563.
  * [28] R. Milner, The Use of Machines to Assist in Rigorous Proof, Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences, 312 (1984), pp. 411–422.
  * [29] S. Negri, Proof Analysis in Modal Logic, Journal of Philosophical Logic, 34 (2005), pp. 507–544.
  * [30] D. Pavlović, Predicates and Fibrations, PhD thesis, University of Utrecht, 1990.
  * [31] G. Polya, How to solve it, Princeton university press, 1945.
  * [32] D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Dover Publications, 1965.
  * [33] D. J. Pym and E. Ritter, Reductive logic and Proof-search: Proof Theory, Semantics, and Control, vol. 45 of Oxford Logic Guides, Oxford University Press, 2004.
  * [34] , A Games Semantics for Reductive Logic and Proof-search, in GALOP @ ETAPS, 2005, pp. 107–123.
  * [35] P. Schroeder-Heister, Validity Concepts in Proof-theoretic Semantics, Synthese, 148 (2006), pp. 525–571.
  * [36] , Proof-Theoretic versus Model-Theoretic Consequence, in The Logica Yearbook 2007, M. Pelis, ed., Filosofia, 2008.
  * [37] , Proof-Theoretic Semantics, in The Stanford Encyclopedia of Philosophy, E. N. Zalta, ed., Metaphysics Research Lab, Stanford University, Spring 2018 ed., 2018.
  * [38] R. A. Seely, Hyperdoctrines, Natural Deduction and the Beck condition, Mathematical Logic Quarterly, 29 (1983), pp. 505–542.
  * [39] T. Streicher, Correctness and completeness of a categorical semantics of the calculus of constructions, PhD thesis, University of Passau, 1988.
  * [40] M. E. Szabo, ed., The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company, 1969.
  * [41] N. Tennant, Entailment and Proofs, Proceedings of the Aristotelian Society, 79 (1978), pp. 167–189.
  * [42] A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, vol. 43 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2000.
  * [43] M. van Atten, The Development of Intuitionistic Logic, in The Stanford Encyclopedia of Philosophy, E. N. Zalta, ed., Metaphysics Research Lab, Stanford University, Summer 2022 ed., 2022.
  * [44] D. van Dalen, Logic and Structure, Universitext, Springer, 2012.
  * [45] Wikipedia, Proof assistant.  https://en.wikipedia.org/wiki/Proof_assistant.