Semantic Foundations of Reductive Reasoning

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 from a given formal system that determine that an inference of a conclusion from a collection of premisses has been established.

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 backwards. Read from conclusion to premisses, the rules are sometimes called reduction operators, and denoted with sufficient premisses above and putative conclusion below.

We call the constructions in a system of reduction operators reductions. This proof-theoretic formulation has been dubbed reductive logic (Pym and Ritter 2004). Note that reductive logic is not a logic in the sense of, for example, classical, intuitionistic, or modal logic, but a conception of logic in the sense of deductive, inductive, or abductive logic. To clarify, reductive logic is defined with respect to a formal specification of a logic and does not encompass semantic reasoning in general. Specifically, the figures above illustrate particular inferences within formal systems, rather than arbitrary steps of problem-solving. As such, reductive logic represents a relatively narrow domain within the broader field of analysis (Beaney and Raysmith 2024). More precisely, it pertains to the aspects of analysis employed in computer-assisted formal reasoning, as we discuss below.

Also to avoid confusion, note that reductive logic should not be conflated with the superficially related concept of reverse mathematics, as developed by Friedman (1975) and others. Reverse mathematics investigates which axioms, within a given formalization of mathematics, are necessary for specific theorems to hold. By contrast, reductive logic focuses on the proof theory and semantics underlying the process of finding proofs—via reduction and search—within fixed systems of logic.

Focusing on areas with formal, well-defined notions of inference allows us to develop a more concrete semantic theory of reductive reasoning. Specifically, our aim is to create a semantics of reductions that not only identifies complete proofs but also clarifies the meaning of unfinished or incomplete proof-searches. This approach places our investigation squarely within the domain of proof-theoretic semantics (P-tS), which seeks to explain the validity of proofs in formal logic. So far, P-tS has largely been developed in the context of deductive logic. We have argued that it is a natural and metaphysically well-motivated semantic framework that is explanatory for both reductive and deductive logic. We therefore argue that this suggests that these two views of formal logic are as valid as each other as ways of modelling reasoning.

For a comprehensive treatment of P-tS, we refer to Schroeder-Heister (2006, 2008), though we provide the key highlights here. While P-tS is typically framed in the context of deductive logic, its core principles are directly applicable to reductive reasoning. In the Dummett-Prawitz tradition of P-tS—perhaps the most extensively studied—direct proofs (closed, normalized proofs) are considered canonically valid, whereas indirect proofs rely on transformations to achieve directness. This distinction introduces a technical separation between proof structures, which represent potential proofs, and justifications, which define the transformations that validate them. Similarly, in reductive reasoning, several steps of reduction may yield a potential proof or contribute proof-theoretic content, even if additional manipulation and transformation are required to achieve the final proof of the intended goal—that is, the putative conclusion one desires to prove.

Naïvely, reductive logic may appear simply as deductive logic read backwards. This heuristic suffices in many cases and is useful for understanding deductive logic; for example, proof of cut-elimination for sequent calculi (see Szabo 1969) can be understood from this perspective. However, the space of reductions studied in reductive logic is larger than the space of proofs, as studied in deductive logic: while the reductive system can simply reconstruct all the correct proofs in the underlying system, it also allows choices to be made that yield reductions that do not correspond to proofs. For example, when no further reduction operators can be applied to a premiss and that premiss is not an axiom of the logic. Reductive logic is thus a paradigm of logic in parallel to deductive logic and cannot be defined purely in terms of it.

While the restriction to proof systems may seem limiting, the conception of reductive logic in this paper is sufficiently general to encompass reasoning activities as diverse as proving a formula in a formal system and seeking to meet a friend before noon on Saturday. Importantly, it more closely resembles what mathematicians do when proving theorems and, more generally, how people solve problems using formal representations. It is also the paradigm of logic used for diverse applications in informatics and other systems-oriented sciences, including, but not limited to, areas such as program and system verification, natural language processing, and knowledge representation. It is the reductive perspective that underpins the use of logic in proof-assistants—for example, LCF (Gordon et al. 1979), HOL (Gordon and Melham 1993), Isabelle (Paulson 1994), Coq (Coq Team 2024; Bertot and Castéran 2004), Twelf (Frank Pfenning et al. 2024; Pfenning and Schürmann 1999), and more. More generally, it is a restricted model of human reasoning, which is discussed extensively, for example, in the work of Kowalski (1986) and Bundy (1985). We discuss this further in Sect. 3.

We seek a semantic foundation for reduction operators. Our motivation is both philosophical and pragmatic. Philosophically, we recognize that reductive logic is a paradigm through which much practical problem solving occurs, as discussed above (examples below). Pragmatically, the increasing significance of technologies reliant on reductive logic suggests the pressing need for a more comprehensive and mathematically more developed semantic theory than currently available—see, for example, Pym and Ritter (2004). Hence, in particular, we seek a representation of reduction operators as functions encapsulating the action suggested by the picture above,

$$\text{Putative Conclusion} \;\longrightarrow\; \text{Sufficient Premiss}_1, \ldots, \text{Sufficient Premiss}_n$$

Having done this, we can then analyze them and formally study reductive reasoning. It is not only the representation of reduction operators as mathematical objects that is important: we seek an account of what makes a reduction operator and its deployment valid.

Historically, semantics in logic has been dominated by the paradigm of denotationalism, where the meaning of logical structures is given in terms of abstract interpretations. For instance, in model-theoretic semantics, propositions are interpreted relative to abstract algebraic structures called models (see Schroeder-Heister 2008). This paradigm is suitable for deductive logic. However, other paradigms of logic may benefit from different approaches.

For reductive logic, denotationalist accounts have been useful and thoroughly explored (see Pym and Ritter 2004, Komendantskaya et al. 2011; Komendantskaya and Power 2011; Komendantskaya et al. 2016, and Gheorghiu et al. (2023a)). These studies are discussed below. In this paper, we generalize these results by removing auxiliary and domain-specific aspects to concentrate on the semantics of reductive reasoning itself.

We also examine semantics with a proof-theoretic focus, this is the connection to P-tS. That is, we give validity conditions not in terms of abstract algebraic structures, but in terms of what 'proofs' are being witnessed during reductive reasoning. Pym and Wallen (1993) provided such an account in terms of proof-valued computations.

To this end, we draw substantively upon Milner's theory of tactical proof (Milner 1984) in Sect. 4. The historical and technical significance of tactical proof in the context of computer-assisted formal reasoning is profound; it forms the basis for almost all proof assistants (see Gordon 2015). Ultimately, this inspires the P-tS account of reductive logic in this paper.

We begin, in Sect. 2, by explicating the notion of reduction and its current semantics in comparison to well-established techniques in deductive logic. This helps expose the subtlety and challenges involved in reductive logic. In Sect. 3, we provide a denotational semantics of the reduction operators and soundness and completeness conditions that determine the validity of a set of reduction operators. In Sect. 4, we give an operational account of reduction operators in terms of structural operational semantics that enables a more refined account of their use and validity. In Sect. 5, we discuss future problems for a satisfactory foundation of reductive reasoning; viz., the expression and semantics of strategies for proof-search. This moves us from a semantic foundation of reduction operators, which we may think of as the local perspective on reduction reasoning, to a full semantic foundation of reductive logic, the corresponding global perspective on reductive logic. The paper ends in Sect. 6 with a summary of the results obtained.

This paper should be seen as a companion to Gheorghiu and Pym (2023a), in which P-tS is used to provide a semantics for tactical proof, mentioned above. By contrast, this paper provides a general foundation for reductive reasoning in terms of P-tS and obtains tactical proof as a significant instance. Happily, the two analyses are mutually coherent.

Technical Background. We assume familiarity with formal logic (see, for example, van Dalen 2012) and basic proof theory (see, for example, Troelstra and Schwichtenberg 2000 and Negri (2005)). We use $\phi, \psi, \chi, \ldots$ to denote logical formulae and $\Gamma, \Delta, \ldots$ to denote collections thereof. We use $\vdash$ as the sequent symbol and we distinguish it from the consequence judgement $\models$ of a logic; that is, a sequent is an expression of an assertion in a logic, which may be valid or invalid, but a consequence is an assertion that is valid.

For the technical portions of this paper, we will assume some basic concepts and terminology from category theory— see, for example, Cheng (2022)—in particular, categories, functors, adjunctions, and natural transformations. However, these technical details are not essential for the thesis, they simply give a systematic mathematical treatment of the ideas presented. As we are always working in the category of sets and (partial) functions, relatively little background is required beyond typical mathematical training.

We use $\mathcal{P}_{<\omega}$ to denote the finite powerset functor—that is, given a set $X$, we write $\mathcal{P}_{<\omega}(X)$ to denote the set of all finite subsets of $X$—and $\mathrm{list}$ to denote the list functor—that is, given a set $X$, we write $\mathrm{list}(X)$ to denote the set of all finite lists of $X$. We will use the concept of $F$-algebra and $F$-coalgebra (for a functor $F$) in various parts of this paper, but they are just functions.¹ The nomenclature of category theory enables us to apply well-established techniques and constructions. For a general introduction to coalgebra, see, for example, Rutten (2000) and Jacobs (2017). We use basic co-induction in some definitions and proofs and, accordingly, give a brief explanation of how it works presently; for a more detailed discussion, see, for example, Barwise and Moss (1996) and Rutten (2000). We have to use co-induction (as opposed to induction) because reduction spaces are co-recursively generated and so may be infinite objects. We follow Reitzig (2012) for a succinct explanation of co-induction as the dual of induction.

In an inductive definition of a set, one begins with some base elements and applies constructors that say how one builds new elements of the set from existing ones. For example, a set of finite sequences, or 'strings', $S$ may be defined by the following:

$$\varepsilon \in S \quad \text{(Base Case)} \qquad w \in S \Rightarrow aw \in S \quad \text{(Condition 1)} \qquad aw \in S \Rightarrow baw \in S \quad \text{(Condition 2)}$$

The set $S$ inductively defined in this way is the smallest set satisfying these conditions. Hence, as defined above, $S$ is the set of strings of $a$ and $b$ with no two subsequent $b$s. This is a perfectly adequate account of induction, but one can give a more subtle treatment that explains precisely how it works in terms of fixed points.

¹ $F$-algebras generalize the notion of algebraic structure. If $\mathbf{C}$ is a category and $F : \mathbf{C} \to \mathbf{C}$ is an endofunctor, then an $F$-algebra is a pair $(A, \alpha)$, where $A$ is an object of $\mathbf{C}$ and $\alpha : F(A) \to A$ is a morphism in $\mathbf{C}$. $A$ is called the carrier of the algebra. If we take $\alpha : A \to F(A)$, then we have an $F$-coalgebra. For endofunctors $F$ on the category of sets, $F$-algebras are functions on the carrier set and $F$-coalgebras are countably infinite streams (sequences) over the carrier set. Often, we refer to the maps $\alpha$ as (co)algebras.

The definition above determines the following map $f$ on sets of strings,

$$f(X) := X \cup \{\varepsilon\} \cup \{aw \mid w \in X\} \cup \{baw \mid aw \in X\}$$

Observe that $f$ is monotone and the sets of strings form a complete lattice under set inclusion. Hence, the Knaster-Tarski Theorem (Knaster and Tarski 1928; Tarski 1955) tells us that the set of fixed points for $f$ forms a complete lattice. The defined set $S$ is the least fixed point; that is, the smallest set $X$ such that $f(X) = X$. Since $f$ is continuous, $S$ is the colimit of the following $\omega$-chain,

$$\emptyset \longrightarrow \emptyset \cup f(\emptyset) \longrightarrow \emptyset \cup f(\emptyset) \cup f(f(\emptyset)) \longrightarrow \cdots \longrightarrow S = \bigcup_n f^n(\emptyset)$$

Here each arrow denotes an application of $f$ and $S$ denotes the colimit of the chain. For a co-inductive definition, we use destructors rather than constructors. Intuitively, we reverse the implications in the inductive definition; observe that in doing so the 'base case' becomes vacuous. That is, rather than say 'if $w$ is included, then so is $aw$', we say 'if $aw$ is included, then so was $w$'. This determines a set $S^\dagger$ with the following property: we can take arbitrarily long prefixes away from any word in $S^\dagger$ and remain in $S^\dagger$. Observe that this property does not hold for finite strings, hence the co-inductive definition requires us to consider infinite strings. While induction determines the least fixed point satisfying $f$, the co-inductive definition determines the (unique) greatest fixed point—that is, the largest set $X$ such that $f(X) = X$. Thus $S^\dagger$ contains all infinite strings of $a$ and $b$ with no consecutive occurrences of $b$s. In other words, it is the limit of any $\omega^{\mathrm{op}}$-chain,

$$1 \longleftarrow f(1) \longleftarrow f(f(1)) \longleftarrow f(f(f(1))) \longleftarrow \cdots$$

in which $1$ is a singleton (i.e., a terminal object in the category), and the arrows denote the duals of the arrows in the least fixed point case (i.e., the unique morphisms that remove a prefix from a string).

This is quite intuitive: we cannot construct $S^\dagger$ by an iterative process on elements as its elements are infinite, so instead we determine it by starting with all strings and removing those that do not satisfy the conditions after an arbitrary amount of time. This concludes the background on co-induction.

2 The Semantics of Reductive Logic

In this section, we motivate the idea of reductive logic and explicate its current semantics. We set this discussion in the historical development of intuitionistic logic (IL) (van Atten 2022) as it is here that the ideas are well known and are the most developed. Subsequently, in Sect. 3 and Sect. 4, we address the semantics of reduction operators, the things that generate reductions.

In logic, we have structures called arguments that represent evidence for a consequence of a logic—for example, natural deduction arguments after Szabo (1969), after Fitch (1952), after Lemmon (1978), and so on. When these arguments are valid they represent a proof of some statement. The semantics of proofs for particular logics have been very substantially developed for particular logics. Perhaps the best example is the BHK interpretation of intuitionism. Intuitionism, as defined by Brouwer (1913), is the view that an argument is valid when it provides sufficient evidence for its conclusion. This is IL. Famously, as a consequence, IL rejects the law of the excluded middle—that is, the metatheoretic statement that either a statement or its negation is valid. This law is equivalent to the principle that, in order to prove a proposition, it suffices to show that its negation is contradictory. In IL, such an argument does not constitute sufficient evidence for its conclusion.

Heyting (1989) and Kolmogorov (1932) provided a semantics for intuitionistic proof that 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 (2022). The propositions-as-types correspondence—see Howard, Barendregt, and others (Howard 1980; Barendregt et al. 2013; Barendregt 1991, 1993)—gives a standard way of instantiating the denotations of proofs in the BHK interpretation of intuitionistic propositional logic (IPL) as terms in the simply-typed $\lambda$-calculus. Technically, the set-up can be sketched as follows: a judgement that $D$ is an NJ-proof of the sequent $\phi_1, \ldots, \phi_k \vdash \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 $D$, and the type $A$ corresponds to $\phi$.

Lambek (1980) gave a more abstract account by showing that the simply-typed $\lambda$-calculus is the internal language of cartesian closed categories (CCCs), thereby giving a categorical semantics of proofs for IPL. In this set-up, a morphism $\phi_1 \times \cdots \times \phi_k \xrightarrow{D} \phi$ in a CCC, where $\times$ denotes cartesian product, that interprets the NJ-proof $D$ of $\phi_1, \ldots, \phi_k \vdash \phi$ also interprets the term $M$.

Altogether, this describes the Curry-Howard-Lambek correspondence for IPL. It may be summarized by Fig. 1 in which:

• $D \Rightarrow_\Gamma \phi$ denotes that $D$ is an NJ-derivation of $\phi$ from $\Gamma$;
• $x : A \vdash M(x) : A_\phi$ denotes a typing judgment, as described above, corresponding to $D$; and,
• $\Gamma \xrightarrow{D} \phi$ denotes that $D$ is a morphism from $\Gamma$ to $\phi$ in a CCC.

To generalize to full IL (and beyond), Seely (1983) modified this categorical set-up and introduced hyperdoctrines—indexed categories of CCCs with coproducts over a base with finite products. Martin-Löf (1975) gave a formulae-as-types correspondence for predicate logic using dependent type theory. Barendregt (1991) gave a systematic treatment of type systems and the propositions-as-types correspondence. A categorical treatment of dependent types came with Cartmell (1978)—see also, for examples among many, work by Streicher (1988), Pavlović (1990), Jacobs (1991), and Hofmann (1997). In total, this gives a semantic account of proof for first- and higher-order predicate intuitionistic logic based on the BHK interpretation.

This is all very well for explaining what is a proof in IL. In reductive logic, however, the space of objects considered contains also things that are not proofs and cannot be continued to form proofs. Pym and Ritter (2004) 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 generalization of the BHK interpretation is known as the constructions-as-realizers-as-arrows correspondence in Fig. 2:

• $\Sigma \Rightarrow_\Gamma \phi$ denotes that $\Sigma$ is a sequence of reductions for the sequent $\Gamma \vdash \phi$;
• $[\,][\,] : [\phi]$ denotes that $[\,]$ is a realizer of $[\phi]$ with respect to the assumptions $[\,]$; and,
• $\Gamma \xrightarrow{\Sigma} \phi$ denotes that $\Sigma$ is a morphism from $\Gamma$ to $\phi$ in the appropriate polynomial category.

They also defined a judgement $w \vdash (\Sigma : \phi)$ which says that $w$ is a world witnessing that $\Sigma$ is a reduction of $\phi$ to $\Gamma$, relative to the indeterminates of $\Gamma$. What has just been presented gives a semantics of reductions that explicates how they relate to proofs and certify the validity of sequents. In this paper, we turn to the semantics of the reduction operators themselves; that is, the things which generate the reductions. Unlike rules, which specify particular transformations, reduction operators contain a certain degree of non-determinism rendering the subject more subtle.

3 Reduction Operators I—Denotational Semantics

In this section, we give a denotational semantics of reduction operators beginning from first principles. We then use this semantics to express the space of reductions.

3.1 Denotational Semantics

As described in Sect. 1, reductive logic is concerned with 'backwards' inference. This framework not only describes reduction in a formal system but also applies to reductive reasoning in more general settings.

$$\frac{\text{Sufficient Premiss}_1 \quad \cdots \quad \text{Sufficient Premiss}_k}{\text{Putative Conclusion}} \tag{$\dagger$}$$

3.2 The Space of Reductions

While we have modelled 'reduction' through the use of operators and said something about how they compose to form reductive reasoning, we can be much more precise about the space of exploration during reductive reasoning. This space, the space of reductions, is larger than the space of deductions—that is, the space of objects studied in deductive logic; for example, the class of proofs in a fixed proof-system—as it also contains 'failed' or 'incomplete' reductions—that is, reductions failing to satisfy condition T1.

To model the space of reductions for a given goal $G \in \mathit{GOALS}$, we move from considering individual reduction operators to considering all possible reductions as different sets of sets of sufficient premisses. Let RED denote the set of reduction operators given in $R_1$'. We define a single destructor for RED representing the collected action of all the reduction operators that apply at any point,

$$\partial : \mathit{GOALS} \to \mathcal{P}_{<\omega}\!\left(\mathcal{P}_{<\omega}(\mathit{GOALS})\right)$$

with the action $\partial : G \mapsto \{\rho(G) \mid \rho \in \mathrm{RED}\}$ — recall that RED is finite and each $\rho \in \mathrm{RED}$ is a $\mathcal{P}_{<\omega}$-coalgebra. Using $\partial$, one can define the space of reductions for a goal $G$ as a limit of $\partial$ applied to a given goal:

This completes the construction of the space of reductions.

3.3 Soundness and Completeness

Let $L$ be a deductive system over $\mathit{GOALS}$. We elide details of $L$ as they do not matter; concrete examples include natural deduction systems, sequent calculi, tableaux systems, and so on. Fix a logic $L$. We have the following soundness and completeness conditions:

• (Soundness) $L$ is sound for $L$ if, for any goal $G \in \mathit{GOALS}$, if $G$ admits a proof in $L$, then $G$ is valid in $L$.
• (Completeness) $L$ is complete for $L$ if, for any goal $G \in \mathit{GOALS}$, if $G$ is valid in $L$, then $G$ admits a proof in $L$.

For the remainder of this section, we take a fixed $L$ that is sound and complete for a fixed logic $L$. We can define the correctness of RED relative to a calculus $L$ as follows:

• (Faithfulness) RED is faithful for $L$ if, for any goal $G \in \mathit{GOALS}$ and any $\rho \in \mathrm{RED}$, if $\rho(G) = \{G_1, \ldots, G_n\}$, then there is a rule in $L$ from $G_1, \ldots, G_n$ to $G$.
• (Adequacy) RED is adequate for $L$ if, for any goal $G \in \mathit{GOALS}$, if there is a rule from $G_1, \ldots, G_n$ to $G$ in $L$, then there is a reduction operator $\rho \in \mathrm{RED}$ such that $\rho(G) = \{G_1, \ldots, G_n\}$.

Relative to this set-up, the validity of reduction we automatically have soundness and completeness of RED with respect to $L$:

4 Reduction Operators II—Operational Semantics

In Sect. 3, we provided a denotational semantics for reduction operators from first principles. This enables the representation of reductive reasoning. In this section, we present a corresponding operational semantics, allowing for a more refined analysis that provides a subtle and expressive account of reduction-operator usage.

4.1 Operational Semantics

In this section, we introduce structural operational semantics (SOS) for reduction and reduction operators. Originally introduced by Plotkin (1981) to define the behaviour of programming constructs, SOS uses formal rules to describe how each part of a program manipulates a state to yield a new state. It adopts a meaning-as-use approach, where 'use' implies 'behaviour'. For our purposes, we focus on one of the most extensively studied rule formats for SOS: the format of general structural operational semantics (GSOS) as defined by Bloom et al. (1995). We represent a state as a (finite) list of current goals, where $G \in \mathit{GOALS}$,

$$S \;::=\; \varepsilon \;\mid\; G :: S$$

Intuitively, $\varepsilon$ denotes the empty string. We may write $[G_1, \ldots, G_n]$ to denote the list $G_1 :: (\cdots :: G_n)$.

We have a countable collection of action labels $A$ and a reduction operator $\rho$ is the transformation of a goal $G$ into a list of subgoals $[G_1, \ldots, G_n]$,

$$G \xrightarrow{\rho} [G_1, \ldots, G_n] \tag{$\Uparrow\partial$}$$

The set of reduction operators RED from Definition $R_1$' can be seen as comprising all such rules. Notably, while Sect. 3 used finite sets, we now work with finite strings due to syntactic considerations. We model the free choice of goal reduction by adding the following for all $\rho \in A$:

$$\frac{G \xrightarrow{\rho} [G_1, \ldots, G_n]}{G \longrightarrow [G_1, \ldots, G_n]} \tag{$\uparrow\rho$}$$

This behaviour extends to states with more than one element via the following rules:

$$\frac{S_1 \longrightarrow S_1' \qquad S_2 \longrightarrow S_2'}{S_1 :: S_2 \longrightarrow S_1' :: S_2'} \tag{$\uparrow$}$$

The operational semantics of reduction comprises the collection of all such rules,

$$O := \mathrm{RED} \cup \{\uparrow\} \cup \{\uparrow\rho \mid \rho \in A\}$$

This system enables us to describe the process of reduction as a 'computation' in $O$.

4.2 The Theory of Tactical Proof

A foundational framework that supports the mechanization of reductive logic is the theory of tactical proof. It systematically underpins the proof-assistants mentioned in Sect. 1. The centrality of tactical proof to computer assisted formal reasoning cannot be understated—see, for example, Gordon (2015). Its efficacy is that it allows users to articulate insight into reasoning methods and delegate routine but possibly error-prone work to machines. The theory clarifies how concepts such as 'goal', 'strategy', 'achievement', 'failure', etc., interrelate during reductive reasoning. In this section, we observe that tactical proof can be viewed as a semantics of reduction operators.

To simplify the operational semantics, we define a set of primary entities called goals ($\mathit{GOALS}$) and reduction operators given by mappings:

$$\rho : \mathit{GOALS} \to \mathrm{list}(\mathit{GOALS})$$

Milner (1984) extends this set-up by introducing another set of primary entities called events ($\mathit{EVENTS}$) and an achievement relation $\propto$, which specifies how events witness goals:

$${\propto} \;\subseteq\; \mathit{GOALS} \times \mathit{EVENTS}$$

This allows us to express that certain events satisfy certain goals.

5 Control Régimes

While in the space of proofs, a rule takes a list of premisses and derives a single conclusion, navigating the space of reductions involves many choices that impact the validity of the resulting construction. We refer to all the strategic aspects of managing search in reductive logic as 'control'.

Proof-search = Reductive Logic + Control

It is control that determines the efficacy of proof-search procedures: some procedures will be complete, some not; some will affect the shape of proofs being found, and some will affect the complexity of the procedure. The more control structure provided, the more work that is delegated: mechanical problem-solving begets algorithmic theorem-proving techniques, which beget a programming language paradigm known as logic programming (LP). A well-known example of this is provided by implementations of the logic programming language Prolog, in which the typical strategy is 'leftmost literal first' in SLD resolution—see, for example, Kowalski and Kuehner (1971) and Plaisted and Zhu (1997). So central are these problems to the use of reductive logic that control is surely a first-class citizen.

How can we represent and reason about control régimes? We have seen that it is possible to extend the operational semantics for reduction with a process calculus, allowing for a flexible way to express control flow during reduction. This setup is more expressive than what can be achieved through the composition of reduction operators (or tactics):

while sequential composition ($;$) can be modelled by a composition of reduction operators, non-deterministic choice ($+$) cannot.

Arguably, $C_1$ and $C_2$ are not aspects of reduction operators but exist at a higher perspective, as they pertain to reductive reasoning rather than the steps comprising it. This is most evident in $C_2$: to backtrack, we need a notion of the sequence of reduction steps taken so far, not just the reduction operators available. Therefore, our notion of state when modelling control cannot be only the list of goals but rather a representation of the explored section of the reduction space.

Related to these control problems is the use of information from one part of the reduction to inform other parts. For example, if we find a successful reduction of a certain subgoal, we should like to reuse that information if we encounter it again during the reduction process. More interesting is how such information may be used dynamically:

6 Conclusion

While deductive logic provides a formal foundation for defining proofs through 'forwards' inference, the dual consideration of how one constructs proofs using 'backwards' inference is essential for understanding the use of logic when reasoning about a putative conclusion. This is reductive logic. It has profound implications across various fields, including program verification, natural language processing, and knowledge representation. By embracing reductive logic, we can not only enhance our understanding of formal reasoning but also develop more effective tools and methodologies for tackling complex problem-solving tasks.

This paper has explored the semantic foundations of reduction operators. They are the reductive logic analogues of rules in deductive logic. We have provided two semantic foundations for them: one denotational and one operational. While the former is conceptually simpler, the operational one permits a more refined account of important aspects of reduction operators, such as the representation of search strategies and their validity. Note that we may regard the operational semantics as an inferential semantics of reductive logic in the sense of Brandom (2000).

Essentially, a reduction operator is modelled by a partial function $\rho : \mathit{GOALS} \to F(\mathit{GOALS})$ in which $\mathit{GOALS}$ is the set of assertions over which we do the reductive reasoning, and $F(\mathit{GOALS})$ denotes collections of such assertions (e.g., finite sets or lists). Relative to this understanding, we can express validity relative to a logic in two different ways.

First, a collection of reduction operators is valid (with respect to a logic) if co-recursively reducing a goal eventually produces an empty list just in case the goal is valid in the logic of interest. While intuitive and useful, this does not improve on the extant semantics of reduction by Pym and Ritter (2004); indeed, it is perhaps less informative as, unlike the earlier work, it does not explain in the case of failed searches what extension of the logic is required to render them valid. It also does not quite answer the question: we desire an account of validity that expresses the correctness of the reduction operators themselves (as opposed to their constructions).

Second, a given reduction operator is valid if there corresponds to it a pre-approved process such that whenever the premisses are achieved, the conclusion is also achieved. The notion of achievement here is flexible, enabling many diverse situations to be encapsulated. A process corresponds to an accepted forwards inference. This version of validity is essentially Milner's theory of tactical proof (Milner 1984). Thus, we regard tactical proof as 'proof-theoretic semantics' (Schroeder-Heister 2018) for reductive logic, and this explains the effectiveness of the framework for proof-assistants.

As we have remarked in Sect. 1, this paper should be seen as a companion to Gheorghiu and Pym (2023a). Whereas in Gheorghiu and Pym (2023a) proof-theoretic semantics is used to provide a semantics for tactical proof, this paper provides a general foundation for reductive reasoning in terms of proof-theoretic semantics, establishes direct connections with foundational abstract work in the semantics of computation, and obtains tactical proof as a significant instance.

The scope of this work is the semantic foundations of reduction operators. It has included the semantic foundations of the things constructed by reduction operators. Future work includes giving the semantic foundations for the method by which those constructions (i.e., reductions) are built using reduction operators. This involves, among other things, expressing control régimes, determining the strategy used when exploring the space of reductions, and expressing how one may leverage information about explored portions of the space of reductions to inform future choices. Bundy (1998) has introduced the notion of a proof plan as a meta-theoretic tool to represent and reason about the pattern of proof-search and the structure of proofs. Future work also includes developing a semantic account of proof plans as an extension of this paper.

Acknowledgements. We are grateful to Simon Docherty, Tao Gu, and Eike Ritter for discussions of various aspects of this work.

Funding. This work has been partially supported by the UK EPSRC grants EP/S013008/1 and EP/R006865/1 and by the EU MOSAIC MCSA-RISE project.

Data availability. There is no data associated with this article.

Conflict of interest. The authors have no conflict of interest to declare that are relevant to the content of this article.

Open Access. This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. To view a copy of this licence, visit creativecommons.org/licenses/by/4.0/.