1 Introduction
According to a philosophical tradition dating back to Aristotle’s Posterior Analytics [Reference Barnes3, Post. An. I, 2–8], certain proofs do not only certify the truth of their conclusion but also display the reasons why their conclusion holds. In the contemporary philosophical literature, the grounding relation—an objective, explanatory relation which can be traced back to Bolzano’s notion of Abfolge [Reference Bolzano4]—is receiving considerable attention in several fields of philosophy. Grounding is usually introduced as the relation that connects two relata if the first—the ground—constitutes a reason why the second—the consequence—holds. Much work is being devoted to characterising grounding for logical formulae in terms of deduction rules, see for instance [Reference Correia6, Reference Poggiolesi19, Reference Schnieder22], but no study focusing on the difference between rules for logical grounding and rules for logical reasoning exists. In this work, we fill this gap by an in-depth formal analysis of the relationship between grounding and logical rules for classical and intuitionistic logic.
It has been shown in [Reference Genco11] that grounding rules defined according to the notion of grounding introduced in [Reference Poggiolesi18] and inspired by Bolzano’s notion of Abfolge can be effectively used as logical introduction rules. In particular, it is possible to define a grounding calculus which is also a complete calculus for classical logic by employing grounding rules instead of certain logical introduction rules. The work presented in [Reference Genco11] moreover includes a proof that the presented calculus normalises and hence that the employed grounding rules are proof-theoretically balanced with respect to logical elimination rules. This balance matches the one between logical rules for introducing connectives and logical rules for eliminating connectives, and implies that by eliminating a connective we do not obtain more than what is required to introduce it. Therefore, we know that the information that the premisses of a grounding rule are derivable already contains all the information that we can obtain from its conclusion by an elimination rule application. This result leaves a question open though, since the calculus introduced in [Reference Genco11] does not only contain grounding rules for introducing connectives, but also contains one logical introduction rule. Indeed, the grounding rules for negation are too strict with respect to the traditional negation introduction rule and hence not enough to define a complete calculus for classical logic. The simple solution to this problem adopted in [Reference Genco11] is to include also an unrestricted version of the negation introduction rule 
in the calculus. The addition of this rule yields a complete and normalising calculus, but it is not immediately apparent whether a subtler solution is possible. Could we not find a more meaningful way to reintegrate what grounding rules lack with respect to logical introduction rules? Moreover, are there logical rules which give us some intuition about what grounding rules are precisely missing to become a sufficient set of introduction rules? We positively answer this question by defining the calculus
$\mathrm {G_{CL}}$
which only contains grounding rules as introduction rules. The calculus essentially relies on the presence of a rule, often called classical dilemma, corresponding to a disjunction elimination applied to an instance of the excluded middle law
$A\vee \neg A $
:
As we will argue, this answer to the question about what grounding rules are missing with respect to logical introduction rules is essentially tied to the nature of grounding as an explanatory relation. The formal role of the classical dilemma rule in this calculus can be given a precise philosophical interpretation which clarifies the nature of grounding rules and presents strong connections with the notion of informational analyticity discussed in [Reference d’Agostino7, Reference D’Agostino8]. The introduced grounding calculus
$\mathrm {G_{CL}}$
thus gives us a very precise idea of what kind of logical derivations are grounding derivations and, even though it constitutes a confirmation of the fact that grounding derivations are logical derivations of a particular kind, it does not trivialise the difference between grounding rules and logical rules, explanatory and non-explanatory parts of a logical derivation.
This result raises a further question though. Since classical logic can be defined by adding the law of excluded middle to intuitionistic logic, and since adding this law to a set of grounding rules and elimination rules yields a calculus for classical logic, could it not be that grounding rules exactly correspond to intuitionistic introduction rules? A positive answer to this question would agree with a quite widespread belief that grounding should be closer to intuitionistic reasoning—or at least to some kind of constructive reasoning—than to classical reasoning. Indeed, Bolzano himself stressed that Abfolge derivations should not feature arguments by reductio ad absurdum. Nevertheless, an exact correspondence between grounding rules and intuitionistic introduction rules does not hold. While it is true that grounding derivations do not contain non-constructive reasoning steps, as we will show, grounding rules alone are not strong enough to constitute a suitable set of introduction rules for intuitionistic logic either.Footnote 1
Before introducing the calculi that we will employ, let us discuss Bolzano’s notion of truth and its relation with Abfolge, classical and intuitionistic logic.
1.1 Bolzano, grounding, classical and intuitionistic logic
Quite clearly, Bolzano’s notion of truth is much more compatible with a classical notion of truth rather than with an intuitionistic one. According to Bolzano, indeed, truth does not depend in any way on its relation to a subject or on the existence of any evidence for it. The following remark clearly witnesses this:
The number of blossoms that were on a certain tree last spring is a statable, if unknown, figure. Thus, the proposition which states this figure I call an objective truth, even if nobody knows it. [Reference Bolzano4, WL §25]
This stance by Bolzano is decidedly incompatible with an intuitionistic notion of truth, according to which something is true only insofar as a mental construction proves it true, see for instance [Reference Iemhoff and Zalta16]. In [Reference Bolzano4, WL §125], moreover, Bolzano extensively discusses his position according to which a proposition is either true or false, and no other possibility is admitted, which evidently matches the classically valid—but not intuitionistically valid—law of the excluded middle:
$A\vee \neg A$
. Therefore, from a technical perspective, Bolzano’s background logic is clearly classical logic, see also [Reference van Benthem26] for a detailed discussion on the topic. Nevertheless, the notion of Abfolge presents strong similarities with intuitionistic derivability. Indeed, as Bolzano argues in [Reference Bolzano4, §530], while logical derivations can feature apagogic reasoning steps—that is, by reductio ad absurdum—this kind of reasoning does not appear among what can be legitimately employed in Abfolge derivations, see also [Reference Hafner15] and [Reference Rumberg21] on the subject. Hence, since according to Bolzano an Abfolge derivation is a particular kind of logical derivation, Abfolge might be taken to define a fragment of the class of classical derivations which is identical—or at least very closely related—to the one induced by intuitionistic derivability. As we will see, though, this is not the case. Indeed, if we define a derivability relation on the basis of Bolzano’s Abfolge, we obtain a notion of derivability which is much stricter than the one based on intuitionistic logical introduction rules.
The rest of the article is structured as follows. In Section 2 we present the simple grounding calculus
$\mathrm {Gr}$
and we show that it is sound and complete with respect to classical logic. In Section 3 we present the refinement
$\mathrm {G_{CL}}$
of the calculus
$\mathrm {Gr}$
which only contains grounding rules as introduction rules; we moreover show that the rules of
$\mathrm {Gr}$
that are not rules of
$\mathrm {G_{CL}}$
are eliminable, and hence that also
$\mathrm {G_{CL}}$
is sound and complete with respect to classical logic. In Section 3.2 we investigate the conceptual significance of
$\mathrm {G_{CL}}$
with respect to the distinction between grounding and logical rules for classical logic. In Section 4, we analyse the relationship between grounding rules and logical rules for intuitionistic logic. We conclude in Section 5 with a brief summary of the presented work.
2 A simple grounding calculus
We formally define the grounding calculus
$\mathrm {Gr}$
for classical logic based on the notion of complete logical grounding introduced in [Reference Poggiolesi18, Reference Poggiolesi19]. The grounding rules of
$\mathrm {Gr}$
are the propositional grounding rules of the calculus presented in [Reference Genco, Poggiolesi and Rossi13]. The logical language that we will consider is the language of propositional classical logic:
$$\begin{align*}\varphi \, ::= \, \xi \, \mid \, \bot \, \mid \, \neg \varphi \, \mid \, \varphi \wedge \varphi \, \mid \, \varphi \vee \varphi \, \mid \, \varphi \rightarrow \varphi \quad\quad \xi \, ::= \, p \, \mid \, q \, \mid \, r \, \mid \ldots,\end{align*}$$
where
$p, q, r, \ldots $
are propositional variables.
We adopt the usual conventions concerning parentheses. In particular, negations bind more strictly than binary connectives,
$\wedge $
and
$\vee $
bind more strictly than
$\rightarrow $
, and, finally, implications associate to the right. Hence, for instance,
$\neg A\wedge B\rightarrow C\rightarrow D$
abbreviates
$((\neg A)\wedge B)\rightarrow (C\rightarrow D)$
.
In order to present the rules of the grounding calculus, we introduce the notion of converse formula. As detailed and philosophically motivated in [Reference Poggiolesi18], complete logical grounds are not constructed by directly negating formulae but by employing converse formulae instead.Footnote
2
Naturally, the converse
$A^{\bot }$
of the formula A is true when A is false. Here is the formal definition.
Notation. We denote by
$\neg ^{n}$
a sequence
$\neg \ldots \neg $
containing n consecutive occurrences of the symbol
$\neg $
. For instance
$\neg ^3 p $
will denote the formula
$\neg \neg \neg p $
.
Definition 2.1 (Converse Formula)
For any formula A, the converse
$A ^{\bot } $
of A is defined as follows:
-
• if
$A=\neg ^{2n}B$
where B does not begin with
$\neg $
, then
$A^{\bot } = \neg A $
-
• if
$A=\neg ^{2n+1}B$
where B does not begin with
$\neg $
, then
$A^{\bot } = \neg ^{2n}B$
Examples of pairs of converse formulae are
$\neg \neg P$
and
$\neg \neg \neg P $
,
$A \wedge B$
and
$\neg (A \wedge B)$
.
Now that we introduced the required notation, we can present the rules of the calculus and clarify their intended meaning. Table 1 contains the grounding rules of the calculus. We distinguish the application of these rules from the applications of other rules by a double inference line. Grounding rules of the forms 
, 
and 
express, respectively, that A is the ground of B, that C and D constitute the ground of E, and that F is the ground of H under the condition G. The vertical bar
$\mid $
appearing in the third kind of rule does not play any role in the construction of derivations: all premisses of any grounding rule must be derived before the rule can be applied. The meaning of the vertical bar exclusively concerns grounding. Indeed, the premiss that stands to the right of the vertical bar is not part of the ground of the formula occurring as conclusion of the rule, but constitutes a side condition required to be able to consider the premiss to the left of the bar as the complete ground of the conclusion.
Grounding rules of
$\mathrm {Gr}$
These grounding rules are intended as means for explaining true formulae according to a notion of logical grounding formalised in [Reference Poggiolesi18] and inspired by the requirements that Bernard Bolzano proposed for his notion of grounding—Abfolge in the original, German text [Reference Bolzano4]. According to this notion of grounding, a ground is supposed to be true, to completely account for the truth of the relative consequence, and to constitute the unique objective reason why the consequence holds—as extensively discussed for instance in [Reference Bolzano4, §203–§210]. Hence, technically, the ground will not only constitute a sufficient condition for the relative consequence, but also a necessary condition if we take into account what is true and what is false in the context under consideration. The role of the side conditions in grounding rules is precisely that of guaranteeing this. If we consider, for instance, the grounding rule 
for disjunction, the condition
$B^{\bot }$
has the role of guaranteeing that the ground A is the unique and complete reason why
$A\vee B$
is true. The truth of A alone, indeed, would certainly imply the truth of
$A\vee B$
; but, if we were not to specify that B is false by
$B^{\bot }$
, the fact that A is true would not necessarily be the only reason why
$A\vee B$
is true and, therefore, A would not be a necessary condition for the truth of
$A\vee B$
. This stress on the necessary character of the ground with respect to the truth of the conclusion is also the main difference between the notion of complete grounding and the well-established notion of full grounding [Reference Correia6, Reference Fine10, Reference Schnieder22]. Indeed, a full ground of a formula is not required to be also a necessary condition for the formula.
In Table 2, we present the logical rules for the connectives
$\bot , \neg , \wedge , \vee $
and
$ \rightarrow $
. We call, as usual, introduction rules those rules in the schema of which a certain logical constant—or group of logical constants—is displayed in the conclusion but not in the premisses, and elimination rules those rules in the schema of which a certain logical constant—or group of logical constants—is displayed in some premisses but not in the conclusion. Hence, Table 2 contains, in order, elimination rules for conjunction, disjunction and implication, negation introduction,
$\bot $
elimination, double negation elimination, and negation elimination.Footnote
3
Logical rules for
$\mathrm {Gr}$
The negation introduction rule is the only introduction rule in Table 2. While the idea behind the definition of the calculus
$\mathrm {Gr}$
is to replace logical introduction rules by grounding rules, this cannot be done for negation rules. Indeed, the restrictions on the grounding rules for negation make them wanting as logical introduction rules. An easy solution to this problem is to include in the calculus an unrestricted version of the grounding rules for negation: the traditional negation introduction rule. This solution is perfectly satisfactory from a logical perspective, but subtler solutions can be adopted if we wish to better understand the relation between grounding rules and logical rules, as shown in Section 3.
Definition 2.2 (Derivation)
A derivation in a calculus
$\mathrm {C}$
is built by starting from hypotheses and by applying the rules of the calculus
$\mathrm {C}$
, see [Reference Prawitz20] for details.
We assume, finally, that the calculus does not distinguish between ground-theoretically equivalent formulae, see [Reference Correia5, Reference Poggiolesi18]. Two formulae A and B are ground-theoretically equivalent if A can be obtained from B by applying the laws of commutativity and associativity, shown below, to some subformulae of B.Footnote 4
$$ \begin{align*} B \wedge A\;\leftrightarrow\; A\wedge B & \quad & (A \wedge B)\wedge C \;\leftrightarrow\; A \wedge (B\wedge C ) \\ B \vee A \;\leftrightarrow\; A\vee B & \quad & (A \vee B)\vee C \;\leftrightarrow\; A \vee (B\vee C ).\end{align*} $$
Notice that, while the calculus contains both grounding and logical rules, only the grounding rules are supposed to be explanatory. The logical rules are simply supposed to provide a background notion of logical reasoning—which we will show to be sufficient even if we do not include all traditional logical introduction rules—but not to comply with the requirements that we have on explanatory rules. Hence, the explanatory parts of the derivations constructed by employing the calculus will only be those obtained by grounding rule applications. The double inference line employed for grounding rules is precisely meant to provide an immediate visual indication of the explanatory parts of a derivation.
2.1 Classical soundness and completeness
We show now that, if we employ the grounding rules as introduction rules for the connectives of classical logic, then
$\mathrm {Gr}$
is also a calculus for classical logic. Technically, we will show that
$\mathrm {Gr}$
is sound and complete with respect to the standard natural deduction calculus
$\mathrm {NC}$
for classical logic, see [Reference Prawitz20], presented in Table 3. But first, we establish some simple lemmata which will enable us to work with the notation
$ A^{\bot }$
for the converse of a formula A without bothering about the internal structure of A.
The calculus
$\mathrm {NC}$
Lemma 2.1. For any formula A,
$A \vee A ^{\bot } $
is derivable in
$\mathrm {Gr}$
and in
$\mathrm {NC}$
.
Proof. If
$A = \neg ^{2n} B$
, then
$A^{\bot } = \neg A$
and
$(\neg A)^{\bot } = A$
. Thus, we can derive
$A \vee A ^{\bot } = A \vee \neg A $
in
$\mathrm {Gr}$
as follows:
If, on the other hand,
$A = \neg \neg ^{2n} B$
, then
$A^{\bot } = \neg ^{2n} B$
and
$A \vee A ^{\bot } = \neg \neg ^{2n} B \vee \neg ^{2n} B $
is of the form
$\neg C \vee C$
where
$ C^{\bot } = \neg C$
and
$(\neg C)^{\bot } = C$
. Thus, we can derive
$A \vee A ^{\bot } = \neg C \vee C$
in
$\mathrm {Gr}$
as follows:
As for
$\mathrm {NC}$
, we just have to notice that
$A \vee (A ^{\bot }) $
has either the form
$C \vee \neg C $
or
$\neg C \vee C$
, as argued above, and that both formulae are derivable in
$\mathrm {NC}$
.
We prove now that the formula A and its converse
$ A^{\bot } $
are always contradictory.
Lemma 2.2. For any A, 
is both a
$\mathrm {Gr}$
and an
$\mathrm {NC}$
derivation.
Proof. If
$A = \neg ^{2n} B$
, then
$A^{\bot } = \neg A$
and we have 
. If, on the other hand,
$A = \neg \neg ^{2n} B$
, then
$A^{\bot } = \neg ^{2n} B$
and we have 
.
We can finally prove that
$\mathrm {Gr}$
is sound and complete with respect to classical logic. In order to do so, we adopt the usual notation for derivability.
Definition 2.3 (Derivability)
For any calculus
$\mathrm {C}$
, set of formulae
$\Gamma $
, and expression E, the relation
$\Gamma \vdash _{\mathrm {C}}E$
holds if there is a derivation of E from hypotheses
$\Gamma $
constructed exclusively using rules of the calculus
$\mathrm {C}$
.
Theorem 2.3 (Soundness (
$\mathbf {CL}$
))
The calculus
$\mathrm {Gr}$
is classically sound.
Proof. We show that, for any
$\Gamma $
and F, if
$\Gamma \vdash _{\mathrm {Gr}}F$
then
$ \Gamma \vdash _{\mathrm {NC}}F$
. The proof is by induction on the number of rule applications in the
$\mathrm {Gr}$
derivation.
If no rule is applied in the
$\mathrm {NC}$
derivation of F,
$ \Gamma =\{ F \}$
and the statement trivially holds. Assume then that the
$\mathrm {Gr}$
derivation of F contains
$n>0$
rule applications and that if F has a
$\mathrm {Gr}$
derivation containing m rule applications, for
$m<n$
, then F has an
$\mathrm {NC}$
derivation. We consider the last rule applied in the
$\mathrm {Gr}$
derivation of F. We only discuss some non-trivial cases.
-
•
By I.H.,
$A ^{\bot }$
and
$ B^{\bot }$
are derivable in
$\mathrm {NC}$
. By Lemma 2.2, the following is an
$\mathrm {NC}$
derivation Therefore, the conclusion of the rule is derivable in
$\mathrm {NC}$
as well.
-
•
By inductive hypothesis (now on I.H.), A and
$ B^{\bot }$
are derivable in
$\mathrm {NC}$
. By Lemma 2.2, the following is an
$\mathrm {NC}$
derivation Therefore, the conclusion of the rule is derivable in
$\mathrm {NC}$
as well.
-
•
By I.H.,
$ \neg \neg A$
is derivable in
$\mathrm {NC}$
. By we can derive the conclusion in
$\mathrm {NC}$
.
By I.H., 
By inductive hypothesis (now on I.H.), A and 
By I.H., 
Theorem 2.4 (Completeness (
$\mathbf {CL}$
))
The calculus
$\mathrm {Gr}$
is classically complete.
Proof. We show, in particular, that, for any set of hypotheses
$\Gamma $
and formula F,
$\Gamma \vdash _{\mathrm {NC}}F$
then
$\Gamma \vdash _{\mathrm {Gr}}F$
. The proof is by induction on the number of rule applications in the
$\mathrm {NC}$
derivation of F. If no rule is applied in the
$\mathrm {NC}$
derivation, the statement trivially holds. Assume then that the
$\mathrm {NC}$
derivation of F contains
$n>0$
rule applications and that if a formula has an
$\mathrm {NC} $
derivation containing m rule applications, for
$m<n$
, then it has also a
$\mathrm {Gr}$
derivation. We consider the last rule applied in the
$\mathrm {NC}$
derivation. We only discuss some non-trivial cases.
By I.H., the premiss is derivable in 
By I.H., the premiss B is derivable in 
Corollary 1. The grounding calculus
$\mathrm {Gr}$
is classically sound and complete.
3 The specific difference between grounding and classical logic
As we have seen, grounding rules constitute a suitable basis for defining a complete set of rules for classical logic. Grounding rules are not the only introduction rules in
$\mathrm {Gr}$
though. This is due to the fact that grounding rules for negation do not enable us to derive the negation of a generic formula. And this is not surprising, because they are not supposed to do so. Since, for instance, no negation of an atomic formula will ever have a logical ground, grounding rules are defined with the precise intent of forbidding grounding derivations of formulae of this kind. This is the reason why
$\mathrm {Gr}$
also includes the traditional logical introduction rule for negation. By including this particular rule in
$\mathrm {Gr}$
, we obtain a complete calculus for classical logic. A question naturally arises though: can we be more precise about the difference between logical introduction rules and grounding rules? In other words, do we need to fully lift the restrictions on the grounding rules for negation or is there a way to define a complete calculus for classical logic that only contains grounding rules as introduction rules? This question can be positively answered, and the answer points at the specific conceptual difference between grounding rules and logical introduction rules. In order to answer this question, we define the calculus
$\mathrm {G_{CL}}$
, a variant of
$\mathrm {Gr}$
that only contains grounding and elimination rules, and the structural rule of classical dilemma. We show then that
$\mathrm {G_{CL}}$
is classically sound and complete by exploiting the fact that
$\mathrm {Gr}$
is.
Here is the formal definition of the grounding calculus
$\mathrm {G_{CL}}$
.
Definition 3.1 (Calculus
$\mathrm {G_{CL}}$
)
$\mathrm {G_{CL}}$
contains the rules in Table 4.
Rules of
$\mathrm {G_{CL}}$
Let us now comment on the choice of the new rules of
$\mathrm {G_{CL}}$
.
The ex falso quodlibet (efq) rule for negated atoms is needed because no formula can ground an atom or its negation. Indeed, the truth conditions of atoms and negated atoms are, so to speak, extra-logical. From a technical perspective, there is no way to derive
$\neg P$
by grounding rules without having
$\neg P$
itself among the hypotheses or inside some hypothesis. Notice, for instance, that even if we assume
$\bot $
as a hypothesis, we still cannot derive
$\neg P$
by using grounding rules.
Let us now move to the rule 
which we will call now on the classical dilemma (
$\mathrm {CD}$
) rule.Footnote
5
The technical role of this rule in
$\mathrm {G_{CL}}$
can be understood if we consider that the principle
$A\vee \neg A$
is used to simulate logical introduction rule applications by grounding rule applications. Suppose, for instance, that we have a derivation
$\delta $
of the formula A and we want to derive
$A\vee B$
. The logical introduction rule enables us to do it directly, but the grounding rule for disjunction does not. Nevertheless we can do it by applying the
$\mathrm {CD}$
rule to make a case distinction on B and
$\neg B$
, and then by applying the grounding rule in each one of the two cases:Footnote
6
The conceptual significance of the possibility of simulating logical introduction rules by grounding rules and the
$\mathrm {CD}$
rule will be discussed in Section 3.2.Footnote
7
In order to prove that
$\mathrm {G_{CL}}$
is sound with respect to classical logic, it is enough to show that the efq rule for negated atoms and the
$\mathrm {CD}$
rule are classically sound.
Theorem 3.1 (Soundness of
$\mathrm {G_{CL}}$
(
$\mathbf {CL}$
))
The calculus
$\mathrm {G_{CL}} $
is classically sound.
Proof. All rules of
$\mathrm {Gr}$
are classically sound, the efq rule for negated atoms is just a restriction of the usual efq rule, and the
$\mathrm {CD}$
rule can be simulated in
$\mathrm {NC} $
by a disjunction elimination on a formula of the form
$A \vee \neg A$
.
Since the only
$\mathrm {Gr}$
rule which is missing from
$\mathrm {G_{CL}} $
is negation introduction and since
$\mathrm {Gr}$
is classically complete, to prove that
$\mathrm {G_{CL}}$
is classically complete, it is enough to prove that negation introduction is unnecessary in
$\mathrm {G_{CL}}$
. Let us then establish some terminology and a lemma which will be essential for the proof.
Definition 3.2 (Formula Length)
The length of a formula F is the number of occurrences of connectives—including
$\bot $
—and propositional variables in F.
Lemma 3.2. For any formula
$B $
there is a
$\mathrm {G_{CL}} $
derivation
$\gamma $
of B from
$\bot $
.
Proof. If
$B=\bot $
, then
$\gamma =\bot $
. Hence, in the rest of the proof we suppose that
$B \neq \bot $
and we proceed by induction on the formula length l of B.
If
$l\leq 2$
, then we can derive B from
$\bot $
by the efq rule or by the efq rule for negated atoms. Suppose then that
$2<l$
. We reason by cases on the form of B.
-
•
$B = \neg C$
. We have four subcases.-
–
$B= \neg \neg D$
. By I.H., we can derive D from
$\bot $
without using negation introductions. We construct
$\gamma $
by applying the grounding rule for double negation to this derivation of D. -
–
$B= \neg (D\wedge E)$
By I.H., we have derivations of
$D^{\bot }$
and
$ E^{\bot }$
from
$\bot $
that do not contain negation introductions. Indeed, it is easy to see that the formula length of
$D^{\bot }$
is always smaller than the formula length of
$ \neg (D\wedge E)$
; as is the formula length of
$E^{\bot }$
. We construct
$\gamma $
by applying the grounding rule for negated conjunctions to these derivations of
$D^{\bot }$
and
$ E^{\bot }$
. -
–
$B= \neg (D\vee E)$
. By I.H., we have derivations of
$ D^{\bot }$
and
$ E^{\bot }$
from
$\bot $
that do not contain negation introductions. We construct
$\gamma $
by applying the grounding rule for negated disjunctions to these derivations of the converses of
$ D$
and
$ E$
. -
–
$B= \neg (D\rightarrow E)$
. By I.H., we have derivations of
$ D$
and
$ E^{\bot }$
from
$\bot $
without negation introductions. We construct
$\gamma $
by applying the grounding rule for negated implications to these derivations.
-
-
•
$B= C\wedge D$
. By I.H., we have derivations of C and D from
$\bot $
that do not contain negation introductions. We construct
$\gamma $
by applying the grounding rule for conjunction to these derivations. -
•
$B= C\vee D$
. By I.H., we have derivations of C and D from
$\bot $
that do not contain negation introductions. We construct
$\gamma $
by applying the grounding rule for disjunction to these derivations. -
•
$B= C\rightarrow D$
. By I.H., we have derivations of D and of
$C^{\bot }$
from
$\bot $
without negation introductions. We construct
$\gamma $
by applying the grounding rule for implication to these derivations.
Let us denote by
$\mathrm {G_{CL}} +\neg I$
the calculus obtained by extending
$\mathrm {G_{CL}}$
with the negation introduction rule. We now prove that all applications of the negation introduction rule can be eliminated from
$\mathrm {G_{CL}} +\neg I$
derivations.
Theorem 3.3. From any derivation in
$\mathrm {G_{CL}} +\neg I $
we can obtain one in
$\mathrm {G_{CL}}$
.
Proof. We associate to each
$\mathrm {G_{CL}} +\neg I $
derivation
$\delta $
a complexity
$(\mu , \nu )$
where
$\mu $
is the maximum among the lengths of the conclusions of negation introductions in
$\delta $
, and
$\nu $
is the number of negation introductions in
$\delta $
the conclusions of which have length
$\mu $
. The pairs
$(\mu , \nu )$
are ordered lexicographically.
The proof is by induction on the derivation complexity
$(\mu , \nu )$
. Consider any
$\mathrm {G_{CL}} +\neg I $
derivation
$\delta $
and suppose that the complexity of
$\delta $
is
$(\mu , \nu )$
. If either
$\mu \leq 1$
or
$\nu =0$
, then
$\delta $
is a
$\mathrm {G_{CL}}$
derivation and we are done. We suppose then that
$1 < \mu $
and
$0<\nu $
and we show that we can obtain a
$\mathrm {G_{CL}} +\neg I $
derivation
$\delta ' $
with complexity strictly smaller than
$(\mu , \nu )$
. Since
$1 < \mu $
and
$0<\nu $
, there is at least one negation introduction in
$\delta $
. We consider a negation introduction 
in
$\delta $
such that
$\neg A $
has length
$\mu $
and 
does not contain any negation introduction the conclusion of which has length
$\mu $
. We can always find such an application of negation introduction because it is enough to consider a topmost one among those the conclusion of which has length
$\mu $
. We reason then by cases on the form of A. We only present some exemplar cases.
-
• A is an atom P. Then
$\delta '$
is where
$1$
is an application of the
$\mathrm {CD}$
rule and r is an application of efq for negated atoms. Clearly
$\delta '$
has complexity
$(\mu ' , \nu ')$
where either
$\mu ' < \mu $
, if the negation introduction eliminated was the only one in
$\delta $
with conclusion of maximal length, or
$\mu ' = \mu $
and
$\nu ' < \nu $
, otherwise. In both cases
$(\mu ' , \nu ')$
is strictly smaller than
$(\mu , \nu )$
. -
•
$A= \neg B$
. Then
$\delta '$
is where
$1$
is an application of the
$\mathrm {CD}$
rule and
$\gamma $
is just an application of negation introduction if
$B=\neg C$
and a derivation of B from some occurrences of
$\bot $
constructed according to Lemma 3.2 otherwise.If
$\gamma $
is an application of negation introduction, its conclusion has length
$\rho < \mu $
and
$\delta '$
has complexity
$(\mu ' , \nu ')$
, which is, according to the argument also used in the previous case, strictly smaller than
$(\mu , \nu )$
.If
$\gamma $
is constructed according to Lemma 3.2, we have that the derivation might occur more than once in
$\delta '$
and that
$\delta ' $
might contain negation introductions. But since
$\alpha $
only contains negation introductions with conclusion of length strictly smaller than
$\mu $
, we can conclude also in this case that
$\delta '$
has complexity
$(\mu ' , \nu ')$
strictly smaller than
$(\mu , \nu )$
. -
•
$A= B\vee C$
. Then
$\delta $
is and
$\delta '$
is where
$2, 3$
and
$4$
are applications of the
$\mathrm {CD}$
rule;
$\gamma _1 , \gamma _2$
and
$\gamma _3 $
are derivations of
$\neg (B\vee C)$
from some occurrences of
$\bot $
constructed according to Lemma 3.2;
$\eta _1$
and
$\eta _2 $
consist of converse rule applications and, possibly, double negation rule applications—which are required to derive
$B^{\bot } $
and
$C^{\bot } $
if, respectively,
$\neg B $
is not the converse of B and
$\neg C$
is not the converse of C—;
$\beta $
is a derivation of
$\neg (B\vee C)$
by the grounding rule for negation and, possibly, double negation elimination rule applications—which are required to derive
$B^{\bot } $
and
$C^{\bot } $
if, respectively,
$\neg B $
is not the converse of B and
$\neg C$
is not the converse of C.Since by assumption
does not contain negation introductions with conclusion of length greater than or equal to
$\mu $
, and
$\gamma _ 1, \gamma _2 , \gamma _ 3 , \eta _1 , \eta _2 $
and
$\beta $
do not contain negation introductions, the complexity of
$\delta '$
is
$(\mu ' , \nu ')$
where either
$\mu ' < \mu $
, if the negation introduction eliminated was the only one in
$\delta $
with conclusion of maximal length, or
$\mu ' = \mu $
and
$\nu ' < \nu $
, otherwise. In both cases
$(\mu ' , \nu ')$
is strictly smaller than
$(\mu , \nu )$
.
where 
where 
might occur more than once in 
and 
where 
does not contain negation introductions with conclusion of length greater than or equal to 
We can finally prove that
$\mathrm {G_{CL}}$
is a calculus for classical logic.
Theorem 3.4. The calculus
$\mathrm {G_{CL}}$
is complete with respect to classical logic.
Proof. All
$\mathrm {Gr}$
derivations are derivations in the calculus
$\mathrm {G_{CL}} + \neg I $
defined by adding the negation elimination rule to
$\mathrm {G_{CL}}$
. Thus, by Theorem 2.4,
$\mathrm {G_{CL}} + \neg I $
is complete with respect to classical logic. But, by Theorem 3.3, the negation introduction rule is eliminable in
$\mathrm {G_{CL}}$
. Hence we can conclude that also
$\mathrm {G_{CL}}$
is complete with respect to classical logic.
3.1 Some minimal grounding systems
Let us present now two minimal grounding calculi that fully exploit the strength of the
$\mathrm {CD} $
rule and thus enable us to dispense with some or all logical elimination rules. These calculi will show once more that grounding rules behave just like logical introduction rules in that, along with the
$\mathrm {CD}$
rule, enable us to partly dispense with elimination rules. The first minimal calculus that we will introduce is
$\mathrm {G_{CL}} ' $
and is defined by removing all elimination rules from
$\mathrm {G_{CL}}$
and by adding the unrestricted efq rule.
Definition 3.3. The calculus
$\mathrm {G_{CL}} ' $
contains all grounding rules displayed in Table 1, the
$\mathrm {CD} $
rule, and the unrestricted efq rule.
In
$\mathrm {G_{CL}}'$
it is possible to prove all classical tautologies. This is easy to see, intuitively, since by nesting applications of the
$\mathrm {CD}$
rule on the subformulae of any formula, we can simulate all assignments considered in the truth table of that formula; if the formula is a tautology, grounding rules will then enable us to derive the formula in all branches above the topmost
$\mathrm {CD}$
applications, and thus to construct a proof of the formula. We prove this formally.
Theorem 3.5. For any theorem T of classical logic, it is possible to construct a derivation of T in
$\mathrm {G_{CL}}'$
without undischarged hypotheses.
Proof. Consider any truth table formalism such that one line of the truth table of a formula F corresponds to one truth assignment for the propositional variables occurring in F and such that a formula is a tautology if, and only if, its value is true on all lines of its truth table. Let us then consider any tautology F and let us construct a
$\mathrm {G_{CL}} '$
derivation of the form
such that
-
• each application of the
$\mathrm {CD}$
rule discharges a pair of hypotheses p and
$\neg p$
where p is a propositional variable occurring in F, -
• all
$\mathrm {CD}$
rule applications at the same distance from the conclusion of the derivation discharge the same hypotheses, -
• for each propositional variable p occurring in F, there is at least one
$\mathrm {CD} $
rule application that discharges the pair of hypotheses p and
$\neg p$
.
Notice, in particular, that above each premiss of any uppermost
$\mathrm {CD}$
application in our derivation, we can discharge either p or
$\neg p$
for each propositional variable occurring in F. Hence, we can associate the derivation of any of these premisses to one line of the truth table of F as follows. If above a certain premiss we can discharge the propositional variables
$p_1 , \ldots , p_n $
and the negated propositional variables
$\neg q_1, \ldots , \neg q_m $
, then the derivation above this premiss will be associated to the line of the truth table in which
$p_1 , \ldots , p_n $
have value true and
$ q_1, \ldots , q_m $
have value false.
Consider now a derivation
$\delta $
of a premiss of any uppermost
$\mathrm {CD}$
application in our proof. As we will formally prove later, the following is true:
$(\ast )\;\; $
For any subformula A of F, if A has value true in the truth table line associated to
$\delta $
, then we can derive A from the hypotheses that we can discharge in
$\delta $
; if A has value false in the truth table line associated to
$\delta $
, then we can derive both
$\neg A$
and
$A^{\bot }$
from the hypotheses that we can discharge in
$\delta $
.
Since F is a subformula of F and since F has value true on all lines of the truth table of F, this is enough to prove that we can derive F as premiss of any uppermost
$\mathrm {CD}$
application in our derivation by only using hypotheses discharged by
$\mathrm {CD}$
rule applications. And this means that we have a derivation of T without undischarged hypotheses,
We now prove
$(\ast )$
by induction on the form of the subformula A of F. If A is atomic, it is either a propositional variable p, and then we can derive it by employing the discharged assumption p or
$\neg p$
, or it is
$\bot $
, and then we can derive its negation by the following proof: 
Since the line of the truth table corresponding to
$\delta $
and the hypotheses that we can discharge in
$\delta $
agree by definition on all propositional variables, and since the value of
$\bot $
is false on all lines of any truth table, we have that
$(\ast )$
holds for A. Suppose now that A is not atomic and that
$(\ast )$
holds for all proper subformulae of A, we prove that
$(\ast )$
holds for A as well by reasoning on its outermost connective. We only present some exemplar cases.
-
•
$A=\neg B\quad $
If A has value true on the considered line of the truth table, then B must have value false. By I.H. on B, we can derive
$\neg B$
, which is exactly A. If A has value false on the considered line of the truth table, then B must have value true. By I.H., we can derive B and by applying the grounding rule for double negation we can derive also
$\neg \neg B = \neg A$
. Since
$A^{\bot } $
is either B or
$\neg \neg B$
, we have
$(\ast )$
. -
•
$A=B\vee C\quad $
If A has value true on the considered line of the truth table, then either B or C must have value true. By I.H. on B and C, we can derive B and C, or
$ B^{\bot }$
and
$ C$
, or
$ B$
and
$ C^{\bot }$
. In all three cases, by one of the grounding rules for disjunction, we can derive
$ B\vee C$
, which is exactly
$ A$
. If A has value false on the considered line of the truth table, then both B and C must have value false. By I.H. on B and C, we can derive both
$ B^{\bot }$
and
$ C^{\bot }$
. Then, by the grounding rule for negated disjunction, we can derive
$\neg ( B\vee C)$
as desired.
A second minimal system that we will present is obtained by removing conjunction, disjunction, implication and double negation elimination rules from
$\mathrm {G_{CL}}$
. In the resulting calculus, which we call
$\mathrm {G_{CL}} "$
, it is possible to directly simulate the elimination rules that we have removed—see [Reference D’Agostino, Gabbay and Modgil9] for a proof of a similar result. Let us define the calculus and show that its completeness can be easily proved by simulating all missing rules.
Definition 3.4. The calculus
$\mathrm {G_{CL}} " $
contains all grounding rules displayed in Table 1, the
$\mathrm {CD} $
rule, the unrestricted efq rule, and the negation elimination rule.
Theorem 3.6. All rules of
$\mathrm {G_{CL}}$
can be simulated in
$\mathrm {G_{CL}} "$
.
Proof. The statement is trivial for the grounding rules, the
$\mathrm {CD} $
rule, the efq rules for atoms and negated atoms, and for the negation elimination rule. We prove it for double negation, conjunction, disjunction and implication elimination:
-
•
can be simulated as follows: -
•
can be simulated as follows: where the converses of A and B might require an application of double negation elimination—which can be simulated as shown above—to be derived from
$\neg A $
and
$\neg B$
respectively.The symmetrical conjunction elimination can be simulated symmetrically.
-
•
can be simulated as follows: where the converses of A and B might require an application of double negation elimination—which can be simulated as shown above—to be derived from
$\neg A $
and
$\neg B$
respectively. -
•
can be simulated as follows: where the converse of B might require an application of double negation elimination—which can be simulated as shown above—to be derived from
$\neg B$
.
can be simulated as follows: 
can be simulated as follows: 
where the converses of A and B might require an application of double negation elimination—which can be simulated as shown above—to be derived from 
can be simulated as follows: 
where the converses of A and B might require an application of double negation elimination—which can be simulated as shown above—to be derived from 
can be simulated as follows: 
where the converse of B might require an application of double negation elimination—which can be simulated as shown above—to be derived from 
The existence of the calculi
$\mathrm {G_{CL}} ' $
and
$\mathrm {G_{CL}} "$
is certainly of interest. Indeed, they show that grounding rules, the
$\mathrm {CD}$
rule and a few rules for
$\bot $
are enough to recover the full strength of classical logic. Nevertheless, some caveats are in order. The calculus
$\mathrm {G_{CL}} ' $
does not fully characterise the consequence relation of classical logic:
$\mathrm {G_{CL}} ' $
does not enable us, indeed, to construct derivations from hypotheses, but only derivations without hypotheses for the theorems of the logic. In other terms,
$\mathrm {G_{CL}} '$
does not fare well as a deductive system—in the sense of a system that enable us to reason according to the logic—but only as a system for characterising the provability relation relative to the logic. On the other hand, while the calculus
$\mathrm {G_{CL}}"$
enables us to fully characterise the consequence relation of classical logic, it does so by rather convoluted derivations. In any case, the conceptual analysis of grounding rules that we will obtain, would not differ much if we considered one of these calculi instead of
$\mathrm {G_{CL}}$
. Indeed, the central element in the analysis that follow is the
$\mathrm {CD}$
rule. Therefore, we will focus on the full system
$\mathrm {G_{CL}}$
and we will show that it constitutes an ideal formal instrument for studying the specific difference between grounding rules and logical introduction rules. Let us dwell on this issue in the next section.
3.2 Why the excluded middle?
As we will see, the presence in
$\mathrm {G_{CL}}$
of one rule—the
$\mathrm {CD}$
rule—that precisely fills the gap between grounding and logical rules is the reason why this calculus enables us to exactly determine the difference between these two kinds of rules. In order to fully understand what this means, though, we must first consider how grounding rules are supposed to work.
Grounding rules are intended as means for explaining true formulae: they are supposed to display the reasons why their conclusion is true. While grounding rules can be employed to derive classical tautologies—as we have shown by the completeness results: Theorems 2.4 and 3.4—these rules are supposed to act on truths and, in particular, to conclude a true consequence given its true reasons. This is why grounding is described as factive.Footnote 8 Therefore, in a sense, grounding rules are supposed to be used only after we have fixed a particular truth assignment, or, in simpler terms, after we have established what is true and what is false.
This dependence of grounding rules on truth is even more evident if we consider the role of the premisses representing the side conditions of the ground. These premisses are indeed useless from a purely logical perspective, that is, they are useless if our only concern is the transmission of truth from the premisses to the conclusion. The ground conditions are, on the other hand, essential for grounding rules since a ground is supposed to completely account for the truth of its consequence, see [Reference Poggiolesi18] for the philosophical motivation behind this requirement. A grounding derivation is meant here to give us a full account of the status of its conclusion with respect to truth, to display the complete reason why its conclusion is true.Footnote
9
Our grounding rules for disjunction are exemplary in this sense, as already mentioned. For instance, the rule 
expresses that A is the complete reason why
$A\vee B$
is true, also considering that B is false, as made explicit by the right premiss of the rule. Thus the condition
$B^{\bot }$
does not contribute in any way to make the conclusion
$A\vee B$
true, but it is required to provide a full account of the truth of all the parts of
$A\vee B$
. The fact that a grounding derivation is required to constitute a full account of the truth of its conclusion explains why grounding rules presuppose the knowledge of what is true and what is false—and not only for the formulae that matter, but also for those that do not really affect the truth of the conclusion but are nevertheless part of it.
We finally have all the elements to understand the conceptual reason why the
$\mathrm {CD}$
rule alone enables us to use grounding rules as logical introduction rules: the
$\mathrm {CD}$
rule is a logical instrument to reason by cases in a hypothetical way on the truth and falsity of formulae. This enables us to simulate in a purely abstract way the choice of a truth assignment. Therefore, when we need to apply a grounding rule and we only possess the information required by a logical introduction rule to introduce a connective, we can use the
$\mathrm {CD}$
rule to make an exhaustive case distinction and show that, in any case, the grounding rule is enough to introduce the connective. Let us consider a simple example in order to discuss this conceptual point in more concrete terms. Consider, for simplicity, the formula
$A\vee P$
where P is atomic. If we use the logical introduction rule for disjunction, it is enough to have a derivation
$\delta $
of A to conclude
$A\vee P$
: 
Indeed, if A is true, then also
$A\vee P$
is true, and this is all that matters as far as logical rules are concerned. If we use the grounding rules for disjunction, on the other hand, we also need information on P. It does not matter whether P is true or false, but we nevertheless need a premiss to witness its truth value, because the grounding rule requires a full account of the truth of all parts of its conclusion. Since we are reasoning at the level of pure logic and we do not know whether P is true or false, we use the
$\mathrm {CD}$
rule and make a case distinction on the truth of P, as shown by the
$\mathrm {CD}$
rule application
$1$
in the derivation below. In each of the two cases, we use the grounding rule for disjunction to conclude
$A\vee P$
as follows: 
. By employing the
$\mathrm {CD}$
rule in this way, on the one hand, we simulate the choice of truth assignments and thus comply with the requirements of grounding rules; on the other hand, we do not actually fix a truth assignment and therefore keep the reasoning on a level of full logical generality. In conclusion, it is due to the possibility of reasoning hypothetically on truth and falsity, provided by the
$\mathrm {CD}$
rule, if we can use grounding rules as logical introduction rules.
Informational analyticity
A system that presents strong technical similarities with
$\mathrm {G_{CL}}$
has been studied in [Reference d’Agostino7, Reference D’Agostino8]. In this system, the only rule that enables the discharge of hypotheses is the
$\mathrm {CD}$
rule. Moreover, there is a striking similarity between the introduction rules of this system and the grounding rules of
$\mathrm {G_{CL}}$
if we forget about the premisses corresponding to ground conditions in the latter rules. These analogies between
$\mathrm {G_{CL}}$
and the system in [Reference d’Agostino7, Reference D’Agostino8] do not seem to be merely technical. Let us dwell on the issue. Conceptually, the calculus discussed in [Reference d’Agostino7, Reference D’Agostino8] has been introduced in order to capture a distinction between informationally analytic inference rules and inference rules that require hypothetical reasoning on virtual information. The characterising feature of an informationally analytic rule is that the information that the conclusion of the rule is true is completely contained in the information that its premisses are true. To the contrary, the validity of a rule that requires hypothetical reasoning on virtual information appeals to information which is not directly carried by the premisses of the rule. The
$\mathrm {CD}$
rule is a typical example of a rule of the latter kind since its validity essentially relies on hypothetical reasoning about the truth of formulae and background information concerning the underlying notion of truth. A conceptual connection between the system in [Reference d’Agostino7, Reference D’Agostino8] and
$\mathrm {G_{CL}}$
seems actually to exist then. Indeed, the premisses of a grounding rule are supposed to carry all the existing information in virtue of which its conclusion is true. The information that these premisses are true is therefore supposed to contain the information that the conclusion is true. It could be argued therefore that grounding rules are informationally analytic rules in nature. A complete equivalence between the two kinds of rules clearly does not hold though, because grounding rules must comply with further requirements which are irrelevant with respect to the notion of informational analyticity. Finally, the role of the
$\mathrm {CD}$
rule in
$\mathrm {G_{CL}}$
, as we have just argued, is precisely that of introducing the possibility of reasoning about virtual information, which is not provided by grounding rules due to their factivity.
4 Grounding rules and intuitionistic introduction rules
We have just shown that classical logic can be characterised by adding the
$\mathrm {CD}$
rule to a calculus only containing grounding rules as introduction rules. Since classical logic can be also characterised by adding the law of excluded middle—for instance in the form of the
$\mathrm {CD}$
rule—to intuitionistic logic, the identification of grounding rules and intuitionistic introduction rules seems possible. A potential connection between grounding and intuitionistic, or constructive, reasoning is moreover hinted at by the idea—already discussed in Section 1—that classical reductio ad absurdum, the use of which is not allowed in intuitionistic proofs, should not occur inside grounding derivations either. Let us formally investigate, then, the connection between grounding rules and intuitionistic introduction rules.
The most evident lack of grounding rules with respect to intuitionistic introduction rules concerns the rules for implication. The logical completeness of grounding rules for implication clearly relies on the classical translation of
$A\rightarrow B $
as
$\neg A\vee B$
; and while the implication rules based on this translation are intuitionistically sound, they are not intuitionistically complete. Indeed, they only capture the most basic cases in which an implication is intuitionistically true—that is, when the consequent is true and when the antecedent is false. In intuitionistic logic, though, an implication can be true also for another reason. If we consider the semantics of intuitionistic implication according to the BHK interpretation, see [Reference Troelstra25], we have that
$A\rightarrow B $
is true if we can transform any proof of A into a proof of B. Clearly this is possible whenever A is false—the condition is trivially met since we will never be provided with a proof of A—and whenever B is true—in this case, our transformation can simply discard the proof of A and directly present the proof of B which we must already have according to the BHK interpretation if we know that B is true. But it is still possible for
$A\rightarrow B $
to be true even if A is not false and we have no proof of B. This third case is not captured by any grounding rule but is captured by the traditional implication introduction rule. The latter rule, indeed, enables us to reason in a hypothetical way from the assumed truth of A: if we can derive B under the hypothetical assumption that A is true, then we can conclude
$A\rightarrow B$
. As we have argued in Section 3.2 though, grounding rules are not supposed to enable us to reason in a hypothetical way about truth, and indeed they do not. To recover the full strength of
$\mathbf {IL}$
then, we need to add a rule to do so. If we moreover wish to study the distinction between grounding rules and intuitionistic introduction rules, the additional rule should not be an introduction rule and should exclusively capture what grounding rules are missing. Let us try to define such a rule.
It is important to remark that in defining this new rule—and the other ones that will be required—we neither simply aim at a simulation of intuitionistic introduction rules by also using grounding rules, nor we aim at the definition of a new notion of grounding complying with the main tenets of complete grounding but based on an intuitionistic notion of truth. The first objective could be easily achieved by the classical calculi presented above, and is not of much interest. Indeed, simulating intuitionistic derivability by classical derivability is, in general, easily done. The second objective, on the other hand, would require a redefinition of the adopted grounding notion and thus of the grounding rules themselves. And while defining such a notion of intuitionistic grounding would constitute a result of great interest, the methods and systems developed here do not seem to directly enable us to do so. Such an endeavour must hence be left for future work. The actual objective of the rest of the present work is to define a calculus which is both sound and complete with respect to intuitionistic logic, and in which grounding rules play an essential role. Only after having defined such a calculus we could hope for a deeper and more formal understanding of the specific difference between intuitionistic introduction rules and grounding rules.
From a proof-theoretical perspective, grounding rules for implication are missing the possibility of discharging hypotheses. According to our rules, in a ground we can only use proven formulae or formulae which we have independently supposed to be true and that we will, perhaps, discharge by other rule applications. Let us then try a technical solution and define a rule that exclusively enables us to discharge hypotheses and such that its use in combination with the grounding rules for implication enables us to prove the truth of an implication in all cases which are relevant for
$\mathbf {IL}$
. Such a rule is the leftmost shown below, and it is sound with respect to
$\mathbf {IL}$
since we can simulate it by the central derivation below. This rule is moreover complete with respect to implication introduction, since for each topmost implication introduction, we can simulate it in the grounding calculus extended with our new rule by the derivation below on the right and then proceed to simulate the other topmost implication introductions until only grounding rules are used to introduce implications in the whole proof.
Let us dwell on the meaning of this rule. Even though, at first glance, the rule seems the result of a proof-theoretical trick to admit the possibility of discharging hypotheses when introducing an implication, a closer inspection enables us to understand its logical meaning. Indeed, the rule directly corresponds to the logical principle
$(A\rightarrow A \rightarrow B)\rightarrow A \rightarrow B$
, because, if we have a proof of
$A\rightarrow B $
from the hypothesis A, it enables us to obtain a proof of
$A\rightarrow B$
; or, in other terms, if we have a proof of
$A\rightarrow A \rightarrow B$
, then we can obtain a proof of
$A\rightarrow B$
. By noticing that
$A\rightarrow A \rightarrow B$
is equivalent to
$A\wedge A \rightarrow B$
, we can easily see that the rule corresponds to the logical principle of left contraction.Footnote
10
Contraction is not enforced by grounding rules since the addition of redundant information to the ground is not admissible, as is clear if we consider the formal definition of the grounding relation presented in [Reference Poggiolesi18] which we follow here.
Since the discrepancies between grounding rules and logical rules for implication can be solved by employing a structural principle such as left contraction. Let us direct our attention towards other structural principles as well. Let us begin with the weakening principle, and in particular with left weakening.Footnote
11
This principle is implied by the a fortiori principle:
$B\rightarrow A\rightarrow B $
, which we can derive in our grounding calculus by additionally employing the rule that we have just defined:
Nothing more is required as far as left weakening is concerned. Exactly the same way of reasoning can be employed for negation, since we can treat—and actually even define—
$\neg A$
as the formula
$A\rightarrow \bot $
. Hence we also introduce the rule 
.
Let us then consider right weakening:
$(A\rightarrow B)\rightarrow A \rightarrow B\vee C $
.Footnote
12
This weakening principle is not a legitimate grounding principle either: even if we have a derivation of A, we cannot ground
$A\vee B$
without specifying whether B is true or false. Adding the rule 
which corresponds to full right weakening would clearly solve the problem, but seems a rather radical overcompensation. Indeed, this rule is the traditional disjunction introduction rule and grounding rules for introducing disjunctions already exist, they are simply more demanding than traditional disjunction introduction rules. An ideal solution would then consist in finding some logical principles which are intuitionistically valid and exactly fill the gap between grounding rules for disjunction and logical introduction rules for disjunction. Let us then consider the right weakening principles that are already valid with respect to our grounding rules for disjunctions:
$$\begin{align*}( A\rightarrow B) \rightarrow A\rightarrow C^{\bot} \rightarrow B\vee C\qquad (\mathrm{GW1}),\end{align*}$$
$$\begin{align*}( A\rightarrow B) \rightarrow A\rightarrow C \rightarrow B\vee C\qquad (\mathrm{GW2}).\end{align*}$$
These are clearly weaker than full right weakening because, in order to enable us to conclude
$B\vee C$
, also require us to specify whether C is true or false. In order to obtain full right weakening, we would also need the principles
$(A\rightarrow C^{\bot } \rightarrow B\vee C)\rightarrow A \rightarrow B\vee C $
and
$ ( A\rightarrow C \rightarrow B\vee C) \rightarrow A \rightarrow B\vee C $
, which, used in combination with
$\mathrm {GW1}$
and
$\mathrm {GW2}$
by transitivity of implication, enable us to derive full right weakening:
$(A\rightarrow B) \rightarrow A\rightarrow B\vee C$
. Unfortunately, these two implications are too general and, even though the first one is valid in
$\mathbf {CL}$
, neither of them is derivable by grounding rules or valid in
$\mathbf {IL}$
.Footnote
13
Nevertheless, we can restrict their form by following the intuition that A is simply supposed to be the hypothesis from which we can derive
$B\vee C$
regardless of the truth of C. This restriction yields the following implications:
$(B\rightarrow C^{\bot } \rightarrow B\vee C)\rightarrow B \rightarrow B\vee C $
and
$ ( B\rightarrow C \rightarrow B\vee C) \rightarrow B \rightarrow B\vee C$
, where instead of supposing that from A we can derive
$B\vee C$
, we directly pick the instance of A that enables us to do so without knowing whether C is true or false, that is, the formula B itself. The latter implications are clearly valid in
$\mathbf {IL}$
since
$B\rightarrow B\vee C$
is. From these two formulae, we can then obtain the following two rules: 
and 
, and add them to the grounding calculus to recover the full strength of
$\mathbf {IL}$
.
Let us dwell for a moment on the proof-theoretical nature of the four rules that we have just defined. These rules, indeed, are certainly of a peculiar kind: while particular connectives are displayed in their schemata, the only premiss appearing in each of them is simply identical to the relative conclusion. Since these rules directly correspond to axioms that express structural principles of the logic—that is, left weakening, left contraction, and right weakening—it seems reasonable to consider them structural rules. And the display of specific connectives in the rule schemata should not lead us to conclude that these rules are not structural, because also the
$\mathrm {CD}$
rule is often considered as a structural rule even though negation plays an essential role in its schematic presentation. Moreover, the four rules above are clearly not operational logical rules,Footnote
14
in the sense that they neither introduce nor eliminate any connective.
The fact that additional rules—such as our four new rules—are required to define a complete calculus for intuitionistic logic based on grounding rules is a formal confirmation that grounding rules are wanting with respect to the intended meaning of intuitionistic connectives. As mentioned above, these rules precisely enable us to cover all possible cases envisaged by the BHK interpretation for the truth of intuitionistic connectives. While a single rule enforcing the adoption of a classical notion of truth—that is, the
$\mathrm {CD}$
rule—was enough to do this with respect to the connectives of classical logic, a technically subtler solution that addresses the problems of each connective separately is required here. The dependence of the solution on the specific connectives is only apparent though, because, as we have just shown, the additional rules required by the solution actually correspond to very general structural principles. Let us then define the calculus
$\mathrm {G_{IL}}$
for
$\mathbf {IL}$
that only contains grounding rules as introduction rules.
Definition 4.1 (Calculus
$\mathrm {G_{IL}}$
)
$\mathrm {G_{IL}}$
contains all rules in Table 5.
Rules of
$\mathrm {G_{IL}}$
Before proving that
$\mathrm {G_{IL}}$
is sound and complete with respect to
$\mathbf {IL}$
, let us formally define the intuitionistic calculus that we will use for reference.
Definition 4.2 (Calculus
$\mathrm {NI}$
)
The natural deduction calculus
$\mathrm {NI}$
for
$\mathbf {IL}$
contains all rules in Table 3 except the classical rule 
.
Theorem 4.1 (Soundness (
$\mathbf {IL}$
))
The calculus
$\mathrm {G_{IL}}$
is intuitionistically sound.
Proof. We show, in particular, that, for any set of hypotheses
$\Gamma $
and formula F, if
$\Gamma \vdash _{ \mathrm {G_{IL}}}F$
then
$ \Gamma \vdash _{\mathrm {NI}}F$
. The proof is by induction on the number of rule applications in the
$ \mathrm {G_{IL}}$
derivation of F. If no rule is applied in the
$ \mathrm {G_{IL}}$
derivation,
$ \Gamma =\{ F \}$
and the statement trivially holds. Assume then that the
$ \mathrm {G_{IL}}$
derivation contains
$n>0$
rule applications and that if we have a
$ \mathrm {G_{IL}}$
derivation containing m rule applications, for
$m<n$
, then we also have an equivalent
$\mathrm {NI}$
derivation. We consider the last rule applied in the
$ \mathrm {G_{IL}}$
derivation of F. We only present some of the non-trivial cases.
-
•
By I.H.,
$A^{\bot }$
is derivable in
$\mathrm {NI}$
. Since
$\mathrm {NI}$
and
$\mathrm {NC}$
contain the same negation elimination rule, by Lemma 2.2, the following is an
$\mathrm {NI}$
derivation of the conclusion of the rule: -
•
By I.H.,
$A^{\bot }$
and
$B^{\bot }$
are derivable in
$\mathrm {NI}$
. Since
$\mathrm {NI}$
and
$\mathrm {NC}$
contain the same negation elimination rule, by Lem. 2.2, the following is an
$\mathrm {NI}$
derivation of the conclusion of the rule: -
•
By I.H., A and
$B^{\bot }$
are derivable in
$\mathrm {NI}$
. Since
$\mathrm {NI}$
and
$\mathrm {NC}$
contain the same negation elimination rule, by Lem. 2.2, the following is an
$\mathrm {NI}$
derivation of the conclusion of the rule:
By I.H., 
By I.H., 
By I.H., A and 
Theorem 4.2 (Completeness (
$\mathbf {IL}$
))
$ \mathrm {G_{IL}}$
is intuitionistically complete.
Proof. We show, in particular, that, for any set of hypotheses
$\Gamma $
and formula F,
$\Gamma \vdash _{\mathrm {NI}}F$
then
$\Gamma \vdash _{ \mathrm {G_{IL}}}F$
. The proof is by induction on the number of rule applications in the
$\mathrm {NI}$
derivation of F. If no rule is applied in the
$\mathrm {NI}$
derivation of F, the statement trivially holds. Assume then that the
$\mathrm {NI}$
derivation of F contains
$n>0$
rule applications and that if a formula has an
$\mathrm {NI} $
derivation containing m rule applications, for
$m<n$
, then it has also an
$ \mathrm {G_{IL}}$
derivation. We consider the last rule applied in the
$\mathrm {NI}$
derivation of F. We only present some non-trivial cases that we have not already discussed.
-
•
By I.H., the premiss is derivable in
$ \mathrm {G_{IL}}$
. We arbitrarily choose between one of the
$\mathrm {G_{IL}}$
derivations and . -
•
By I.H.,
$\bot $
is derivable in
$ \mathrm {G_{IL}}$
from A. Hence is a
$\mathrm {G_{IL}}$
derivation.
By I.H., the premiss is derivable in 
and 
.
By I.H., 
is a 
We have thus shown that, in order to define a calculus for
$\mathbf {IL}$
by only employing grounding rules as introduction rules, it is necessary to also include additional rules. The specific rules that we used here in order to do so enable us to recover precisely the structural principles of left contraction, left weakening and right weakening. These rules also show us then that grounding rules do not enforce all structural principles that hold with respect to intuitionistic reasoning. Therefore, we can conclude that grounding rules are not equivalent to intuitionistic introduction rules. Moreover, we have provided an independent confirmation of the thesis defended in [Reference Genco and Poggiolesi12] that grounding is based on a derivability relation which is essentially substructural. Substructural logics, indeed, are defined by proof-theoretical systems in which the use of the structural rules of contraction and weakening is either forbidden or strongly limited.
5 Conclusions
In the present work, we investigated the relationship between logical grounding rules and traditional logical rules. First of all, we showed that logical grounding rules constitute a complete set of introduction rules for classical and intuitionistic logic; secondly, we showed that logical grounding rules are not identical to logical rules because, due to their very nature of explanatory rules, they lack the abstractness of logical introduction rules. In particular we showed that if we want to use grounding rules as logical introduction rules, we need to employ logical principles or rules that enable us to reason about truth in a hypothetical way. We moreover argued that this result connects grounding rules and the notion of informational analyticity discussed in [Reference d’Agostino7, Reference D’Agostino8]. The grounding calculus introduced to conduct the analysis strongly confirms the thesis that grounding derivations are logical derivations of a particular kind without trivialising the distinction between grounding and logical rules. Finally, we showed that grounding rules are essentially different from intuitionistic logical rules as well, since the former do not enforce the structural inferential principles which are required to derive all theorems of intuitionistic logic.
While the present work exclusively focuses on grounding rules for connectives, introduction and elimination rules for a grounding operator can be defined as well. A study concerning the properties of these rules and their interaction with grounding rules would constitute a natural and essential extension of the presented analysis. Since, moreover, grounding is a typical example of a hyper-intensional notion, an analysis focusing on the connection between the proof-theoretical features of grounding rules and their hyper-intensional nature would certainly be of great interest both for proof-theory and for the study of grounding.
Acknowledgements
We thank the anonymous referees for their insightful comments and suggestions, which have been instrumental in improving this article. We also thank Francesca Poggiolesi very much for several extremely useful discussions on the presented work.
Funding
Funded by the IBS project (ANR-18-CE27-0012-01) and by theBRIO project (PRIN scheme project no. 2020SSKZ7R).
would be simulated by a derivation of the form 
where 
and 
are grounding rules, then 
is a grounding rule, then 
.
.
.
