On Conditional Axioms and Associated Inference Rules

Abstract

In the present paper, we address the following general question in the framework of classical first-order logic. Assume that a certain mathematical principle can be formalized in a first-order language by a set E of conditional formulas of the form $\alpha \left(v\right)\to \beta \left(v\right)$. Given a base theory T, we can use the set of conditional formulas E to extend the base theory in two natural ways. Either we add to T each formula in E as a new axiom (thus obtaining a theory denoted by $T+E$) or we extend T by using the formulas in E as instances of an inference rule (thus obtaining a theory denoted by $T+E\text{–}\mathrm{Rule}$). The theory $T+E$ will be stronger than $T+E\text{–}\mathrm{Rule}$, but how much stronger can $T+E$ be? More specifically, is $T+E$ conservative over $T+E\text{–}\mathrm{Rule}$ for theorems of some fixed syntactical complexity $\mathsf{\Gamma }$? Under very general assumptions on the set of conditional formulas E, we obtain two main conservation results in this regard. Firstly, if the formulas in E have low syntactical complexity with respect to some prescribed class of formulas $\mathsf{\Pi }$ and in the applications of $E\text{–}\mathrm{Rule}$ side formulas from the class $\mathsf{\Pi }$ and can be eliminated (in a certain precise sense), then $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+E\text{–}\mathrm{Rule}$. Secondly, if, in addition, E is a finite set with m conditional sentences, then nested applications of $E\text{–}\mathrm{Rule}$ of a depth at most of m suffice to obtain $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ conservativity. These conservation results between axioms and inference rules extend well-known conservation theorems for fragments of first-order arithmetics to a general, purely logical framework.

1. Introduction

In the field of logic, encompassing both mathematical and computational aspects, the question of whether to prioritize axioms or rules greatly influences the study of various problems. This dilemma affects areas like logic programming design, different axiomatizations in arithmetics, and automated reasoning, among others.

Designing rules that enhance demonstration by substituting axioms is a viable approach to addressing provability in a theory (e.g., see [1]), provided that the impact of such substitution on the theorems of the latter is analyzed. For example, it is essential to manage induction in equational reasoning [2] or noetherian induction by rewriting [3], among others. Specific representation formalisms, such as geometric logic, can also benefit from the introduction of rules to simplify the axiom set [4,5].

In some applied fields, rule-based reasoning plays a pivotal role in various realms of mathematical or computational logic, the Semantic Web, and expert systems, among others, where rules provide a flexible and potent framework for representing and applying knowledge in a computer system.

Studying the (proof–theoretic) strength of a deductive system when we replace axioms for rules is not only interesting theoretically but also useful for tasks like designing and implementing computational proof systems.

This paper presents some theoretical tools and results that can be useful in enhancing our understanding of the (proof–theoretic) strength of systems representing knowledge by means of conditional axioms or, instead, by means of rules.

1.1. From Conditional Axioms to Rules

In this work, we address the following general question. Assume that a certain mathematical principle can be formalized in a first-order language by a set E of conditional formulas of the form $\alpha \left(v\right)\to \beta \left(v\right)$ (for instance, an induction principle). Then, given a first-order theory T expressing some basic properties of the functions and relations involved, T can be extended by adding the (universal closures of the) formulas in E as new axioms. In this way, we obtain a new theory that we denote by $T+E$. However, it is also possible (and in some cases perhaps more convenient, see some examples below) to extend T by using the involved principle to produce a new inference rule. This can be carried out, for example, by considering for each $\alpha \left(v\right)\to \beta \left(v\right)$ in E an instance

$$\frac{\forall v\alpha \left(v\right)}{\forall v\beta \left(v\right)}$$

of a new inference rule denoted by $E\text{–}\mathrm{Rule}$. Let $T+E\text{–}\mathrm{Rule}$ be the closure of T under first-order logic and applications of this new rule. This approach can also be seen as a weaker version of the typical conversion process from a Hilbert-style axiomatic system to a (Gentzen) sequent system. After leaving out the external quantifiers, the conversion primarily involves identifying a sound decomposition for each axiom to generate the rules.

In general, $T+E$ will be a proper extension of $T+E\text{–}\mathrm{Rule}$, but how much stronger than $T+E\text{–}\mathrm{Rule}$ can $T+E$ be? What is the exact relationship between both theories? And, are there other natural rules associated with a set E of conditional axioms that provide interesting information about $T+E$?

Before delving into the answers to these questions, let us present the scenario from which we extract both motivation and methods to deal with the previous problems: the study of conservation results between formal arithmetic theories. By a conservation result between two theories $T_1$ and $T_2$, we mean a proposition stating that for some class of sentences $\mathsf{\Gamma }$ and every sentence $\theta \in \mathsf{\Gamma }$, if $T_1$ proves $\theta$, then so does $T_2$ (and in such a case, we say that $T_1$ is $\mathsf{\Gamma }$-conservative over $T_2$).

Classical axiom schemes axiomatizing Peano arithmetics (say, ${\mathsf{\Sigma }}_n$–induction, ${\mathsf{\Sigma }}_n$–collection, and uniform ${\mathsf{\Sigma }}_n$–reflection, $n\ge 1$) share basic axiomatization and conservativity properties. It is a well-known fact that it is possible to develop a uniform treatment of conservation results for these schemes and, as a matter of fact, several (mainly proof–theoretic) methods providing uniform derivations of the basic conservation results are known. These methods include Herbrand Analysis as developed by W. Sieg in [6,7], S. Buss’ witnessing method both in Peano arithmetic and in bounded arithmetic (see [8,9]), the model–theoretic approach to Herbrand Analysis developed by J. Avigad in [10], and several approaches based on applications of cut elimination, see for instance Parsons’ [11], or more recently, the approach followed by L. Beklemishev in [12,13] (also closely related to Sieg’s method).

However, the basic ideas of these methods are, to a great extent, independent of any specific arithmetic notion and, therefore, could be developed for arbitrary (countable) first-order languages and theories. In order to explore this intuition, we can isolate the main characteristics of these arithmetical contexts.

Most axiom schemes that are considered in first-order arithmetic produce (when restricted to some class of formulas) sets of conditional axioms; that is, formulas of the form

$$\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right),$$

where $\overrightarrow{v}$ denotes a sequence $v_1,\cdots ,v_n$ of possible free variables. A classical example from formal arithmetics is the ${\mathsf{\Sigma }}_1$–induction scheme, $I{\mathsf{\Sigma }}_1$, given by the formulas

$$\phi (0,\overrightarrow{v})\wedge \forall x(\phi (x,\overrightarrow{v})\to \phi (x+1,\overrightarrow{v}))\to \forall x\phi (x,\overrightarrow{v})$$

where $\phi (x,\overrightarrow{v})$ varies within the class of formulas ${\mathsf{\Sigma }}_1$ in the arithmetic hierarchy. We can also introduce an inference rule, $E\text{–}\mathrm{Rule}$, associated with E in a natural way. Namely, E–Rule denotes the inference rule whose instances are

$$\frac{\forall \overrightarrow{v}\alpha \left(\overrightarrow{v}\right)}{\forall \overrightarrow{v}\beta \left(\overrightarrow{v}\right)}$$

for each $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$. The rule corresponding to the previous ${\mathsf{\Sigma }}_1$–induction scheme is denoted by ${\mathsf{\Sigma }}_1\text{–}\mathrm{IR}$ and consists of instances of the form

$$\frac{\forall \overrightarrow{v}(\phi (0,\overrightarrow{v})\wedge \forall x(\phi (x,\overrightarrow{v})\to \phi (x+1,\overrightarrow{v})))}{\forall \overrightarrow{v}\forall x\phi (x,\overrightarrow{v})}$$

where $\phi (x,\overrightarrow{v})\in {\mathsf{\Sigma }}_1$.

Then, given a base theory T, we are interested in conservation properties of the extensions of T, $T+E$, and $T+E\text{–}\mathrm{Rule}$ (the closure of T under first-order logic and applications of $E\text{–}\mathrm{Rule}$.) The analysis of these conservation properties typically proceeds from some level of syntactical complexity (represented for some class of formulas $\mathsf{\Pi }$) and (for some class of formulas $\mathsf{\Gamma }$ containing $\mathsf{\Pi }$) studies of $\mathsf{\Gamma }$–conservation results between the theories associated with E over the base theory T.

It is a classical theorem in the proof theory of first-order arithmetics (proved by Parsons [11]) that (over a base theory, $T_0$, axiomatized by some elementary arithmetic facts) the scheme $I{\mathsf{\Sigma }}_1$ is ${\mathsf{\Pi }}_2$-conservative over $T_0+{\mathsf{\Sigma }}_1\text{–}\mathrm{IR}$. More precisely, $T_0+I{\mathsf{\Sigma }}_1$ is a ${\mathsf{\Pi }}_2$-conservative extension of $T_0+{\mathsf{\Sigma }}_1\text{–}\mathrm{IR}$. In this work, we isolate conditions under which a similar result to Parsons’ theorem can be derived for a given set of conditional axioms E. We show that if the formulas in the set of conditional axioms E have a suitable syntactical complexity, then the conservation properties of the theories associated with E can be derived from simple conditions on the $E\text{–}\mathrm{Rule}$. In order to derive these general counterparts of Parson’s theorem, the following auxiliary notions are introduced.

If, for each $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$, the formulas $\alpha \left(\overrightarrow{v}\right)$ and $\beta \left(\overrightarrow{v}\right)$ have a low syntactical complexity with respect to the basic level $\mathsf{\Pi }$ (see Definition 6), then we say that E is a set of normal conditional axioms with respect to $\mathsf{\Pi }$. Let us denote by $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ the set of universal closures of boolean combinations of formulas in $\mathsf{\Pi }$. Then, the set of $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ consequences of $T+E$ can be described using an auxiliary inference rule $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$, with instances

$$\frac{\forall \overrightarrow{v}\forall \overrightarrow{z}(\theta (\overrightarrow{v},\overrightarrow{z})\to \alpha \left(\overrightarrow{v}\right))}{\forall \overrightarrow{v}\forall \overrightarrow{z}(\theta (\overrightarrow{v},\overrightarrow{z})\to \beta \left(\overrightarrow{v}\right))}$$

where $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$ and $\theta (\overrightarrow{v},\overrightarrow{z})$ is a conjunction of formulas that belong to $\mathsf{\Pi }$ or are negations of some formulas in $\mathsf{\Pi }$. Using a model–theoretic argument (based upon simple properties of a general notion of an existentially closed model, following ideas developed by Avigad in [10]) we prove that for every theory T (axiomatized by formulas with restricted syntactical complexity, see Corollary 1),

• For every set of normal conditional axioms with respect to $\mathsf{\Pi }$ and E, $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ (the closure of T under first-order logic and applications of $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$).

Let us remark here that the auxiliary $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is a natural device in the proof–theoretic approach to conservation results for arithmetical theories via cut elimination. As a matter of fact, the rule $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ was considered by J. C. Shepherdson in his analysis of open induction (see lemma 2.3 in [14]). A very similar rule was also used for ${\mathsf{\Sigma }}_n$ induction by Parsons (see section §3 in [11]) and more recently by Beklemishev in his work on ${\mathsf{\Sigma }}_n$–collection (see [12]) and ${\mathsf{\Delta }}_{n+1}$–induction (see [13]). Our proof of Corollary 1 (as a consequence of Proposition 2) provides a model–theoretic interpretation of these proof–theoretic arguments.

Corollary 1 suggests the following notion (see Definition 7): we say that E is weakly Π-reducible modulo T if $T^{\prime }+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ and $T^{\prime }+E\text{–}\mathrm{Rule}$ are equivalent for every theory $T^{\prime }$ extending T. Putting it all together, we can state a version of Parson’s theorem in a more general context where the axiomatization of T has again a restricted syntactical complexity (see Theorem 1 for this and other related conservation results):

• Let E be a set of normal conditional axioms with respect to $\mathsf{\Pi }$. If E is weakly $\mathsf{\Pi }$-reducible modulo T, then $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+E\text{–}\mathrm{Rule}$.

This result, and more generally Theorem 1, can be considered as a reformulation of some aspects of Kaye’s model–theoretic work in [15] where, using Henkin constructions, Kaye derived conservation results in the spirit of Theorem 1. As pointed out in the survey paper [16], a uniform model–theoretic treatment of conservation results between several induction schemes and their parameter-free versions can be obtained using these ideas. The model–theoretic core of this uniform approach was developed in a general setting in [17]. The main conceptual difference between Kaye’s approach and our exposition in this paper is, on top of the use of existentially closed models, the emphasis on the role played by inference rules in these results that, we think, allows for a more systematic presentation.

In a similar vein, in Section 5, we reinterpret, using the notion of a set of normal conditional sentences, a conservation result obtained by Kaye (see Theorem 1.4 in [17]). Namely, we show that (see Theorem 3), given a theory T and a finite set E of normal conditional sentences with respect to $\mathsf{\Pi }$, then

• If a $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ sentence $\theta$ can be derived from T together with m sentences in E, then $\theta$ can be also derived from $T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ using nested applications of $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ with a depth of at most m.

For the reader’s convenience,

Table 1. Theories to be considered in this paper.

Extension	T Augmented with/Closed Under
$T+E$	$\forall \overrightarrow{v}(\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right))$, with $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$
$T+UE$	$\forall \overrightarrow{v}\alpha \left(\overrightarrow{v}\right)\to \forall \overrightarrow{v}\beta \left(\overrightarrow{v}\right)$, with $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$
$T+E\text{–}\mathrm{Rule}$	${\displaystyle \frac{\forall \overrightarrow{v}\alpha \left(\overrightarrow{v}\right)}{\forall \overrightarrow{v}\beta \left(\overrightarrow{v}\right)}}$, with $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$
$T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$	${\displaystyle \frac{\forall \overrightarrow{v}\forall \overrightarrow{z}(\theta (\overrightarrow{v},\overrightarrow{z})\to \alpha \left(\overrightarrow{v}\right))}{\forall \overrightarrow{v}\forall \overrightarrow{z}(\theta (\overrightarrow{v},\overrightarrow{z})\to \beta \left(\overrightarrow{v}\right))}}$, with $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$ and $\theta \in {(\mathsf{\Pi }\cup \neg \mathsf{\Pi })}^{\wedge }$
$T+E_{\forall }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$	${\displaystyle \frac{\theta \to \alpha }{\theta \to \beta }}$, with $\alpha \to \beta \in E$ and $\theta \in \exists \mathcal{B}\left(\mathsf{\Pi }\right)$
$T+E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$	${\displaystyle \frac{\theta \to \alpha }{\theta \to \beta }}$, with $\alpha \to \beta \in E$ and $\theta \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$
${[T,R]}_m$	Nested applications of the corresponding rule R with a depth of at most m

where m is a natural number and $\theta \in {(\mathsf{\Pi }\cup \neg \mathsf{\Pi })}^{\wedge }$ expresses the fact that $\theta (\overrightarrow{v},\overrightarrow{z})$ is a finite conjunction of formulas, each of which is in $\mathsf{\Pi }$ or its negation is in $\mathsf{\Pi }$.

summarizes the axiomatizations of the theories we will work with in this paper. Given a first-order language L, let E denote a set of conditional axioms of the form $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)$ and let $\mathsf{\Pi }$ denote a basic fragment of L (as defined in Definition 3). The first two theories are given by a base theory T together with a set of axioms. The remaining theories are constructed using (Hilbert-style) inference rules and thus are defined by the closure of the base theory T under applications of the corresponding rule.

Table 2. Conservation results demonstrated in this paper.

Subtheory	Conservation	Conditions on E	Reference
$T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$	$\forall \mathcal{B}\left(\mathsf{\Pi }\right)$	$\alpha \left(\overrightarrow{v}\right)\in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$, $\beta \left(\overrightarrow{v}\right)\in \forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$	Corollary 1
$T+E\text{–}\mathrm{Rule}$	$\forall \mathcal{B}\left(\mathsf{\Pi }\right)$	$\alpha \left(\overrightarrow{v}\right)\in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$, $\beta \left(\overrightarrow{v}\right)\in \forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, E is weakly $\mathsf{\Pi }$-reducible	Theorem 1
$T+UE$	$\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$	$\alpha \left(\overrightarrow{v}\right)\in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$, $\beta \left(\overrightarrow{v}\right)\in \forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, E is weakly $\mathsf{\Pi }$-reducible	Theorem 1
$T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$	$\forall \mathcal{B}\left(\mathsf{\Pi }\right)$	$\alpha \in \mathcal{B}(\forall \mathcal{B}(\mathsf{\Pi }\left)\right)$, $\alpha \to \beta$ sentences	Lemma 5
${[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m$	$\forall \mathcal{B}\left(\mathsf{\Pi }\right)$	$\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)\cup \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, E consists of m sentences	Theorem 3
${[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m$	$\exists \mathcal{B}\left(\mathsf{\Pi }\right)$	$\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)\cup \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, E consists of m sentences	Theorem 3
${[T,E\text{–}\mathrm{Rule}]}_m$	$\forall \mathcal{B}\left(\mathsf{\Pi }\right)$	$\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)\cup \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, E consists of m sentences, E is $\mathsf{\Pi }$-reducible	Corollary 2

where E is said to be weakly $\mathsf{\Pi }$-reducible (modulo T) if $S+E\text{–}\mathrm{Rule}\equiv S+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ for each theory S extending T, and E is said to be $\mathsf{\Pi }$-reducible (modulo T) if ${[S,E\text{–}\mathrm{Rule}]}_1\equiv {[S,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_1$ for each theory S extending T.

summarizes the main conservation results obtained in this paper. For a given base theory T, the theory $T+E$ is conservative over each of the following subtheories (it is important to note that, for the first three conservation results, we also require the base theory T to be $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable, whereas the remaining four hold for base theories T of arbitrary syntactical complexity).

1.2. Aim and Structure of the Paper

In this paper, we prove some conservation results between, on the one hand, an arbitrary theory axiomatized (over a basic theory T) by a set of conditional axioms E and, on the other hand, theories axiomatized (again over T) by (nested) applications of the rules $E\text{–}\mathrm{Rule}$ and $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$. Although the results included here are not essentially new and the corresponding arithmetical versions are well-known, we think that the model–theoretic approach that we develop in their proofs is rather simple and clear. This simplicity aids in making the whole presentation of these kinds of results in a general context very easy to follow. In a fundamental sense, this paper revisits a substantial part of the work of Kaye in [16,17] through the light of the methods introduced more recently by Avigad in [10]. It also reformulates Kaye’s results in terms of natural inference rules, as can be found in more standard proof–theoretic works [12,18]. We hope this reformulation, together with the model–theoretic approach we adopt here, can contribute to making the logical content of these results more accessible to a wider audience, including researchers working on topics with no direct connection with formal arithmetics.

The structure of this paper is as follows. The next section, Section 2, specifies the basic notions and notation used in the paper. In Section 3, we present the basic model–theoretic device used throughout the paper to derive conservation results. Here, a generalization of the notion of an existentially closed model plays a central role. The notion of a normal conditional axiom is introduced in Section 4, where some conservation results between the theory axiomatized by conditional axioms and the one obtained by considering the associated rules are established. The specific case of a finite set of conditional sentences is analyzed in Section 5. This paper concludes with some considerations about the results obtained and possible lines of future research.

2. Inference Rules and Conditional Axioms

We always work in classical first-order logic with equality. Let us fix a countable first-order language L. A formula is a literal of L if it is atomic or negated atomic.

As usual, a theory T is a set of sentences of L closed under logical consequence (that is, for each formula $\phi$, if $T\vDash \phi$, then $\phi \in T$). An axiomatization of T is a set of formulas $\mathsf{\Gamma }$ such that $T=\{\phi :\mathsf{\Gamma }\vDash \phi \}$.

Through this paper, we shall deal with different sets of formulas built up from a basic distinguished set using several syntactical operations. So, we shall begin by defining these operations. Given a set of formulas $\mathsf{\Gamma }$, the following notation will be used:

• $\neg \mathsf{\Gamma }$ is the set of formulas $\{\neg \phi \left(\overrightarrow{x}\right):\phi \left(\overrightarrow{x}\right)\in \mathsf{\Gamma }\}$.
• $\exists \mathsf{\Gamma }$ is the set $\{\exists \overrightarrow{x}\phi \left(\overrightarrow{x}\right):\phi \left(\overrightarrow{x}\right)\in \mathsf{\Gamma }\}$ (the sets $\forall \mathsf{\Gamma }$, $\exists \forall \mathsf{\Gamma }$, $\forall \exists \mathsf{\Gamma }$,…are defined accordingly using the appropriate blocks of initial quantifiers).
• ${\mathsf{\Gamma }}^{\wedge }$ (resp. ${\mathsf{\Gamma }}^{\vee }$) is the set of all finite conjunctions (resp. disjunctions) of formulas of $\mathsf{\Gamma }$. ${\mathsf{\Gamma }}^{+}$ is the closure of $\mathsf{\Gamma }$ under disjunctions and conjunctions.
• $\mathcal{B}\left(\mathsf{\Gamma }\right)$ denotes the set of boolean combinations of formulas in $\mathsf{\Gamma }$.

As usual, a tuple of elements (or variables) $a_1,\cdots ,a_n$ is abbreviated by $\overrightarrow{a}$, and we write $\phi \left(\overrightarrow{x}\right)$ to indicate that the free variables of $\phi$ are among the tuple $\overrightarrow{x}$.

For a given base theory T, extensions of T can typically be axiomatized in two ways: (1) by adding a new set of sentences E to T and closing under logical consequence, or (2) by closing T under (first-order logic and) applications of some new inference rules. In this paper, we shall explore the relationship between both extensions.

Firstly, we recall some basic notions and terminology on inference rules introduced by Beklemishev in [18]. By an inference rule, we mean a set of instances, that is, expressions of the form

$$\frac{{\phi }_1,\cdots ,{\phi }_n}{\psi }$$

where ${\phi }_1,\cdots ,{\phi }_n,\psi$ are formulas. If R is an inference rule, then $[T,R]$ denotes the closure of T under first-order logic and unnested applications of R (that is, a proof in $[T,R]$ may contain several applications of R but they are not to occur on the same branch within the proof). By recursion on $k\in \omega$, we define ${[T,R]}_0=T$ and ${[T,R]}_{k+1}=[{[T,R]}_k,R]$. The closure of T under first-order logic and applications of R is $T+R={\bigcup }_{k\in \omega }{[T,R]}_k$.

Definition 1.

Let $R_1$ and $R_2$ be rules and let U be a theory.

1. 

The rule $R_1$ is derivable from $R_2$ modulo U if for every extension T of U, $T+R_2$ extends $T+R_1$.

2. 

The rules $R_1$ and $R_2$ are equivalent modulo U if for every extension T of U, $T+R_1\equiv T+R_2$ (that is, they are equivalent theories).

3. 

The rule $R_1$ is reducible to $R_2$ modulo U if for every extension T of U, $[T,R_2]$ extends $[T,R_1]$.

4. 

$R_1$ and $R_2$ are congruent modulo U if for every extension T of U, $[T,R_1]\equiv [T,R_2]$.

Many significant mathematical and combinatorial principles are expressed in the form of implications, where the satisfaction of a certain condition A entails the presence of another condition B. The formal representation of these principles corresponds to formulas whose outermost connective is the logical implication symbol →. This motivates the following definition.

Definition 2.

We say that a set E of L-formulas is a set of conditional axioms if every element of E is a formula of the form $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)$ (recall that for a formula φ, we write $\phi \left(\overrightarrow{v}\right)$ to mean that the free variables of φ are among the variables $\overrightarrow{v}$).

Let T be an L-theory and let E be a set of conditional axioms. Then, by definition, $T+E$ is the theory axiomatized by T plus the universal closure of every formula in E, i.e., the theory given by T plus

$$\forall \overrightarrow{v}(\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)),$$

for each $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$.

A natural inference rule, $E\text{–}\mathrm{Rule}$, can be associated with E by considering the instances

$$\frac{\forall \overrightarrow{v}\alpha \left(\overrightarrow{v}\right)}{\forall \overrightarrow{v}\beta \left(\overrightarrow{v}\right)}$$

for each $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$.

In this paper, we explore the relationship between the theories $T+E$, $T+E\text{–}\mathrm{Rule}$, and ${[T,E\text{–}\mathrm{Rule}]}_k$$(k\ge 1)$ for a given set of conditional axioms.

In order to be able to determine more precisely the relative proof–theoretic strength of these theories, we shall fix some level of syntactical complexity for the formulas considered. This will be performed through the notion of a basic fragment of a first-order language:

Definition 3.

A set of formulas of L, Π, is a basic fragment of L if Π satisfies the following conditions:

1. 

Every atomic formula of L belongs to Π.

2. 

If $\phi \in \mathsf{\Pi }$ and θ is a subformula of φ, then $\theta \in \mathsf{\Pi }$.

3. 

If $\phi (x,v_1,\cdots ,v_n)\in \mathsf{\Pi }$ and t is a term of L, then $\phi (t,v_1,\cdots ,v_n)\in \mathsf{\Pi }$.

In short, a basic fragment is a set of formulas that includes all atomic formulas and is closed under subformulas and term substitution.

Let us enumerate a few natural examples of basic fragments.

• The sets ${\forall }_n$ and ${\exists }_n$ of formulas of L (where ${\forall }_0={\exists }_0$ denotes the class of open formulas of L and for each $n\ge 0$, ${\exists }_{n+1}=\exists {\forall }_n$ and ${\forall }_{n+1}=\forall {\exists }_n$).
• The set of all literals of L (a formula is a literal if it is atomic or negated atomic).
• The set comprising all clauses (i.e., disjunctions of literals) of L.
• In the context of arithmetic languages, other examples are the classes in the arithmetical hierarchy ${\mathsf{\Pi }}_n$ and ${\mathsf{\Sigma }}_n$, $n\ge 0$, (see [19] or [20]); the sets $U_n$ and $E_n$, $n\ge 0$, in the ${\mathsf{\Delta }}_0$ hierarchy of bounded formulas (see [21]); and the sets ${\widehat{\mathsf{\Pi }}}_n^b$ and ${\widehat{\mathsf{\Sigma }}}_n^b$, $n\ge 0$, of strictly bounded formulas considered in bounded arithmetic (see [20]).

Given a basic fragment $\mathsf{\Pi }$, we associate E with a new set of conditional axioms denoted by $E^{\mathsf{\Pi }}$ and given by the set of all formulas

$$({\theta }_1(\overrightarrow{v},\overrightarrow{z})\wedge \cdots \wedge {\theta }_k(\overrightarrow{v},\overrightarrow{z})\to \alpha \left(\overrightarrow{v}\right))\to ({\theta }_1(\overrightarrow{v},\overrightarrow{z})\wedge \cdots \wedge {\theta }_k(\overrightarrow{v},\overrightarrow{z})\to \beta \left(\overrightarrow{v}\right))$$

where $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$, and for each $j=1,\cdots ,k$, ${\theta }_j(\overrightarrow{v},\overrightarrow{z})\in \mathsf{\Pi }\cup \neg \mathsf{\Pi }$. We will also consider its associated inference rule, $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$, given by the set of instances

$$\frac{\forall \overrightarrow{v}\forall \overrightarrow{z}({\theta }_1(\overrightarrow{v},\overrightarrow{z})\wedge \cdots \wedge {\theta }_k(\overrightarrow{v},\overrightarrow{z})\to \alpha \left(\overrightarrow{v}\right))}{\forall \overrightarrow{v}\forall \overrightarrow{z}({\theta }_1(\overrightarrow{v},\overrightarrow{z})\wedge \cdots \wedge {\theta }_k(\overrightarrow{v},\overrightarrow{z})\to \beta \left(\overrightarrow{v}\right))}$$

where $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$ and for each $j=1,\cdots ,k$, ${\theta }_j(\overrightarrow{v},\overrightarrow{z})\in \mathsf{\Pi }\cup \neg \mathsf{\Pi }$.

Let us observe that $T+E$ is equivalent to $T+E^{\mathsf{\Pi }}$ (both are different axiomatizations of the same theory) but, in general, the theories $[T,E\text{–}\mathrm{Rule}]$ and $[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]$ are not equivalent. Indeed, $[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]$ always extends $[T,E\text{–}\mathrm{Rule}]$ (to simulate an application of $E\text{–}\mathrm{Rule}$, one applies the corresponding instance of $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ with $\theta \left(z_1\right)\equiv (z_1=z_1)$, which belongs to $\mathsf{\Pi }$ for any basic fragment). However, in general, $[T,E\text{–}\mathrm{Rule}]$ may not necessarily be an extension of $[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]$.

3. A Model–Theoretic Standpoint

In this section, we introduce the machinery that we will use to derive our conservation results between theories $T+E$ and $T+E\text{–}\mathrm{Rule}$, where E is a set of conditional axioms.

The methods we use in this paper are model–theoretic in nature and essentially follow the methodology introduced by Avigad in [10] who, in turn, mentions that in the context of bounded arithmetic, this methodology has been used in Zambella [22], where it is attributed to unpublished work by Albert Visser.

Central to our approach is the notion of an $\exists \mathsf{\Pi }$-closed model of a theory T, where $\mathsf{\Pi }$ is a fixed but arbitrary basic fragment. This notion is a natural generalization of the well-known concept of an existentially closed model and extends the concept of a Herbrand-saturated model introduced in [10].

All the languages and models considered through this paper are countable. Given two L structures $\mathfrak{A}$ and $\mathfrak{B}$ and a set of formulas $\mathsf{\Phi }$, we shall write $\mathfrak{A}{\prec }_{\mathsf{\Phi }}\mathfrak{B}$ to express that $\mathfrak{B}$ is a $\mathsf{\Phi }$-elementary extension of $\mathfrak{A}$; that is, $\mathfrak{A}$ is a substructure of $\mathfrak{B}$, and for each $\theta (u_1,\cdots ,u_n)\in \mathsf{\Phi }$ and each $a_1,\cdots ,a_n\in \mathfrak{A}$, we have

$$\mathfrak{A}\vDash \theta \left(\overrightarrow{a}\right)⟺\mathfrak{B}\vDash \theta \left(\overrightarrow{a}\right).$$

Definition 4.

Given a basic fragment Π of a first-order language L and an L structure $\mathfrak{A}$, the Π-diagram of $\mathfrak{A}$ is the set of sentences of the language $L\cup \{a:a\in \mathfrak{A}\}$ given by

$$D_{\mathsf{\Pi }}\left(\mathfrak{A}\right)=\{\phi \left(\overrightarrow{a}\right):\mathfrak{A}\vDash \phi \left(\overrightarrow{a}\right)and\phi \left(\overrightarrow{x}\right)\in \mathsf{\Pi }\cup \neg \mathsf{\Pi }\}$$

Remark 1.

Let Π be a basic fragment of a language L and let $\mathfrak{A}$ be an L structure.

1. 

If $\mathfrak{B}$ is an L structure and $\mathfrak{A}$ is a substructure of $\mathfrak{B}$, then

$$\mathfrak{B}\vDash D_{\mathsf{\Pi }}\left(\mathfrak{A}\right)⟺\mathfrak{A}{\prec }_{\mathsf{\Pi }}\mathfrak{B}.$$

2. 

For every L-theory T, the following conditions are equivalent:

(a) 

$T+D_{\mathsf{\Pi }}\left(\mathfrak{A}\right)$ is consistent.

(b) 

There exists $\mathfrak{B}\vDash T$ such that $\mathfrak{A}{\prec }_{\mathsf{\Pi }}\mathfrak{B}$.

Remark 2.

Let us observe that, for every two L structures $\mathfrak{A}$ and $\mathfrak{B}$, we have

$$\mathfrak{A}{\prec }_{\mathsf{\Pi }}\mathfrak{B}⟺\mathfrak{A}{\prec }_{\mathcal{B}\left(\mathsf{\Pi }\right)}\mathfrak{B}.$$

The next definition introduces a straightforward generalization of the notion of an existentially closed model.

Definition 5.

Let $\mathfrak{A}$ be an L structure. We say that $\mathfrak{A}$ is an $\exists \mathsf{\Pi }$-closed model of T if $\mathfrak{A}\vDash T$, and for each $\mathfrak{B}\vDash T$, $\mathfrak{A}{\prec }_{\mathsf{\Pi }}\mathfrak{B}$ implies $\mathfrak{A}{\prec }_{\exists \mathsf{\Pi }}\mathfrak{B}.$

Observe that taking $\mathsf{\Pi }={\forall }_0$, we obtain the classical notion of an existentially closed model from Model Theory; taking $\mathsf{\Pi }={\forall }_1$, we obtain the notion of a Herbrand-saturated model from [10]; taking $\mathsf{\Pi }={\mathsf{\Delta }}_0$, we obtain the notion of a 1-closed model from [23]; and taking $\mathsf{\Pi }={\widehat{\mathsf{\Pi }}}_i^b$, we obtain the notion of an $\exists {\widehat{\mathsf{\Pi }}}_i^b$-closed model from [24].

The usual chain argument for constructing existentially closed models provides us with an existence lemma. The proof of Lemma 1 is rather standard but we include a sketch so that the reader can check where the properties defining the notion of a basic fragment $\mathsf{\Pi }$ are needed.

Lemma 1.

Let T be a $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable consistent theory. Then, for each $\mathfrak{A}\vDash T$, there exists an $\exists \mathsf{\Pi }$-closed model of T, $\mathfrak{B}$, such that $\mathfrak{A}{\prec }_{\mathsf{\Pi }}\mathfrak{B}$.

Proof. 

Let $\mathfrak{A}$ be a model of T. In the first step, we will construct a model of T, ${\mathfrak{A}}^1$, satisfying $\mathfrak{A}{\prec }_{\mathsf{\Pi }}{\mathfrak{A}}^1$, and for each $\mathfrak{C}\vDash T$ with ${\mathfrak{A}}^1{\prec }_{\mathsf{\Pi }}\mathfrak{C}$ and for all $\phi (x_1,\cdots ,x_n,\overrightarrow{y})\in \mathsf{\Pi }$ and $a_1,\cdots ,a_n\in \mathfrak{A}$,

$$\mathfrak{C}\vDash \exists \overrightarrow{y}\phi (a_1,\cdots ,a_n,\overrightarrow{y})\Rightarrow {\mathfrak{A}}^1\vDash \exists \overrightarrow{y}\phi (a_1,\cdots ,a_n,\overrightarrow{y}).$$

To this end, we will form a chain of models of T of power $\omega$,

$$\mathfrak{A}={\mathfrak{A}}_0^1{\prec }_{\mathsf{\Pi }}{\mathfrak{A}}_1^1{\prec }_{\mathsf{\Pi }}\cdots {\prec }_{\mathsf{\Pi }}{\mathfrak{A}}_i^1{\prec }_{\mathsf{\Pi }}\cdots ,$$

and take ${\mathfrak{A}}^1={\bigcup }_{i\in \omega }{\mathfrak{A}}_i^1$.

Let $\{{\theta }_i(a_1,\cdots ,a_{n_i},\overrightarrow{y}):i\in \omega \}$ be an enumeration of all formulas in $\mathsf{\Pi }$ with parameters $a_i$ from $\mathfrak{A}$.

• $i=0$: Put ${\mathfrak{A}}_0^1=\mathfrak{A}$.
• $i\to i+1$: If $T+D_{\mathsf{\Pi }}\left({\mathfrak{A}}_i^1\right)+\exists \overrightarrow{y}{\theta }_i(a_1,\cdots ,a_{n_i},\overrightarrow{y})$ is consistent, there exists $\mathfrak{D}\vDash T$ such that ${\mathfrak{A}}_i^1{\prec }_{\mathsf{\Pi }}\mathfrak{D}$ and $\mathfrak{D}\vDash \exists \overrightarrow{y}{\theta }_i(a_1,\cdots ,a_{n_i},\overrightarrow{y})$. Define ${\mathfrak{A}}_{i+1}^1$ to be $\mathfrak{D}$. If $T+D_{\mathsf{\Pi }}\left({\mathfrak{A}}_i^1\right)+\exists \overrightarrow{y}{\theta }_i(a_1,\cdots ,a_{n_i},\overrightarrow{y})$ is inconsistent, define ${\mathfrak{A}}_{i+1}^1$ to be ${\mathfrak{A}}_i^1$.

Let us check that ${\mathfrak{A}}^1={\bigcup }_{i\in \omega }{\mathfrak{A}}_i^1$ satisfies the required properties.

• $\mathfrak{A}{\prec }_{\mathsf{\Pi }}{\mathfrak{A}}^1$. As usual, by induction on the syntactical complexity of the formulas in $\mathsf{\Pi }$, it is easy to see that the union of the chain ${\mathfrak{A}}^1$ is a $\mathsf{\Pi }$-elementary extension of each model in the chain (here we use the assumption that a basic fragment $\mathsf{\Pi }$ is closed under subformulas and term substitution).
• ${\mathfrak{A}}^1\vDash T$. It follows from the fact that $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable theories are preserved under unions of $\mathsf{\Pi }$-elementary chains. In fact, let $\forall \overrightarrow{x}\exists \overrightarrow{y}\theta (\overrightarrow{x},\overrightarrow{y})$ be an axiom of T, where $\theta (\overrightarrow{x},\overrightarrow{y})\in \mathsf{\Pi }$, and consider $a_1,\cdots ,a_n\in {\mathfrak{A}}^1$. Pick $i_0\in \omega$ such that $a_1,\cdots ,a_n\in {\mathfrak{A}}_{i_0}^1$. Since ${\mathfrak{A}}_{i_0}^1$ is a model of T, there are $b_1,\cdots ,b_m\in {\mathfrak{A}}_{i_0}^1$ such that ${\mathfrak{A}}_{i_0}^1\vDash \theta (\overrightarrow{a},\overrightarrow{b})$. Since ${\mathfrak{A}}_{i_0}^1{\prec }_{\mathsf{\Pi }}{\mathfrak{A}}^1$ and $\theta (\overrightarrow{x},\overrightarrow{y})\in \mathcal{B}\left(\mathsf{\Pi }\right)$, ${\mathfrak{A}}^1\vDash \theta (\overrightarrow{a},\overrightarrow{b})$. Hence, ${\mathfrak{A}}^1\vDash \exists \overrightarrow{y}\theta (\overrightarrow{a},\overrightarrow{y})$, as required.
• Consider $\mathfrak{C}\vDash T$ with ${\mathfrak{A}}^1{\prec }_{\mathsf{\Pi }}\mathfrak{C}$, $\phi (x_1,\cdots ,x_n,\overrightarrow{y})\in \mathsf{\Pi }$ and $a_1,\cdots ,a_n\in \mathfrak{A}$ such that $\mathfrak{C}\vDash \exists \overrightarrow{y}\phi (a_1,\cdots ,a_n,\overrightarrow{y})$. Pick $j\in \omega$ such that $\phi (a_1,\cdots ,a_n,\overrightarrow{y})$ is ${\theta }_j(a_1,\cdots ,a_{n_j},\overrightarrow{y})$. Clearly, $T+D_{\mathsf{\Pi }}\left({\mathfrak{A}}_j^1\right)+\exists \overrightarrow{y}{\theta }_j(a_1,\cdots ,a_{n_j},\overrightarrow{y})$ is consistent and so ${\mathfrak{A}}_{j+1}^1\vDash \exists \overrightarrow{y}\phi (a_1,\cdots ,a_n,\overrightarrow{y})$ by construction. But then ${\mathfrak{A}}^1\vDash \exists \overrightarrow{y}\phi (a_1,\cdots ,a_n,\overrightarrow{y})$ since ${\mathfrak{A}}_{j+1}^1{\prec }_{\mathsf{\Pi }}{\mathfrak{A}}^1$.

Repeating the construction $\omega$ times, we obtain a chain of models of T:

$$\mathfrak{A}={\mathfrak{A}}^0{\prec }_{\mathsf{\Pi }}{\mathfrak{A}}^1{\prec }_{\mathsf{\Pi }}{\mathfrak{A}}^2{\prec }_{\mathsf{\Pi }}\cdots$$

such that any $\exists \mathsf{\Pi }$ sentence with constants from ${\mathfrak{A}}^i$ that holds in some extension of ${\mathfrak{A}}^{i+1}$, which is a model of T, holds in ${\mathfrak{A}}^{i+1}$ as well. Take $\mathfrak{B}={\bigcup }_{i\in \omega }{\mathfrak{A}}^i$. It is clear that $\mathfrak{A}{\prec }_{\mathsf{\Pi }}\mathfrak{B}$ and $\mathfrak{B}$ is an $\exists \mathsf{\Pi }$-closed model of T. □

Our basic device to prove the conservation results is the next lemma, which is a general version of Theorem 3.4 in [10].

Lemma 2.

Let T be a $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable theory and let $T^{\prime }$ be a theory such that every $\exists \mathsf{\Pi }$-closed model of T is a model of $T^{\prime }$. Then, $T^{\prime }$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over T.

Proof. 

Let $\phi \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ be a sentence such that $T^{\prime }⊢\phi$. We must show that $T⊢\phi$.

Suppose that $T⊬\phi$. Then, there exists $\mathfrak{A}\vDash T+\neg \phi$. Since $\neg \phi$ is an $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$ sentence, $T+\neg \phi$ is a $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatized, consistent theory and, by Lemma 1 and Remark 2, there exists an $\exists \mathsf{\Pi }$-closed model of T, $\mathfrak{B}$, such that $\mathfrak{A}{\prec }_{\mathcal{B}\left(\mathsf{\Pi }\right)}\mathfrak{B}$. Firstly, by the assumption on the theory $T^{\prime }$, $\mathfrak{B}$ is a model of $T^{\prime }$. Secondly, put $\neg \phi \equiv \exists \overrightarrow{y}{\phi }_0\left(\overrightarrow{y}\right)$, with ${\phi }_0\left(\overrightarrow{y}\right)\in \mathcal{B}\left(\mathsf{\Pi }\right)$, and pick $\overrightarrow{a}\in \mathfrak{A}$, satisfying that $\mathfrak{A}\vDash {\phi }_0\left(\overrightarrow{a}\right)$. Since $\mathfrak{A}{\prec }_{\mathcal{B}\left(\mathsf{\Pi }\right)}\mathfrak{B}$, $\mathfrak{B}\vDash {\phi }_0\left(\overrightarrow{a}\right)$, and so $\mathfrak{B}\vDash \exists \overrightarrow{y}{\phi }_0\left(\overrightarrow{y}\right)$. Then, $\mathfrak{B}\vDash T^{\prime }+\neg \phi$, a contradiction. □

In order to apply Lemma 2, we will need the following result that mirrors theorem 3.3 outlined in [10]. It establishes a connection between validity within an $\exists \mathsf{\Pi }$-closed model of T and the provability within the theory T itself.

Proposition 1.

Let $\mathfrak{A}$ be an $\exists \mathsf{\Pi }$-closed model of T and $\phi \left(\overrightarrow{x}\right)\in \exists \forall \neg \mathsf{\Pi }$, $\overrightarrow{a}\in \mathfrak{A}$ such that $\mathfrak{A}\vDash \phi \left(\overrightarrow{a}\right)$. Then, there exist $\overrightarrow{c}\in \mathfrak{A}$ and ${\theta }_1(\overrightarrow{x},\overrightarrow{z}),\cdots ,{\theta }_k(\overrightarrow{x},\overrightarrow{z})\in \mathsf{\Pi }\cup \neg \mathsf{\Pi }$ such that

$$\mathfrak{A}\vDash {\theta }_1(\overrightarrow{a},\overrightarrow{c})\wedge \cdots \wedge {\theta }_k(\overrightarrow{a},\overrightarrow{c})andT⊢{\theta }_1(\overrightarrow{x},\overrightarrow{z})\wedge \cdots \wedge {\theta }_k(\overrightarrow{x},\overrightarrow{z})\to \phi \left(\overrightarrow{x}\right).$$

Proof. 

Since $\mathfrak{A}\vDash \phi \left(\overrightarrow{a}\right)$ and $\phi \left(\overrightarrow{x}\right)\in \exists \forall \neg \mathsf{\Pi }$, there are ${\phi }_0(\overrightarrow{x},\overrightarrow{v})\in \forall \neg \mathsf{\Pi }$ and $\overrightarrow{d}\in \mathfrak{A}$ such that $\phi \left(\overrightarrow{x}\right)$ is $\exists \overrightarrow{v}{\phi }_0(\overrightarrow{x},\overrightarrow{v})$ and $\mathfrak{A}\vDash {\phi }_0(\overrightarrow{a},\overrightarrow{d})$. Since $\mathfrak{A}$ is $\exists \mathsf{\Pi }$-closed, $T+D_{\mathsf{\Pi }}\left(\mathfrak{A}\right)+\neg {\phi }_0(\overrightarrow{a},\overrightarrow{d})$ is inconsistent. Indeed, assume that $T+D_{\mathsf{\Pi }}\left(\mathfrak{A}\right)+\neg {\phi }_0(\overrightarrow{a},\overrightarrow{d})$ is consistent. By Remark 1, there exists $\mathfrak{B}\vDash T+\neg {\phi }_0(\overrightarrow{a},\overrightarrow{d})$ such that $\mathfrak{A}{\prec }_{\mathsf{\Pi }}\mathfrak{B}$. It follows from the fact that $\mathfrak{A}$ is an $\exists \mathsf{\Pi }$-closed model of T that $\mathfrak{A}{\prec }_{\exists \mathsf{\Pi }}\mathfrak{B}$. But then $\mathfrak{A}\vDash \neg {\phi }_0(\overrightarrow{a},\overrightarrow{d})$ since $\neg {\phi }_0(\overrightarrow{x},\overrightarrow{v})\in \exists \mathsf{\Pi }$, which contradicts the fact that $\mathfrak{A}\vDash {\phi }_0(\overrightarrow{a},\overrightarrow{d})$.

Therefore,

$$T+D_{\mathsf{\Pi }}\left(\mathfrak{A}\right)⊢{\phi }_0(\overrightarrow{a},\overrightarrow{d}).$$

In particular, $T+D_{\mathsf{\Pi }}\left(\mathfrak{A}\right)⊢\exists \overrightarrow{v}{\phi }_0(\overrightarrow{a},\overrightarrow{v})$ and hence $T+D_{\mathsf{\Pi }}\left(\mathfrak{A}\right)⊢\phi \left(\overrightarrow{a}\right)$. By compactness, there exist ${\theta }_1(\overrightarrow{a},\overrightarrow{c}),\cdots ,{\theta }_k(\overrightarrow{a},\overrightarrow{c})\in D_{\mathsf{\Pi }}\left(\mathfrak{A}\right)$ such that $T+{\theta }_1(\overrightarrow{a},\overrightarrow{c})+\cdots +{\theta }_k(\overrightarrow{a},\overrightarrow{c})⊢\phi \left(\overrightarrow{a}\right)$. Since the constant symbols $\overrightarrow{a},\overrightarrow{c}$ do not appear in the language of the theory T, we obtain

$$T⊢{\theta }_1(\overrightarrow{x},\overrightarrow{z})\wedge \cdots \wedge {\theta }_k(\overrightarrow{x},\overrightarrow{z})\to \phi \left(\overrightarrow{x}\right),$$

as required. □

4. Normal Conditional Axioms

After introducing the basic model–theoretic machinery in the previous section, we are now ready to establish our first general conservation theorem between axioms and inference rules. To this end, we first need the following simple yet useful lemma.

Lemma 3.

Let T be a theory and let E be a set of conditional axioms. Then, for every basic fragment Π, $E^{\mathsf{\Pi }}\text{–}Rule$ and $E^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}Rule$ are congruent modulo T.

Proof. 

Since $\mathsf{\Pi }\subseteq \mathcal{B}\left(\mathsf{\Pi }\right)$, it is enough to show that for every theory U extending T, $[U,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]$ extends $[U,E^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}\mathrm{Rule}]$. Even more, since $\mathcal{B}\left(\mathsf{\Pi }\right)$ is closed under conjunctions and negation, it is enough to show that for all $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$ and $\sigma (\overrightarrow{u},\overrightarrow{v})\in \mathcal{B}\left(\mathsf{\Pi }\right)$, if $U⊢\sigma (\overrightarrow{u},\overrightarrow{v})\to \alpha \left(\overrightarrow{v}\right)$, then

$$[U,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]⊢\sigma (\overrightarrow{u},\overrightarrow{v})\to \beta \left(\overrightarrow{v}\right).$$

Given $\sigma (\overrightarrow{u},\overrightarrow{v})\in \mathcal{B}\left(\mathsf{\Pi }\right)$, there are ${\sigma }_{ij}(\overrightarrow{u},\overrightarrow{v})\in \mathsf{\Pi }\cup \neg \mathsf{\Pi }$ such that

$$\sigma (\overrightarrow{u},\overrightarrow{v})\equiv \underset{i=1}{\overset{n}{\bigvee }}\underset{j=1}{\overset{m_i}{\bigwedge }}{\sigma }_{i,j}(\overrightarrow{u},\overrightarrow{v}).$$

Then, since $U⊢\sigma (\overrightarrow{u},\overrightarrow{v})\to \alpha \left(\overrightarrow{v}\right)$, we have

$$U⊢\underset{i=1}{\overset{n}{\bigwedge }}\left(\underset{j=1}{\overset{m_i}{\bigwedge }}{\sigma }_{ij}(\overrightarrow{u},\overrightarrow{v})\to \alpha \left(\overrightarrow{v}\right)\right).$$

Then, n (unnested) applications of $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ give us

$$[U,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]⊢\underset{i=1}{\overset{n}{\bigwedge }}\left(\underset{j=1}{\overset{m_i}{\bigwedge }}{\sigma }_{ij}(\overrightarrow{u},\overrightarrow{v})\to \beta \left(\overrightarrow{v}\right)\right)$$

and, therefore,

$$[U,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]⊢\underset{i=1}{\overset{n}{\bigvee }}\underset{j=1}{\overset{m_i}{\bigwedge }}{\sigma }_{ij}(\overrightarrow{u},\overrightarrow{v})\to \beta \left(\overrightarrow{v}\right),$$

as required. □

The next Proposition establishes a general conservation theorem between a base theory T augmented with a set of conditional axioms E and the associated inference rule theory $T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$, where $\mathsf{\Pi }$ is an appropriate basic fragment. Namely, under very general conditions, it is possible to replace the use of an axiom from E by the use of an inference rule at the price of adding certain side formulas from the class $\mathsf{\Pi }$ during the application of the inference rule.

Proposition 2.

Let T be a theory, let Π be a basic fragment, and let E be a set of conditional axioms such that

• (S1) For every $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$, $\alpha \left(\overrightarrow{v}\right)$ is T-provably equivalent to an $\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ formula; and
• (S2) $T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable.

Then, $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$.

Proof. 

By Lemma 3, $E^{\mathsf{\Pi }}$–Rule and $E^{\mathcal{B}\left(\mathsf{\Pi }\right)}$–Rule are congruent and hence it is sufficient to show that $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+E^{\mathcal{B}\left(\mathsf{\Pi }\right)}$–Rule. Note that $\mathcal{B}\left(\mathsf{\Pi }\right)$ is also a basic fragment and that $\mathcal{B}\left(\mathcal{B}\right(\mathsf{\Pi }\left)\right)=\mathcal{B}\left(\mathsf{\Pi }\right)$. By condition ($S2$) $T+E^{\mathcal{B}\left(\mathsf{\Pi }\right)}$–Rule is $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable. Hence, by Lemma 2 for the basic fragment $\mathcal{B}\left(\mathsf{\Pi }\right)$, it suffices to prove that every $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-closed model of $T+E^{\mathcal{B}\left(\mathsf{\Pi }\right)}$–Rule is a model of $T+E$.

Let $\mathfrak{A}$ be an $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-closed model of $T+E^{\mathcal{B}\left(\mathsf{\Pi }\right)}$–Rule. Consider $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$ and $\overrightarrow{a}\in \mathfrak{A}$ such that $\mathfrak{A}\vDash \alpha \left(\overrightarrow{a}\right)$. We must show that $\mathfrak{A}\vDash \beta \left(\overrightarrow{a}\right)$.

By condition ($S1$), there exists ${\alpha }_0\left(\overrightarrow{v}\right)\in \exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ such that $T⊢\alpha \left(\overrightarrow{v}\right)\leftrightarrow {\alpha }_0\left(\overrightarrow{v}\right)$ and so $\mathfrak{A}\vDash {\alpha }_0\left(\overrightarrow{a}\right)$. By Proposition 1 for the basic fragment $\mathcal{B}\left(\mathsf{\Pi }\right)$, there exist $\theta (\overrightarrow{v},\overrightarrow{z})\in \mathcal{B}\left(\mathsf{\Pi }\right)$ and $\overrightarrow{c}\in \mathfrak{A}$, satisfying

$$\mathfrak{A}\vDash \theta (\overrightarrow{a},\overrightarrow{c})$$

and

$$T+E^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}\mathrm{Rule}⊢\theta (\overrightarrow{v},\overrightarrow{z})\to {\alpha }_0\left(\overrightarrow{v}\right).$$

Then,

$$T+E^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}\mathrm{Rule}⊢\theta (\overrightarrow{v},\overrightarrow{z})\to \alpha \left(\overrightarrow{v}\right)$$

and, by an application of $E^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}\mathrm{Rule}$, we obtain

$$T+E^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}\mathrm{Rule}⊢\theta (\overrightarrow{v},\overrightarrow{z})\to \beta \left(\overrightarrow{v}\right).$$

Therefore, $\mathfrak{A}\vDash \beta \left(\overrightarrow{a}\right)$ since $\mathfrak{A}\vDash T+E^{\mathcal{B}\left(\mathsf{\Pi }\right)}$–Rule and $\mathfrak{A}\vDash \theta (\overrightarrow{a},\overrightarrow{c})$. □

Please note that conditions (S1) and (S2) of the above Proposition are satisfied by every theory and every set of conditional axioms with suitable syntactical complexity. Namely, if T is a $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable theory and E is a set of conditional axioms such that for all $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$ we have $\alpha \left(\overrightarrow{v}\right)\in \exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ and $\beta \left(\overrightarrow{v}\right)\in \forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, then T and E satisfy (S1) and (S2). According to this, in what follows we focus on $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable theories and sets of conditional axioms of restricted syntactical complexity. This motivates the following definitions:

Definition 6.

A formula $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)$ is a normal conditional axiom with respect to Π if (modulo logical equivalence) $\alpha \left(\overrightarrow{v}\right)\in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ and $\beta \left(\overrightarrow{v}\right)\in \forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$.

If, instead, for some theory T, $\alpha \left(\overrightarrow{v}\right)$ is T-provably equivalent to a $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ formula and $\beta \left(\overrightarrow{v}\right)$ is T-provably equivalent to a $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$ formula, then we say that $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)$ is a normal conditional axiom with respect to Π over T.

Remark 3.

In the context of formal arithmetic, there are a good number of combinatorial or logical principles that can be naturally expressed as a set of normal conditional axioms with respect to a suitable basic fragment Π. For instance, the induction principle and the collection or Replacement principles are prominent examples.

In a non-arithmetical context, an interesting example of normal conditional axioms could be the geometric ones (cf. [25]). A geometric axiom is a formula following the geometric axiom scheme below:

$$\forall \overrightarrow{x}\left(P_1\left(\overrightarrow{x}\right)\wedge \cdots \wedge P_n\left(\overrightarrow{x}\right)\to \exists {\overrightarrow{y}}_1{M}_1(\overrightarrow{x},{\overrightarrow{y}}_1)\vee \cdots \vee \exists {\overrightarrow{y}}_m{M}_m(\overrightarrow{x},{\overrightarrow{y}}_m)\right)$$

where each $P_j$ is an atom and each $M_i$ is a conjunction of a list of atoms $Q_{i_1},\dots ,Q_{i_{\ell }}$, and none of the variables in any ${\overrightarrow{y}}_i$ are free in the $P_j$’s.

It is easy to check that a set of geometric axioms, E, is a set of normal conditional axioms with respect to the basic fragment consisting of the atomic formulas of the language, At.

In view of the discussion preceding Definition 6 and as an immediate corollary of Proposition 2, the following result is obtained.

Corollary 1.

Let Π be a basic fragment and let T be a $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable theory. Let E be a set of normal conditional axioms with respect to Π over T. Then, $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+E^{\mathsf{\Pi }}$–Rule.

The previous corollary establishes a broadly applicable conservation result between a set of conditional axioms $T+E$ and the naturally associated inference rule $T+E^{\mathsf{\Pi }}$–Rule. Remarkably, in Corollary 1, we only imposed certain syntactical conditions on the quantifier complexity of the involved theories. Therefore, this conservation phenomenon remains independent of the specific combinatorial or mathematical principles that the set of conditional axioms E could express.

Remark 4.

It is important to notice that these conservation results are properties of the given axiomatizations of the theories $T+E$. That is, there are sets of conditional axioms $E_1$ and $E_2$ such that $T+E_1$ and $T+E_2$ are equivalent theories but the associated inference rules $E^{{\mathsf{\Pi }}_1}\text{–}\mathrm{Rule}$ and $E^{{\mathsf{\Pi }}_2}\text{–}\mathrm{Rule}$ significantly differ in strength.

A set of geometric axioms E can be used to illuminate this aspect of the approach developed in this work. Let us observe that if E is a set of geometric axioms, then each element in E is a conditional axiom $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right),$ where $\alpha \left(\overrightarrow{v}\right)$ is a conjunction of atomic formulas. As a consequence,

$$\frac{\forall \overrightarrow{v}(\alpha \left(\overrightarrow{v}\right)\to \alpha \left(\overrightarrow{v}\right))}{\forall \overrightarrow{v}(\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right))}$$

is an instance of $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ (with $\mathsf{\Pi }=At$) and it follows that, for every theory T, $[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]$ is equivalent to $T+E$, rendering trivial every conservation result between both theories. However, let us observe that if we put

$$D=\{\neg \beta \left(\overrightarrow{v}\right)\to \neg \alpha \left(\overrightarrow{v}\right):\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E\}$$

then $T+E\equiv T+D$ and D is also a set of normal conditional axioms with respect to Π.

By Proposition 2, $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$, but now $T+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is a theory presumably weaker than $T+E$ (since the applications of rule $D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ only produce $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ formulas).

Moreover, Corollary 1 suggests a natural scenario in which the conservativity of $T+E$ over the directly associated inference rule $T+E$–Rule can be established, namely when E–Rule and $E^{\mathsf{\Pi }}$–Rule are shown to be equivalent rules. This prompts the following definition.

Definition 7.

Let T be a theory and let E be a set of conditional axioms. We say that

• E is weakly $\mathsf{\Pi }$-reducible modulo T if $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is derivable from $E\text{–}\mathrm{Rule}$ modulo T.
• E is$\mathsf{\Pi }$-reducible modulo T if $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is reducible to $E\text{–}\mathrm{Rule}$ modulo T.

Paradigmatic examples of $\mathsf{\Pi }$-reducible sets of conditional axioms are provided by the different versions of the induction principle in first-order arithmetics, usually formulated by means of a scheme. In particular, the open induction scheme gives us a simple but very clear example that was already studied in the early 1960s by Shepherdson (see [14]). Let us consider a first-order language L extending the language of first-order arithmetics. Let T be a theory in the language L axiomatized by $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ sentences and let E be the set of conditional sentences generated by the scheme

$$\phi (0,\overrightarrow{v})\wedge \forall x(\phi (x,\overrightarrow{v})\to \phi (x+1,\overrightarrow{v}))\to \forall x\phi (x,\overrightarrow{v})$$

where $\phi (x,\overrightarrow{v})$ varies within the set ${\forall }_0$ of all open formulas of L. Then,

• $(★)$ E is ${\forall }_0$-reducible modulo T.

To see this, it is enough to notice that, given $\phi (x,\overrightarrow{v}),\theta (\overrightarrow{v},\overrightarrow{z})\in {\forall }_0$ such that, for some extension U of T,

$$U⊢\forall \overrightarrow{v}\forall \overrightarrow{z}(\theta (\overrightarrow{v},\overrightarrow{z})\to \phi (0,\overrightarrow{v})\wedge \forall x(\phi (x,\overrightarrow{v})\to \phi (x+1,\overrightarrow{v})))$$

then the sentence $\forall \overrightarrow{v}\forall \overrightarrow{z}(\theta (\overrightarrow{v},\overrightarrow{z})\to \forall x\phi (x,\overrightarrow{v}))$ can be derived in $[U,E\text{–}\mathrm{Rule}]$ from a single instance of $E\text{–}\mathrm{Rule}$ as follows:

Let $\psi (x,\overrightarrow{v},\overrightarrow{z})$ be the formula $\theta (\overrightarrow{v},\overrightarrow{z})\to \phi (x,\overrightarrow{v})$. Then,

$$U⊢\forall \overrightarrow{v}\forall \overrightarrow{z}(\psi (0,\overrightarrow{v})\wedge \forall x(\psi (x,\overrightarrow{v})\to \psi (x+1,\overrightarrow{v})))$$

and, therefore, $[U,E\text{–}\mathrm{Rule}]⊢\forall \overrightarrow{v}\forall \overrightarrow{z}\forall x\psi (x,\overrightarrow{v})$, but this last sentence is easily seen to be equivalent to $\forall \overrightarrow{v}\forall \overrightarrow{z}(\theta (\overrightarrow{v},\overrightarrow{z})\to \forall x\phi (x,\overrightarrow{v}))$.

In [14], the theory $T+E$ was denoted by IAO and $T+E\text{–}\mathrm{Rule}$ by RIO. Bearing in mind Corollary 1 and $(★)$, we obtain an alternative proof of Theorem 2.2 in [14] stating that IAO is ${\forall }_1$-conservative over RIO.

Now we are ready to prove our first general conservation theorem of a theory from $T+E$ over the associated inference rule theory $T+E$–Rule. As a by-product, we will also obtain the conservativity of $T+E$ over a certain parameter-restricted version of that theory. In fact, given a set of conditional axioms E, we define the set of sentences

$$UE=\{\forall \overrightarrow{v}\alpha \left(\overrightarrow{v}\right)\to \forall \overrightarrow{v}\beta \left(\overrightarrow{v}\right):\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E\}$$

(U stands for uniform, for in order to apply an axiom of $UE$, the antecedent $\alpha \left(\overrightarrow{v}\right)$ must be uniformly true, i.e., true for all values of the parameters $\overrightarrow{v}$). It is clear that $T+E$ implies $T+UE$, which, in turn, implies $T+E$–Rule

Theorem 1.

Let T be a $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable theory and let E be a set of normal conditional axioms with respect to Π over T. If E is weakly Π-reducible modulo T, then

1. 

$T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+E\text{–}\mathrm{Rule}$.

2. 

$T+E$ is $\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+UE$.

3. 

In fact, if a theory D satisfies that every extension of $T+D$ is closed under $E\text{–}\mathrm{Rule}$, then $T+E$ is $\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+D$.

Proof. 

Part (1) directly follows from Proposition 2. Note that conditions ($S1$) and ($S2$) in the statement of Proposition 2 are satisfied since E is a set of normal conditional axioms with respect to $\mathsf{\Pi }$ over T and $T+E$–Rule and $T+E^{\mathsf{\Pi }}$–Rule are equivalent since E is assumed to be weakly $\mathsf{\Pi }$-reducible modulo T.

Let us prove part (2). Let $\psi \in \exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ be a sentence such that $T+UE⊬\psi$. Then, $T^{\prime }=T+UE+\neg \psi$ is consistent and $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable; hence, by Lemma 1, there exists an $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-closed model of $T^{\prime }$, say $\mathfrak{A}$.

Observe that $T^{\prime }$ is closed under E–Rule. By weak $\mathsf{\Pi }$-reducibility modulo T and Lemma 3, $T^{\prime }$ is also closed under $E^{\mathcal{B}\left(\mathsf{\Pi }\right)}$–Rule. Hence, reasoning as in the proof of Proposition 2, we obtain that $\mathfrak{A}\vDash T^{\prime }+E$. In particular, $\mathfrak{A}\vDash T+E+\neg \psi$ and so $T+E⊬\psi$.

As for part (3), let us observe that $T+D$ extends $T+UE$ (for otherwise there would be $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$ such that $T+D+\forall \overrightarrow{v}\alpha \left(\overrightarrow{v}\right)⊬\forall \overrightarrow{v}\beta \left(\overrightarrow{v}\right)$ and so $T+D+\forall \overrightarrow{v}\alpha \left(\overrightarrow{v}\right)$ would not be closed under E-Rule, contradicting the hypothesis on D). Hence, part (3) follows from part (2). □

Remark 5.

Theorem 1 provides a general method for proving the conservativity of a set of axioms E over the associated inference rule E–Rule: (i) expressing E as a set of normal conditional axioms with respect to an appropriate basic fragment Π, and (ii) showing that E is weakly Π-reducible (i.e., $E^{\mathsf{\Pi }}$–Rule is derivable from E–Rule).

In the realm of arithmetic, significant results can be derived from this approach. For instance, it can be readily demonstrated that the theory of ${\mathsf{\Sigma }}_1$-induction $I{\mathsf{\Sigma }}_1$ can be formulated as a set of normal conditional axioms with respect to the basic fragment ${\mathsf{\Pi }}_1$. Subsequently, the resulting $E^{{\mathsf{\Pi }}_1}$–Rule can be derived from (or, more precisely, reduced to) ${\mathsf{\Sigma }}_1$–IR modulo $I{\mathsf{\Delta }}_0$. This leads to a proof of the well-known fact regarding the ${\mathsf{\Pi }}_2$ conservativity of $I{\mathsf{\Sigma }}_1$ over $I{\mathsf{\Delta }}_0+{\mathsf{\Sigma }}_1\text{–}\mathrm{IR}$. Through this approach, numerous other significant conservation results for arithmetic theories can be proved.

In the setting of formal number theory, a natural question regarding the proof strength of an arithmetic theory T is to characterize the $\mathsf{\Gamma }$ consequences of the theory; that is, the set of all theorems of T of a fixed quantifier complexity $\mathsf{\Gamma }$. To fix notation, given a theory T and a set of formulas $\mathsf{\Gamma }$ in the language of T, we denote

$$T{h}_{\mathsf{\Gamma }}\left(T\right)=\{\phi \in \mathsf{\Gamma }:\phi \mathrm{is} \mathrm{a} \mathrm{sentence} \mathrm{and} T⊢\phi \}.$$

Two prototypical results in this regard are the well-known facts that $I{\mathsf{\Delta }}_0+{\mathsf{\Sigma }}_1\text{–}\mathrm{IR}$ characterizes the ${\mathsf{\Pi }}_2$ consequences of ${\mathsf{\Sigma }}_1$-induction $T{h}_{{\mathsf{\Pi }}_2}\left(I{\mathsf{\Sigma }}_1\right)$ and that $UI{\mathsf{\Sigma }}_1$ characterizes $T{h}_{{\mathsf{\Sigma }}_3}\left(I{\mathsf{\Sigma }}_1\right)$.

In [17], Kaye already observed that these fundamental facts can be extended to a broader, arithmetic-free context, and that they can be established by using simple model–theoretic arguments. Our Theorem 1 provides an alternative proof of Kaye’s observation. Specifically, suppose that T is a $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable theory and that E is a set of conditional axioms satisfying that if $\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E$, then both $\alpha \left(\overrightarrow{v}\right)$ and $\beta \left(\overrightarrow{v}\right)$ are in $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ (possibly modulo T). Then, $T+E^{\mathsf{\Pi }}$–Rule is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable and $T+UE$ is $\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable. Therefore, if E satisfies the assumptions of Theorem 1, we obtain characterizations of $T{h}_{\forall \mathcal{B}\left(\mathsf{\Pi }\right)}\left(T\right)$ and $T{h}_{\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)}\left(T\right)$. Namely, $T+E^{\mathsf{\Pi }}$–Rule captures, precisely, the $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ consequences of $T+E$, and $T+UE$ captures, precisely, the $\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ consequences of $T+E$.

To close this section, we show how to derive from Theorem 1 another result of Kaye regarding general L-theories. Namely, Theorem 1.1. of [17] establishes that if T is any ${\forall }_{n+1}$-axiomatizable L-theory ($n\ge 1$), then

$$T{h}_{{\exists }_{n+1}}\left(T\right)\equiv T{h}_{\mathcal{B}\left({\exists }_n\right)}\left(T\right).$$

Here we obtain a slightly more general version of this result: if $\mathsf{\Pi }$ is a basic fragment of a language L and T is a $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable L-theory, then $T{h}_{\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)}\left(T\right)$ and $T{h}_{\mathcal{B}(\exists \mathcal{B}(\mathsf{\Pi }\left)\right)}\left(T\right)$ coincide (note that Kaye’s result can be recovered by taking $\mathsf{\Pi }={\forall }_{n-1}$).

Theorem 2.

If T is a $\forall \exists \mathcal{B}\left(\mathsf{\Pi }\right)$-axiomatizable theory, then

$$T{h}_{\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)}\left(T\right)\equiv T{h}_{\mathcal{B}(\exists \mathcal{B}(\mathsf{\Pi }\left)\right)}\left(T\right).$$

Proof. 

Without a loss of generality, it suffices to prove the result under the assumption that the basic fragment $\mathsf{\Pi }$ is closed under boolean combinations. Assume $\mathsf{\Pi }=\mathcal{B}\left(\mathsf{\Pi }\right)$ and let T be any $\forall \exists \mathsf{\Pi }$-axiomatized theory. We must show that $T{h}_{\exists \forall \mathsf{\Pi }}\left(T\right)$ and $T{h}_{\mathcal{B}(\exists \mathsf{\Pi })}\left(T\right)$ are equivalent theories.

First of all, observe that T can be axiomatized by a set of conditional axioms as follows. Let $T_0$ denote the theory in the language of T with no non-logical axioms and define

$$R_T=\{\forall \overrightarrow{y}\neg \phi (\overrightarrow{x},\overrightarrow{y})\to \perp :\forall \overrightarrow{x}\exists \overrightarrow{y}\phi (\overrightarrow{x},\overrightarrow{y})\in T,\phi (\overrightarrow{x},\overrightarrow{y})\in \mathsf{\Pi }\},$$

where $\perp \in \forall \mathsf{\Pi }$ denotes the (false) sentence $\forall x(x\ne x)$. It is clear that $T\equiv T_0+R_T$. Now consider the new set of conditional axioms $E={\left(R_T\right)}^{\mathsf{\Pi }}$; that is, E is the set of conditional axioms given by

$$(\theta (\overrightarrow{x},\overrightarrow{z})\to \forall \overrightarrow{y}\neg \phi (\overrightarrow{x},\overrightarrow{y}))\to (\theta (\overrightarrow{x},\overrightarrow{z})\to \perp ),$$

where $\theta (\overrightarrow{x},\overrightarrow{z})\in \mathsf{\Pi }$, $\forall \overrightarrow{x}\exists \overrightarrow{y}\phi (\overrightarrow{x},\overrightarrow{y})\in T$, and $\phi (\overrightarrow{x},\overrightarrow{y})\in \mathsf{\Pi }$. We also have $T\equiv T_0+E$ and now it is immediate to verify that E is a set of normal conditional axioms with respect to $\mathsf{\Pi }$, which, in addition, is $\mathsf{\Pi }$-reducible modulo $T_0$. By Theorem 1, we obtain that T is $\exists \forall \mathsf{\Pi }$-conservative over $T_0+UE$, which, by definition, is given by the set of sentences

$$\forall \overrightarrow{x}\forall \overrightarrow{z}(\theta (\overrightarrow{x},\overrightarrow{z})\to \forall \overrightarrow{y}\neg \phi (\overrightarrow{x},\overrightarrow{y}))\to \forall \overrightarrow{x}\forall \overrightarrow{z}(\theta (\overrightarrow{x},\overrightarrow{z})\to \perp ),$$

where $\theta (\overrightarrow{x},\overrightarrow{z})\in \mathsf{\Pi }$, $\forall \overrightarrow{x}\exists \overrightarrow{y}\phi (\overrightarrow{x},\overrightarrow{y})\in T$, and $\phi (\overrightarrow{x},\overrightarrow{y})\in \mathsf{\Pi }$. But it is straightforward to check that $UE$ can be rewritten as a set of sentences which, modulo logical equivalence, are in $\mathcal{B}(\exists \mathsf{\Pi })$. Namely,

$$\exists \overrightarrow{x}\exists \overrightarrow{z}\theta (\overrightarrow{x},\overrightarrow{z})\to \exists \overrightarrow{x}\exists \overrightarrow{z}\exists \overrightarrow{y}(\theta (\overrightarrow{x},\overrightarrow{z})\wedge \phi (\overrightarrow{x},\overrightarrow{y})),$$

where $\theta (\overrightarrow{x},\overrightarrow{z})\in \mathsf{\Pi }$, $\forall \overrightarrow{x}\exists \overrightarrow{y}\phi (\overrightarrow{x},\overrightarrow{y})\in T$, and $\phi (\overrightarrow{x},\overrightarrow{y})\in \mathsf{\Pi }$. Consequently, $T{h}_{\mathcal{B}(\exists \mathsf{\Pi })}\left(T\right)$ implies $T_0+UE$, which, in turn, implies $T{h}_{\exists \forall \mathsf{\Pi }}\left(T\right)$ by conservativity. For the opposite direction, observe that (modulo logical equivalence) every $\mathcal{B}(\exists \mathsf{\Pi })$ sentence can be rewritten as an $\exists \forall \mathsf{\Pi }$ sentence. □

5. Finite Sets of Conditional Sentences

In the previous section, we obtained a number of conservation theorems of $T+E$ over $T+E\text{–}\mathrm{Rule}$ or $T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ for a general set of normal conditional axioms E. In this section, we will prove finer conservation results for the particular case where E is a finite set of normal sentences. In other words, we are interested in cases where E can be expressed as

$$\{{\alpha }_1\to {\beta }_1,\cdots ,{\alpha }_m\to {\beta }_m\},$$

where $m\in \omega$ and all ${\alpha }_i$s and ${\beta }_i$s are sentences, i.e., they contain no free variables.

Again, the original motivation for considering these particular sets of conditional axioms comes from results in the context of formal arithmetics. A well-studied fragment of first-order Peano arithmetic is the scheme of parameter-free ${\mathsf{\Sigma }}_1$-induction $I{\mathsf{\Sigma }}_1^{-}$ given by a basic algebraic theory $P^{-}$ together with

$$I_{\phi }:\phi \left(0\right)\wedge \forall x(\phi \left(x\right)\to \phi (x+1))\to \forall x\phi \left(x\right),$$

where $\phi \left(x\right)\in {\mathsf{\Sigma }}_1^{-}$; that is, $\phi \left(x\right)\in {\mathsf{\Sigma }}_1$ and contains no other free variables than the induction variable x. Note that $I{\mathsf{\Sigma }}_1^{-}$ can be seen as a set of normal conditional sentences with respect to $\mathsf{\Pi }={\mathsf{\Pi }}_1$. It is well-known that $I{\mathsf{\Sigma }}_1$ and its parameter-free counterpart $I{\mathsf{\Sigma }}_1^{-}$ share the same ${\mathsf{\Pi }}_2$ consequences (indeed, the ${\mathsf{\Sigma }}_3$ consequences are also preserved), but $I{\mathsf{\Sigma }}_1^{-}$ enjoys the following nice property:

• Let $\theta$ be a ${\mathsf{\Pi }}_2$ sentence. If for some ${\phi }_1\left(x\right),\cdots ,{\phi }_m\left(x\right)\in {\mathsf{\Sigma }}_1^{-}$ we have $I{\mathsf{\Delta }}_0+I_{{\phi }_1}+\cdots +I_{{\phi }_m}⊢\theta$, then ${[I{\mathsf{\Delta }}_0,{\mathsf{\Sigma }}_1\text{–}\mathrm{IR}]}_m⊢\theta$.

The previous property is a well-known conservation theorem for fragments of arithmetic obtained (independently) by Z. Adamowicz, T. Bigorajska, G. Mints, and also by Z. Ratajczyk. The result generalizes to $I{\mathsf{\Sigma }}_n^{-}$ for each $n\ge 1$, but we cannot expect to have a similar result for (parametric) $I{\mathsf{\Sigma }}_1$ since $I{\mathsf{\Sigma }}_1$ is well-known to be finitely axiomatizable.

At first sight, the previous result for $I{\mathsf{\Sigma }}_1^{-}$ could seem to be a very particular property of the induction scheme in the formal arithmetic setting. However, and this was already observed by Kaye in [17], this property again corresponds to a very general purely logical fact for theories described in terms of conditional sentences, see theorem 1.4 in [17] (let us observe that similar results in the context of bounded arithmetic theories have been obtained by Jeřábek in [26].)

In the present section, we shall prove a (slightly more general) version of theorem 1.4 in [17] using our methodology. Namely, we shall obtain a conservation theorem relating the number of conditional sentences needed to derive a $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$ formula from E and the depth of the nested applications of the corresponding $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$, see Theorem 3 below.

Through this section, $\mathsf{\Pi }$ will denote an arbitrary basic fragment. We shall begin with an analysis of $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ when E is a set of conditional sentences but E is not necessarily a finite set. Let us observe that, since E is a set of sentences and, by Lemma 3, $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is congruent with $E^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}\mathrm{Rule}$, it is straightforward to check that $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is congruent with the following rule (that we shall denote by $E_{\forall }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$):

$$\frac{\theta \to \alpha }{\theta \to \beta }(\mathrm{for} \mathrm{each} \mathrm{sentence} \theta \in \exists \mathcal{B}\left(\mathsf{\Pi }\right) \mathrm{and} \alpha \to \beta \in E).$$

This motivates the introduction of a kind of dual version of $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ that we shall denote by $E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$. Instances of this new rule are

$$\frac{\theta \to \alpha }{\theta \to \beta }(\mathrm{for} \mathrm{each} \mathrm{sentence} \theta \in \forall \mathcal{B}\left(\mathsf{\Pi }\right) \mathrm{and} \alpha \to \beta \in E).$$

Please notice that the subscript ∃ in the name of the $E_{\exists }^{\mathsf{\Pi }}$–Rule indicates that, as shown in Theorem 3 below, under certain assumptions, $T+E$ is $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over applications of this rule. Similarly, the subscript ∀ in the name of the $E_{\forall }^{\mathsf{\Pi }}$–Rule indicates that, under certain assumptions, $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over applications of $E_{\forall }^{\mathsf{\Pi }}$–Rule.

Lemma 4.

Let T be a theory and let E be a set of conditional sentences.

1. 

For every sentence $\sigma \in \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, $[T+\sigma ,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]\equiv [T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]+\sigma$.

2. 

For every sentence $\tau \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$, $[T+\tau ,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]\equiv [T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]+\tau .$

Proof. 

(1) We only prove that, for all sentences $\sigma \in \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, $[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]+\sigma$ extends $[T+\sigma ,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]$ (the opposite direction is trivial).

Let $\theta \left(\overrightarrow{u}\right)\in {(\mathsf{\Pi }\cup \neg \mathsf{\Pi })}^{\wedge }$ be such that $T+\sigma ⊢\forall \overrightarrow{u}(\theta \left(\overrightarrow{u}\right)\to \alpha )$, for some sentence $\alpha \to \beta \in E$. Since $\sigma$ is $\exists \overrightarrow{y}{\sigma }_0\left(\overrightarrow{y}\right)$ for some ${\sigma }_0\left(\overrightarrow{y}\right)\in \mathcal{B}\left(\mathsf{\Pi }\right)$ (and we can assume that the variables in $\overrightarrow{y}$ are all different from the ones in $\overrightarrow{u}$), we obtain

$$T⊢\forall \overrightarrow{y}\forall \overrightarrow{u}({\sigma }_0\left(\overrightarrow{y}\right)\wedge \theta \left(\overrightarrow{u}\right)\to \alpha ).$$

But recall that, by Lemma 3, $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is congruent with $E^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}\mathrm{Rule}$, and therefore it follows that $[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]⊢\forall \overrightarrow{y}\forall \overrightarrow{u}({\sigma }_0\left(\overrightarrow{y}\right)\wedge \theta \left(\overrightarrow{u}\right)\to \beta )$. Thus,

$$[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]⊢\sigma \to \forall \overrightarrow{u}(\theta \left(\overrightarrow{u}\right)\to \beta )$$

and the result follows.

(2) We prove that, given $\tau \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$, $[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]+\tau$ extends $[T+\tau ,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]$.

Let $\theta \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ be a sentence such that $T+\tau ⊢\theta \to \alpha$ for some $\alpha \to \beta \in E$. Since $\theta$ and $\tau$ are (respectively) $\forall \overrightarrow{u}{\theta }_0\left(\overrightarrow{u}\right)$ and $\forall \overrightarrow{y}{\tau }_0\left(\overrightarrow{y}\right)$ for some ${\tau }_0\left(\overrightarrow{y}\right),{\theta }_0\left(\overrightarrow{u}\right)\in \mathcal{B}\left(\mathsf{\Pi }\right)$ (and we can assume that the variables in $\overrightarrow{y}$ are all different from the ones in $\overrightarrow{u}$), we obtain

$$T⊢\forall \overrightarrow{y}\forall \overrightarrow{u}({\tau }_0\left(\overrightarrow{y}\right)\wedge {\theta }_0\left(\overrightarrow{u}\right))\to \alpha .$$

So, $[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]⊢\tau \to (\theta \to \beta )$, and the result follows. □

The first interesting fact about sets of conditional sentences is the following improvement of Proposition 2.

Lemma 5.

Let E be a set of conditional sentences such that if $\alpha \to \beta \in E$, then $\alpha \in \mathcal{B}(\forall \mathcal{B}(\mathsf{\Pi }\left)\right)$. Then, for every theory T, $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$.

Proof. 

Let $T_1$ denote the theory axiomatized by $T{h}_{\forall \mathcal{B}\left(\mathsf{\Pi }\right)}(T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule})$. We shall prove that every $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-closed model of $T_1$ is a model of $T{h}_{\forall \mathcal{B}\left(\mathsf{\Pi }\right)}(T+E)$. Thus, the result will follow from Lemma 2.

Let $\mathfrak{A}$ be an $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-closed model of $T_1$. First of all, note that

• (•) $(T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule})+D_{\mathcal{B}\left(\mathsf{\Pi }\right)}\left(\mathfrak{A}\right)$ is consistent.
• Proof of (•): For otherwise by compactness, there would exist $\delta \left(\overrightarrow{v}\right)\in \mathcal{B}\left(\mathsf{\Pi }\right)$ and $\overrightarrow{a}\in \mathfrak{A}$ satisfying $\mathfrak{A}\vDash \delta \left(\overrightarrow{a}\right)$ and $T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}⊢\forall \overrightarrow{v}\neg \delta \left(\overrightarrow{v}\right)$. Since $\forall \overrightarrow{v}\neg \delta \left(\overrightarrow{v}\right)\in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$, we would have $\mathfrak{A}\vDash \forall \overrightarrow{v}\neg \delta \left(\overrightarrow{v}\right)$, a contradiction.

Hence, there exists $\mathfrak{B}\vDash T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ such that $\mathfrak{A}{\prec }_{\mathcal{B}\left(\mathsf{\Pi }\right)}\mathfrak{B}$. Let us show that $\mathfrak{B}\vDash E$.

Pick $\alpha \to \beta \in E$ such that $\mathfrak{B}\vDash \alpha$. It follows from $\mathfrak{A}{\prec }_{\mathcal{B}\left(\mathsf{\Pi }\right)}\mathfrak{B}$ and the fact that $\mathfrak{A}$ is an $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-closed model of $T_1$ that $\mathfrak{A}{\prec }_{\exists \mathcal{B}\left(\mathsf{\Pi }\right)}\mathfrak{B}$. Since $\alpha \in \mathcal{B}(\forall \mathcal{B}(\mathsf{\Pi }\left)\right)$ and $\mathfrak{A}{\prec }_{\exists \mathcal{B}\left(\mathsf{\Pi }\right)}\mathfrak{B}$, we also have $\mathfrak{A}\vDash \alpha$. But note that every $\mathcal{B}(\forall \mathcal{B}(\mathsf{\Pi }\left)\right)$ sentence can be rewritten (modulo logical equivalence) as an $\exists \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ sentence.

Therefore, by applying Proposition 1, we obtain that there exist $\overrightarrow{a}\in \mathfrak{A}$ and $\theta \left(\overrightarrow{z}\right)\in \mathcal{B}\left(\mathsf{\Pi }\right)$ such that $\mathfrak{A}\vDash \theta \left(\overrightarrow{a}\right)$ and $T_1⊢\exists \overrightarrow{z}\theta \left(\overrightarrow{z}\right)\to \alpha$. Then,

$$T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}⊢\exists \overrightarrow{z}\theta \left(\overrightarrow{z}\right)\to \beta$$

(recall that $E^{\mathsf{\Pi }}$ and $E^{\mathcal{B}\left(\mathsf{\Pi }\right)}$ are congruent rules) and so $\mathfrak{B}\vDash \exists \overrightarrow{z}\theta \left(\overrightarrow{z}\right)\to \beta$. But, $\mathfrak{B}\vDash \exists \overrightarrow{z}\theta \left(\overrightarrow{z}\right)$ since $\mathfrak{A}{\prec }_{\mathcal{B}\left(\mathsf{\Pi }\right)}\mathfrak{B}$. Therefore, $\mathfrak{B}\vDash \beta$, as required.

We have thus shown that there is $\mathfrak{B}\vDash T+E$ such that $\mathfrak{A}{\prec }_{\mathcal{B}\left(\mathsf{\Pi }\right)}\mathfrak{B}$ and, therefore, $\mathfrak{A}\vDash T{h}_{\forall \mathcal{B}\left(\mathsf{\Pi }\right)}(T+E)$, as required. □

We now turn to the study of the case where E is a finite set of conditional sentences. First, we introduce some notation. If $E=\left\{\psi \right\}$, where $\psi$ is a conditional sentence, then $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ will be denoted by ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ and $E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ will be denoted by ${\psi }_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$. The next lemma shows that for every conditional sentence $\psi$, nested applications of ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ (or ${\psi }_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$) collapse to unnested applications of the rule.

Lemma 6.

Assume ψ is a conditional sentence of the form $\alpha \to \beta$.

1. 

If $\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$, then $[T,{\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]\equiv T+{\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$.

2. 

If $\alpha \in \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, then $[T,{\psi }_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]\equiv T+{\psi }_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}.$

Proof. 

(1): By Lemma 3, ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ and ${\psi }^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}\mathrm{Rule}$ are congruent, and thus we can assume, without loss of generality, that $\mathsf{\Pi }$ is closed under boolean combinations (that is, $\mathsf{\Pi }=\mathcal{B}\left(\mathsf{\Pi }\right)$). In addition, we also take advantage of the fact that, since we are dealing with conditional sentences, each instance of ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ can be easily transformed into an equivalent instance of ${\psi }_{\forall }^{\mathsf{\Pi }}$. Thus, in the following proofs, we shall deal with instances of ${\psi }_{\forall }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$, although we refer to them as instances of ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$.

First, we show that $k\ge 1$ unnested applications of ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ can be replaced by a single unnested application of this rule: Let $\theta$ be an $\exists \mathsf{\Pi }$ sentence equivalent to ${\bigvee }_{i=1}^k{\theta }_i$, where ${\theta }_1,\cdots ,{\theta }_k\in \exists \mathsf{\Pi }$ are sentences such that for each $i=1,\cdots ,k$, we have $T⊢{\theta }_i\to \alpha$. Then, $T⊢\theta \to \alpha$, and as a consequence, since for each $i=1,\cdots ,k$,

$$T⊢(\theta \to \beta )\to ({\theta }_i\to \beta ),$$

we obtain that these k applications of ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ corresponding to ${\theta }_1,\cdots ,{\theta }_k$ can be replaced by the instance given by the sentence $\theta$.

Now we show how to deal with nested applications of ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$. Let ${\theta }_1,{\theta }_2\in \exists \mathsf{\Pi }$ be sentences such that

$$T⊢{\theta }_1\to \alpha , \mathrm{and} T+({\theta }_1\to \beta )⊢{\theta }_2\to \alpha .$$

Let $\theta \in \exists \mathsf{\Pi }$ be a sentence equivalent to ${\theta }_1\vee {\theta }_2$. Let us see that $T⊢\theta \to \alpha$.

Indeed, we argue using T and assume that $\theta$ holds. Firstly, if ${\theta }_1$ holds, then we obtain $\alpha$ since $T⊢{\theta }_1\to \alpha$ by our hypothesis. Secondly, if ${\theta }_1$ does not hold, then we have ${\theta }_1\to \beta$ and ${\theta }_2$. But, since by hypothesis $T+({\theta }_1\to \beta )⊢{\theta }_2\to \alpha$, it follows that ${\theta }_2\to \alpha$. As a consequence, we obtain $\alpha$ again, as required.

We showed that $T⊢\theta \to \alpha$ and therefore one application of ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is enough to derive $\theta \to \beta$, which is equivalent to $({\theta }_1\to \beta )\wedge ({\theta }_2\to \beta )$. So, two nested applications of ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ can be replaced by one unnested application of the rule, and the equivalence between $[T,{\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]$ and $T+{\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ follows.

(2) A straightforward modification of the previous proof allows us to derive part (2). We must notice that ${\psi }_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ is congruent with ${\psi }_{\exists }^{\mathcal{B}\left(\mathsf{\Pi }\right)}\text{–}\mathrm{Rule}$, as can be easily seen. □

Now we consider a finite set $E=\{{\psi }_1,\cdots ,{\psi }_m\}$ of conditional sentences. In this case, applications of the corresponding $E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ (respectively, $E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$) can be described in terms of the set of rules ${{\psi }_j}^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ (respectively, ${\left({\psi }_j\right)}_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$), $j=1,\cdots ,m$. We shall study the interaction of these m rules and derive a collapse result.

Proposition 3.

Let $E=\{{\psi }_1,\cdots ,{\psi }_m\}$ be a finite set of conditional sentences with cardinal m. Then, for every theory T,

1. 

If for every $\alpha \to \beta \in E$, $\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$, then $T+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}\equiv {[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m$.

2. 

If for every $\alpha \to \beta \in E$, $\alpha \in \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, then $T+E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}\equiv {[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m$.

Proof. 

(1) As we pointed out in the proof of Lemma 6, we can assume, without loss of generality, that $\mathsf{\Pi }$ is closed under boolean combinations. In addition, we deal with instances of ${\psi }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ as instances of ${\psi }_{\forall }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$. Now, the proof proceeds by induction on $m\ge 1$, the number of sentences in the set E.

• $m=1$: In this case, the result is just part (1) in Lemma 6.
• $m\to m+1$: Consider $E=\{{\psi }_1,\cdots ,{\psi }_m,{\psi }_{m+1}\}$ where for each $j,1\le j\le m+1$, ${\psi }_j$ is a conditional sentence ${\alpha }_j\to {\beta }_j$ with ${\alpha }_j\in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$. We assume that the result holds for every set of conditional sentences with cardinal m.

In order to derive the result for E, it is enough to show that ${[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m+1}$ is closed under ${\psi }_j^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ for each $j=1,\cdots ,m+1$. Let us assume that

$${[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m+1}⊢\theta \to {\alpha }_p$$

for some p$(1\le p\le m+1)$ and $\theta \in \exists \mathsf{\Pi }$. Put $D=E-\left\{{\psi }_p\right\}$. It is enough to show that ${[T,D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m⊢\theta \to {\alpha }_p$, since then it will follow that ${[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m+1}⊢\theta \to {\beta }_p$, as required.

We observe that $\neg {\alpha }_p$ is equivalent to an $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$ sentence and, as a consequence, by Lemma 4,

$${[T,D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m+\neg {\alpha }_p\equiv {[T+\neg {\alpha }_p,D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m.$$

Now the crucial point is the following fact:

• Claim: $(T+\neg {\alpha }_p)+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}extendsT+E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}.$
• Proof of Claim: We shall prove this by showing, by induction on $k\ge 1$, that for all $k\ge 1$, $(T+\neg {\alpha }_p)+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ extends ${[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_k$:
  • $•$ For $k=1$, this is straightforward in view of the following easy fact: if S extends T and $S⊢\sigma \to {\alpha }_p$ for some sentence $\sigma \in \exists \mathsf{\Pi }$, then $S+\neg {\alpha }_p⊢\sigma \to {\beta }_p$.
  • $•$ Assume that for some $k\ge 1$ the result holds, and assume that

    $${[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_k⊢\sigma \to {\alpha }_j$$

    for some j, $(1\le j\le m+1)$ and $\sigma \in \exists \mathsf{\Pi }$. By the induction hypothesis on k,

    $$(T+\neg {\alpha }_p)+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}⊢\sigma \to {\alpha }_j$$

    and we can now distinguish two cases:

    ·

    If $j\ne p$, then obviously $(T+\neg {\alpha }_p)+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}⊢\sigma \to {\beta }_j.$

    ·

    If $j=p$, then, as in case $k=1$, ${[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_k+\neg {\alpha }_p⊢\sigma \to {\beta }_p$. But, by the induction hypothesis on k, $(T+\neg {\alpha }_p)+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ extends ${[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_k$; so,

    $$(T+\neg {\alpha }_p)+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}⊢\sigma \to {\beta }_p$$

    as required.

  • This proves the claim. □

Consider $\mathfrak{A}\vDash {[T,D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m$. If $\mathfrak{A}\vDash {\alpha }_p$, then, obviously, $\mathfrak{A}\vDash \theta \to {\alpha }_p$; hence, let us assume that $\mathfrak{A}\vDash \neg {\alpha }_p$. Then,

$$\mathfrak{A}\vDash {[T,D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m+\neg {\alpha }_p.$$

Now, by the induction hypothesis (on m), ${[T,D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m\equiv T+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$, and so

$$\mathfrak{A}\vDash (T+\neg {\alpha }_p)+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}.$$

In view of the claim above, we obtain $\mathfrak{A}\vDash {[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m+1}$, and therefore, $\mathfrak{A}\vDash \theta \to {\alpha }_p$. This shows that ${[T,D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m⊢\theta \to {\alpha }_p$ and concludes the proof.

(2): It is easy to adapt the proof of item (1). We omit the details. □

Remark 6.

Let us note that Proposition 3 also holds for every finite set of conditional sentences, E, satisfying that for all $\alpha \to \beta \in E$, $\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)\cup \exists \mathcal{B}\left(\mathsf{\Pi }\right)$.

For instance, we can deal with part (2) of Proposition 3 just by putting

$$E_1=\{\alpha \to \beta \in E:\alpha \in \exists \mathcal{B}\left(\mathsf{\Pi }\right)\},and{E}_2=\{\alpha \to \beta \in E:\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)\}$$

and having in mind that for all T, if $\alpha \to \beta \in E_2$, then we obtain $[T,{\left(E_2\right)}_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]⊢\alpha \to \beta$, since $\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$ and $T⊢\alpha \to \alpha$. Therefore, $[T,{\left(E_2\right)}_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]\equiv T+E_2$, and it follows that

$${[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m\equiv {[[T,{\left(E_2\right)}_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}],{\left(E_1\right)}_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m_1}\equiv T+E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$$

where $m_1=\left|E_1\right|$. We can deal with part (1) in a similar way.

We are now in a position to prove the main result of the present section. From Proposition 3 and Lemma 5, we derive the following version of theorem 1.4 of [17].

Theorem 3.

Let T be a theory and let E be a finite set of conditional sentences such that for every $\alpha \to \beta \in E$, $\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)\cup \exists \mathcal{B}\left(\mathsf{\Pi }\right)$. Let m be the number of elements of E. Then,

1. 

$T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over ${[T,E^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m$.

2. 

$T+E$ is $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over ${[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m$.

Proof. 

In view of Remark 6, part (1) follows from Lemma 5 and Proposition 3.

We give a direct proof for part (2).

Let $\phi \in \exists \mathcal{B}\left(\mathsf{\Pi }\right)$ be a sentence such that $T+E⊢\phi$. We shall prove that ${[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m⊢\phi$ by induction on $m\ge 1$:

$m=1$: If $E=\{\alpha \to \beta \}$ and $T+(\alpha \to \beta )⊢\phi$, then $T⊢\neg \phi \to \neg (\alpha \to \beta )$. As a consequence, $T⊢(\neg \phi \to \alpha )\wedge (\neg \phi \to \neg \beta )$. Since $\neg \phi \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)$, we obtain

$$[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]⊢\neg \phi \to \beta$$

and, therefore, $[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]⊢\phi$.

$m\to m+1$: Let $E=\{{\alpha }_1\to {\beta }_1,\cdots ,{\alpha }_{m+1}\to {\beta }_{m+1}\}$ be a set of sentences. First, we consider the case where ${\alpha }_j\in \exists \mathcal{B}\left(\mathsf{\Pi }\right)$ for all $j=1,\cdots ,m+1$. Let $\phi \in \exists \mathcal{B}\left(\mathsf{\Pi }\right)$ be a sentence such that $T+{\bigwedge }_{j=1}^{m+1}({\alpha }_j\to {\beta }_j)⊢\phi$. Then,

$$T⊢\neg \phi \to \neg \underset{j=1}{\overset{m+1}{\bigwedge }}({\alpha }_j\to {\beta }_j)$$

and, in particular, it follows that $T⊢\neg \phi \to {\bigvee }_{j=1}^{m+1}\neg {\beta }_j$. For each $l=1,\cdots ,m+1$, let $T_l$ be the theory $T+E_l$ where $E_l=E-\{{\alpha }_l\to {\beta }_l\}$. Then, $T_l+({\alpha }_l\to {\beta }_l)⊢\phi$, and reasoning as in case $m=1$, we obtain $T_l⊢\neg \phi \to {\alpha }_l$. If ${\alpha }_l\in \exists \mathcal{B}\left(\mathsf{\Pi }\right)$, then by the induction hypothesis, ${[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m⊢\neg \phi \to {\alpha }_l$. We proved in this way that for all l$(1\le l\le m+1)$, ${[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m+1}⊢\neg \phi \to {\beta }_l$. As a consequence,

$${[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m+1}⊢\neg \phi \to \underset{j=1}{\overset{m+1}{\bigwedge }}{\beta }_j$$

and it follows that ${[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m+1}⊢\phi$.

For the general case, we put

$$E_1=\{\alpha \to \beta \in E:\alpha \in \exists \mathcal{B}\left(\mathsf{\Pi }\right)\}and{E}_2=\{\alpha \to \beta \in E:\alpha \in \forall \mathcal{B}\left(\mathsf{\Pi }\right)\}$$

and observe that $T+E_2\equiv [T,{\left(E_2\right)}_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]$. Then, by the previous restricted case, $T+E$ is $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over ${[T+E_2,{\left(E_1\right)}_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m_1}$ (where $m_1=\left|E_1\right|$). Hence, $T+E$ is $\exists \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over

$${[[T,{\left(E_2\right)}_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}],{\left(E_1\right)}_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_{m_1}$$

which is, obviously, a subtheory of ${[T,E_{\exists }^{\mathsf{\Pi }}\text{–}\mathrm{Rule}]}_m$. □

Corollary 2.

Let E be a set of normal conditional axioms with respect to Π over T such that E is Π-reducible modulo T. If F is a finite subset of $UE$ with m elements or F is a finite set of m sentences included in E, then

$$T{h}_{\forall \mathcal{B}\left(\mathsf{\Pi }\right)}(T+F)\subseteq {[T,E\text{–}\mathrm{Rule}]}_m.$$

6. Conclusions and Future Work

Both in pure and in applied logic, the question of whether it is more convenient to formalize a certain mathematical principle as an axiom or as an inference rule is important and ubiquitous.

In this work, we developed a general logical framework that allows for replacing axioms with corresponding inference rules without greatly affecting the proof–theoretical strength, preserving theorems up to a certain level of quantifier complexity. While these results are familiar to logicians working in arithmetic formal theories, we believe they could also benefit a broader audience in logic.

The proof methods we use are conceptually very simple: we essentially combine syntactical manipulations and basic model–theoretic constructions. This should make the article accessible to a wide audience.

Several avenues for future research suggest themselves. Firstly, it is natural to ask whether the main results of the present paper also hold for other settings different from classical first-order logics (such as, for example, intuitionistic logic or minimal logic). In order to explore this line of future work, one should have to isolate first a suitable notion that could play the role of the $\exists \mathsf{\Pi }$-closed models for these new settings. Secondly, and still from a theoretical point of view, it would also be of interest to explore possible applications of the obtained results to other formal theories different from the arithmetical ones (for example, theories axiomatized by geometric axioms could serve as a first field of study). Finally, from an applied perspective, it would be desirable to investigate possible applications to rule-based reasoning in computational logic. In areas such as logic programming, expert systems, or the Semantic Web, rule-based knowledge representation is a crucial and powerful tool, and implementations of rule-based systems naturally emerge. A formal analysis of the axioms-as-rules strategy could be of interest in these fields.

We close this paper with some pointers to the kind of applications that we think deserve further exploration.

6.1. Description Logics

Conditional axioms are frequently used as "general axioms" in description logics. For example, in $\mathcal{ALC}$ logic, consider the axiom

$$\exists r_1.\forall r_{2}A⊑\forall s_1.\exists s_2.B$$

which, when translated to first-order logic (with A and B being concept names translated to unary predicates and roles r, $s_1$, and $s_2$ as binary relations), becomes

$$\forall x(\exists y_1(r_1(x,y_1)\wedge \forall y_2(r(y_1,y_2)\to A\left(y_2\right)))\to \forall z_1(s_1(x,z_1)\to \exists z_2(s_2(z_1,z_2)\wedge B\left(z_2\right))))$$

which is equivalent to the normal condition axiom (defined in Section 4):

$$\exists y_1\forall y_2(r_1(x,y_1)\wedge (r(y_1,y_2)\to A\left(y_2\right)))\to \forall z_1\exists z_2(s_1(x,z_1)\to (s_2(z_1,z_2)\wedge B\left(z_2\right)))$$

An example of the utility of introducing rules would be as a mechanism for simplification through design patterns. Consider the following example extracted from [27]:

$$\begin{array}{cc}\hfill {\mathcal{O}}_1=\{\mathrm{Jaguar}⊑\mathrm{Animal},& \mathrm{Jaguar}⊑\forall \mathrm{hasChild}.\mathrm{Jaguar},\hfill \\ \hfill \mathrm{Tiger}⊑\mathrm{Animal},& \mathrm{Tiger}⊑\forall \mathrm{hasChild}.\mathrm{Tiger},\hfill \\ \hfill \mathrm{Lion}⊑\mathrm{Animal},& \mathrm{Lion}⊑\forall \mathrm{hasChild}.\mathrm{Lion}\}\hfill \end{array}$$

Note that, since it is not possible to quantify over concepts in typical description logics, expressing the fact that every subclass of animals only has a child of the same subclass is not feasible. Nevertheless, by employing a certain type of (meta)rules [27], it is possible to obtain a representation of such information, which allows for the elimination of certain axioms from the ontology:

$${\mathcal{O}}_2=\{\mathrm{Jaguar}⊑\mathrm{Animal},\mathrm{Tiger}⊑\mathrm{Animal},\mathrm{Lion}⊑\mathrm{Animal}\}$$

$$g:\underset{\mathrm{Body}}{\underbrace{\{?X⊑\mathrm{Animal}\}}}\to \underset{\mathrm{Head}}{\underbrace{\{?X⊑\forall \mathrm{hasChild}.?X\}}},$$

which could be added to the standard tableau-based consistency class algorithm as a rule that acts on classes:

$$R:\frac{a:?X⊑\mathrm{Animal}}{a:?X⊑\forall \mathrm{hasChild}.?X}$$

The question that arises with this transformation is what degree of conservativity is maintained between the original ontology ${\mathcal{O}}_1$ and the new representation ${\mathcal{O}}_2+R$.

In the framework of first-order logic, we could deal with g as an axiom scheme, where X ranges over a convenient class of formulas. In this way, we could obtain a set of conditional axioms E and applications of the (meta)rule R that will correspond to applications of the $E\text{–}\mathrm{Rule}$. Nevertheless, although we do not discard that some conservation results could be derived by a more or less direct application of the machinery developed in this paper, the chief question here would be: Is it possible to derive, in the setting of description logics, some results and techniques similar to the ones developed in this paper for first-order theories? In particular, can such an approach be useful in settling the exact conservation between the ontologies ${\mathcal{O}}_1$ and ${\mathcal{O}}_2+R$ (or other similar cases)?

6.2. Coherent/Geometric Logic

In Remark 3, we briefly discussed the notion of a (finitary) geometric axiom (also known as a coherent formula). There we pointed out that a set E of geometric axioms provides us with an example of a normal set of conditional axioms with respect to the basic fragment $\mathsf{\Pi }$ of all atomic formulas of the language. We also noticed that if we put

$$D=\{\neg \beta \left(\overrightarrow{v}\right)\to \neg \alpha \left(\overrightarrow{v}\right):\alpha \left(\overrightarrow{v}\right)\to \beta \left(\overrightarrow{v}\right)\in E\}$$

then $T+E\equiv T+D$, and D is also a set of normal conditional axioms with respect to $\mathsf{\Pi }$. Therefore, by Proposition 2, $T+E$ is $\forall \mathcal{B}\left(\mathsf{\Pi }\right)$-conservative over $T+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$.

It is a theorem of Barr that if a geometric sentence is derivable from a geometric theory using classical (first-order) logic, then it is also derivable using intuitionistic logic. As noted in [25], this result can be easily derived using a cut–elimination argument. However, can the model–theoretic methods that we presented in this paper be adapted to derive Barr’s theorem or some related result?

Towards a positive answer to this problem, the following question could be considered. In [28], Coste, Lombardi, and Roy deal with dynamical theories axiomatized by geometric axioms (in [28], the term "dynamical axiom" is used to refer to geometric axioms). A key notion in that work is the notion of a dynamical proof (closely related to a derivation of a basic sequence in a cut-free system with mathematical rules, as pointed out in [25]). Theorem 1.1 in [28] shows that there is a construction associating a dynamical proof to each classical proof of an atomic formula B from a set of atomic formulas R. Is it possible to transform a proof of a geometric sentence in $T+D^{\mathsf{\Pi }}\text{–}\mathrm{Rule}$ in (some kind of) a dynamical proof?

6.3. Inference Rules and Automated Reasoning

The examples we just mentioned are interesting not only from a theoretical point of view. The inference rules we described in these examples can be implemented as tools for automated reasoning. Automated theorem proving is an important research field with applications in Artificial Intelligence and Program Verification (just to mention two application areas). Inference rules provide the base for efficient implementations of the reasoning principles expressed by conditional axioms. In addition to providing a guide to the search for appropriate inference rules, the results presented in this paper can play a fundamental role in the analysis of the formal properties (correctness, completeness, conservativeness,…) of the systems finally developed.

A classic example of such use is provided by the Boyer–Moore Nqthm theorem prover [29] and the closely related system ACL2 [30], developed by Kaufmann and Moore, used in the modeling and verification of computer hardware and software. In these systems, the (noetherian) induction principle is implemented as an inference rule that provides a powerful tool to derive properties of functions defined by recursion. Model–theoretic methods play an important role in the proofs of the correctness properties of ACL2, as shown in [31].