1.1 The Canonical Notion of Grounding

Let me start with what I will dub the canonical notion of grounding. This is the notion that has been most studied and used by philosophers and logicians in the past dozen years.

The notion is often expressed by means of predicates of facts, as in the following sentence type:

1. (1) The fact that $q$ , the fact that $r$ , $\dots$ ground the fact that $p$

Alternatively, one may express the notion using sentential operators as in:

1. (2) $p$ because $q$ , $r$ , $\dots$

2. (3) Its being the case that $q$ , that $r$ , $\dots$ make it the case that $p$

One also encounters hybrid expressions, partly operational and partly predicational, such as:

1. (4) $p$ in virtue of the fact that $q$ , the fact that $r$ , $\dots$

These modes of expression are, of course, far from being equivalent from the point of view of logical grammar. Only if grounding is expressed by means of a predicate as in (1) can it be properly said to be a relation. However, for ease of expression it is often convenient to speak as if grounding were a relation even on the assumption that it is expressed by means of a sentential operator or a hybrid expression. I will feel free to do that in what follows.

The canonical notion of grounding has the following three features: it is (i) (one or many)-to-one, (ii) factive and (iii) metaphysical. In order to spell this out, let me first adopt the predicational mode of formulation.

To say that a notion of grounding is (one or many)-to-one is to say that grounding of the corresponding sort is always of one particular fact, and that when a fact is grounded, it may be grounded in one fact, or in several facts taken together without being grounded in each of these facts taken individually. This aspect of the canonical notion is made syntactically explicit in (1) by having a list of fact-terms on the left of the predicate – which may contain only one element – and a single fact-term on the right. The view that there are (one or many)-to-one relations is far from being heretical: causation and (the intuitive notion of) logical consequence are arguably of that kind.

To say that a notion of grounding is factive is to say that grounding of the corresponding sort relates facts. This aspect of the canonical notion is also made explicit in (1) by the choice of the terms that flank the predicate. Facts, in this context, may be understood as obtaining states of affairs, or alternatively as true propositions.

There are two main ways of cashing out the idea that the canonical notion of grounding is metaphysical. One is to say that it is metaphysical insofar as it entails metaphysical necessitation – that is, insofar as the following conditional holdsFootnote ¹:

(Nec)

If some facts $G$ , $H$ , $\dots$ ground a fact $F$ in the canonical sense, then as a matter of metaphysical necessity, if $G$ , $H$ , $\dots$ all obtain, then $F$ also obtains.

Despite its popularity, this principle has been criticized (see Leuenberger Reference Leuenberger2014 and Skiles Reference Skiles2015). The other main way of cashing out the idea is in terms of comparative fundamentality. On that account, the canonical notion is metaphysical insofar as the following holdsFootnote ²:

(Fund)

If some facts $G$ , $H$ , $\dots$ ground a fact $F$ in the canonical sense, then each of $G$ , $H$ , $\dots$ is more fundamental than $F$ .

Fundamentality here is of course to be understood as metaphysical fundamentality, as opposed to, say, epistemic fundamentality.Footnote ³ Note that these two ways of cashing out the metaphysical character of grounding may be orthogonal: it does not seem to be incoherent to hold that some notions of grounding satisfy (Nec) but not (Fund) and that some notions of grounding (leaving aside ‘partial’ notions, see below) satisfy (Fund) but not (Nec). I propose a disjunctive account of metaphysicality: for a notion of grounding to be metaphysical is for it to satisfy (Nec) or (Fund) or both.

Importantly, the fact that the canonical notion of grounding is metaphysical does not preclude there being cases of grounding in the canonical sense that are ‘logical’ or ‘conceptual’. Compare (5) and (6) below with (7)–(10):

1. (5) Mental facts are grounded in physical facts

2. (6) The existence of a whole is grounded in the existence of its parts

3. (7) The fact that it is both raining and cold is grounded in the fact that it is raining and the fact that it is cold

4. (8) The fact that 2 + 2 = 4 or 1 = 0 is grounded in the fact that 2 + 2 = 4

5. (9) The fact that John is a bachelor is grounded in the fact that he is an adult, the fact that he is a male and the fact that he is not married

6. (10) The fact that the sky is coloured is grounded in the fact that it is blue

(5)–(10) are all typical claims involving the canonical notion. In all these cases, what grounds plausibly metaphysically necessitates what is groun-ded. But in (7)–(10) the link between the grounds and the groundees is not merely one of metaphysical necessitation: it is arguably one of conceptual necessitation; and in the case of (7) and (8) it is also arguably one of logical necessitation.

I have spelled out the three features of the canonical notion of ground-ing – being (one or many)-to-one, being factive and being metaphysical – on the assumption that the notion is expressed by means of a predicate as in (1) above. Assuming instead that the canonical notion is expressed by means of a sentential operator – say, ‘because’ – only requires a few adjustments. The canonical notion is (one or many)-to-one insofar as the basic claims involving it are of the form (2), where what is on the right-hand side of ‘because’ may comprise one or more items. The notion is factive insofar as for all $p$ , $q$ , $r$ , $\dots$ , if $p$ because $q$ , $r$ , $\dots$ , then $p$ , $q$ , $r$ , $\dots$ . The notion is metaphysical insofar as it satisfies at least one of the following two conditions:

(Nec ${}^{*}$ )

For all $p$ , $q$ , $r$ , $\dots$ , if $p$ because $q$ , $r$ , $\dots$ , then as a matter of metaphysical necessity, if $q$ , $r$ , $\dots$ , then $p$

(Fund ${}^{*}$ )

For all $p$ , $q$ , $r$ , $\dots$ , if $p$ because $q$ , $r$ , $\dots$ , then its being the case that $q$ is more fundamental than its being the case that $p$ , its being the case that $r$ is more fundamental than its being the case that $p$ , $\dots$

It should be clear how the three features are to be spelled out on the assumption that the canonical notion of grounding is expressed by means of a hybrid expression.

A further feature of the canonical notion of grounding is that it is explanatory. Two quite different ways of cashing this out have been put forward in the literature: there is on one hand the view that grounding is a form of explanation; and there is on the other hand the view that grounding is not a form of explanation but is rather, like causation, a determinative notion that backs explanations (see Raven Reference Raven2015 for a discussion and relevant references). On both views, the type of explanation involved is taken to be distinctively metaphysical (on metaphysical explanation, see Brenner et al. Reference Brenner, Maurin, Skiles, Stenwall, Thompson and Zalta2021).

On the assumption that the canonical notion of grounding is explanatory, one may argue that it is both relevant and non-monotonic. Assuming that the notion is expressed by means of a predicate (here as in many other places throughout this Element, I will leave the other modes of expression aside for the sake of brevity), these features can be glossed as follows: the notion is relevant in the sense that when some facts ground a further fact, each of the former facts is relevant to the obtaining of the grounded fact; and it is non-monotonic in the sense that from the hypothesis that a fact $F$ is grounded in some facts $G$ , $H$ , $\dots$ , one cannot validly infer that $F$ is grounded in $G$ , $H$ , $\dots$ together with other arbitrary facts. (Note that non-monotonicity arguably follows from relevance.) In both respects, the canonical notion of grounding differs from classical logical consequence. Relevance and non-monotonicity are features that are often attributed to the canonical notion of grounding, often independently from their connection with explanatoriness.

1.2 Other Notions

The other notions of grounding that have been discussed or simply mentioned in the literature depart from the canonical notion in one or more features of the latter. Let me run through the relevant features in turn, starting with some features that have been discussed in the previous section:

Being (one or many)-to-one.

Some authors have taken seriously the idea that there can be cases of ‘zero-grounding’, that is, (speaking in the predicational mode) cases of metaphysical strict full grounding where the ground is the empty collection of facts rather than a collection of one or more facts (see for instance Fine Reference Fine, Correia and Schneider2012a and Litland Reference Litland2017). And some authors have argued that there can be cases where a plurality of facts is metaphysically strictly fully grounded which cannot be reduced to cases in which the members of the plurality are individually grounded (see for instance Dasgupta Reference Dasgupta2014 and Litland Reference Litland2016).

Being factive.

Several authors countenance notions of grounding that are not factive (see for instance Correia Reference Correia2014, Reference Correia2017; Fine Reference Fine, Correia and Schneider2012a and Litland Reference Litland2017).

Being metaphysical.

The literature on grounding features, alongside metaphysical grounding, notions of grounding of other kinds, like logical grounding, conceptual grounding, natural grounding or again normative grounding (see for instance Correia Reference Correia2005, Reference Correia2014 and Fine Reference Fine, Correia and Schneider2012a).

In addition to having the features mentioned in the previous section, the canonical notion is both full and strict (the vocabulary of ‘full’ versus ‘partial’ and ‘strict’ versus ‘weak’ is from Fine Reference Fine, Correia and Schneider2012a). The canonical notion is full insofar as the grounds, in the canonical sense, of a fact are sufficient for the fact to obtain. And it is strict insofar as it is, strictly speaking, a notion of ‘making the case’ or ‘obtaining in virtue of’. Fine (Reference Fine, Correia and Schneider2012a) ties the notion of strictness with that of irreflexivity or non-circularity: he takes it that no fact can strictly ground, or even help strictly ground, itself. This may be true; but if it is, it is a substantial, non-analytic truth.Footnote ⁴ Other notions of grounding discussed in the literature lack one or both of these features:

Being full.

Fine (Reference Fine, Correia and Schneider2012a) introduces notions of grounding that are partial, that is, not full. Here is the definition of one of them: $G$ partially grounds $F$ iff ${}_{\text{df}}F$ is grounded in the canonical sense in $G$ , or in $G$ together with other facts. (Note that even though the notion just defined is not full, given the definition every full ground, in the canonical sense of ‘ground’, is a partial ground.)

Being strict.

Fine (Reference Fine, Correia and Schneider2012a) also introduces notions of grounding that are weak, that is, not strict. They are all reflexive. One can easily define such a notion in terms of the canonical notion: $G$ , $H$ , $\dots$ weakly ground $F$ iff ${}_{\text{df}}$ either $G$ , $H$ , $\dots$ ground in the canonical sense $F$ , or $F$ is one of $G$ , $H$ , $\dots$ . (I hasten to stress that Fine Reference Fine, Correia and Schneider2012a does not propose such a definition.)

The five dimensions of departure from features of the canonical notion that have been discussed so far are prima facie independent from one another. Even if this first impression is incorrect, there are certainly sufficiently many independencies among these dimensions to already generate an impressive number of different notions of grounding – not all of which have been explicitly discussed or even just mentioned in the literature.

Let me close this section with a further distinction that adds even more to this variety. This is the distinction between immediate and mediate grounding (Fine Reference Fine, Correia and Schneider2012a). Fine illustrates the distinction as follows: the fact that $q\wedge r$ is immediately grounded in the fact that $q$ and the fact that $r$ (taken together), he claims, whereas the fact that $p\wedge (q\wedge r)$ is only mediately grounded in the fact that $p$ , the fact that $q$ and the fact that $r$ (taken together). The canonical notion of grounding is certainly not an immediate notion. Fine holds that it should be identified with a mediate notion. In fact, he intends his example to feature the canonical notion and the corresponding immediate notion. Fine’s view that the canonical notion should be identified with a mediate notion is a substantial view, at least if it is granted, as it seems reasonable to hold, that a mediate notion must be definable in terms of chains of a corresponding immediate notion (I will come back to this at the end of Section 2.3).

2.1 Fine’s ‘The Pure Logic of Ground’

Fine’s pure logic of grounding has four primitive operators:

• $⩽$ expresses weak full grounding

• $\preccurlyeq$ expresses weak partial grounding

• $<$ expresses strict full grounding

• $\prec$ expresses strict partial grounding

The language in which the logic is formulated has a given non-empty set of basic sentences which, from the point of view of the language, are simple, and the sequents of the language are all the expressions of the following types, where $\Delta$ is a (possibly empty) set of basic sentences and $\varphi$ and $\psi$ are basic sentences:

1. (1) $\Delta ⩽\varphi$

2. (2) $\varphi \preccurlyeq \psi$

3. (3) $\Delta <\varphi$

4. (4) $\varphi \prec \psi$

For the sake of homogeneity, it would be better to have either (2) and (4) of the form $\left\{\varphi \right\}\preccurlyeq \psi$ and $\left\{\varphi \right\}\prec \psi$ , respectively, or alternatively to take $\Delta$ in (1) and (3) to be a plurality of sentences, as long as one allows empty pluralities and pluralities comprising only one item – but I will leave this detail aside.

Fine takes his ground-theoretic notions to be factive. But nothing in the logic he puts forward forces this interpretation of these notions, and it turns out that interpreting these notions as being non-factive is the most natural option.Footnote ⁵ Similarly, the ground-theoretic notions discussed in Sections 2.1 to 2.4 are all most naturally understood as being non-factive.

Fine does not say whether his notions are metaphysical (as opposed to, say, normative or natural), and so we may assume that the logic is intended to be neutral on the question. If $<$ is interpreted as expressing a metaphysical notion, $\Delta <\varphi$ with $\Delta$ non-empty can be interpreted as the claim that the members of $\Delta$ ground, in the canonical sense, $\varphi$ .

On Fine’s view, the four notions are intimately connected. Indeed, as this will be reflected in the logic, Fine takes $⩽$ to be the basic grounding relation in terms of which the other three notions are defined. Assuming that the language is suitably enriched, the definitions could be formulated as follows:

• $\varphi \preccurlyeq \psi :=\exists \Delta (\varphi \in \Delta \wedge \Delta ⩽\psi )$

• $\varphi \prec \psi :=\varphi \preccurlyeq \psi \wedge \neg (\psi \preccurlyeq \varphi )$

• $\Delta <\varphi :=\Delta ⩽\varphi \wedge \neg \exists \psi (\psi \in \Delta \wedge \varphi \preccurlyeq \psi )$

Fine discusses another notion of partial grounding, partial strict grounding, which he symbolizes as ${\prec }^{*}$ and which can be defined as follows:

• $\varphi {\prec }^{*}\psi :=\exists \Delta (\varphi \in \Delta \wedge \Delta <\psi )$

Importantly, partial strict grounding is not strict partial grounding (in Fine’s logic, it can be shown that the former entails the latter and that the converse entailment fails), and Fine’s pure logic of grounding features the latter notion, not the former.

Fine’s system for the pure logic of grounding, PLG, is based on a list of rules of inference, where each rule says (or is to be interpreted as saying) that from a collection of 0 or more sequents (possibly infinitely many), one can infer a given sequent. The rules are listed in Figure 1.Footnote ⁶ Despite appearances, Non-Circularity ( $\prec$ ) does not involve a special sequent $\perp$ : the rule is meant to say that from any sequent of type $\varphi \prec \varphi$ , any sequent can be inferred.

Figure 1 Rules for PLG

$\frac{\Delta <\varphi }{\Delta ⩽\varphi }\frac{\varphi \prec \psi }{\varphi \preccurlyeq \psi }\frac{\Delta ,\varphi <\psi }{\varphi \prec \psi }\frac{\Delta ,\varphi ⩽\psi }{\varphi \preccurlyeq \psi }$	Subsumption
$\frac{{\Delta }_1⩽{\varphi }_1{\Delta }_2⩽{\varphi }_2\dots {\varphi }_1,{\varphi }_2,\dots ⩽\varphi }{{\Delta }_1,{\Delta }_2,\dots ⩽\varphi }$	Cut ( $⩽$ )
$\frac{\varphi \preccurlyeq \psi \psi \preccurlyeq \chi }{\varphi \preccurlyeq \chi }\frac{\varphi \preccurlyeq \psi \psi \prec \chi }{\varphi \prec \chi }\frac{\varphi \prec \psi \psi \preccurlyeq \chi }{\varphi \prec \chi }$	Transitivity
$\frac{ }{\varphi ⩽\varphi }\frac{\varphi \prec \varphi }{\perp }$	Identity, Non-Circularity ( $\prec$ )
$\frac{{\varphi }_1,{\varphi }_2,\dots ⩽\varphi {\varphi }_1\prec \varphi {\varphi }_2\prec \varphi \dots }{{\varphi }_1,{\varphi }_2,\dots <\varphi }$	Reverse Subsumption

A sequent $\sigma$ is said to be derivable from a set $\Sigma$ of sequents in PLG iff $\sigma$ can be obtained from $\Sigma$ by means of the rules. Note that since PLG has some rules – namely, Cut ( $⩽$ ) and Reverse Subsumption – that allow for infinitely many premisses, derivability cannot be formally defined in the familiar way in terms of finite sequences of items. But this can nevertheless be done in terms of sequences by saying that $\sigma$ is derivable from $\Sigma$ in PLG iff there is a (finite or infinite) sequence with a last member such that (i) $\sigma$ is the sequence’s last member, and (ii) each member of the sequence is either a sequent in $\Sigma$ , or an identity sequent $\varphi ⩽\varphi$ , or a sequent obtained from previous sequents by means of some rule distinct from Identity.Footnote ⁷ This is the way Fine goes. Another, somewhat more natural option invokes the notion of a labelled tree as defined in the Appendix: say that $\sigma$ is derivable from $\Sigma$ in PLG iff there is a tree with no infinite branch, labelled by sequents, such that (i) $\sigma$ is the tree’s bottom, (ii) the tree’s top contains only members of $\Sigma$ or sequents of type $\varphi ⩽\varphi$ , and (iii) for every parent node $n$ of the tree, there is (an instance of) a rule of inference distinct from Identity whose conclusion labels $n$ and whose premisses are the labels of $n$ ’s children.

A derived rule of the system is a rule of the same format as the previous rules whose conclusion is derivable from its premisses in PLG. PLG has the following noteworthy derived rules:

$\frac{{\Delta }_1⩽\varphi {\Delta }_2⩽\varphi \dots }{{\Delta }_1,{\Delta }_2,\dots ⩽\varphi }\text{Amalgamation}(⩽)$

$\frac{{\Delta }_1<{\varphi }_1{\Delta }_2<{\varphi }_2\dots {\varphi }_1,{\varphi }_2,\dots ,\Gamma <\psi }{{\Delta }_1,{\Delta }_2,\dots ,\Gamma <\psi }\text{Cut}(<)$

$\frac{\Delta ,\varphi <\varphi }{\perp }\text{Non-Circularity}(<)$

$\frac{{\Delta }_1<\varphi {\Delta }_2<\varphi \dots }{{\Delta }_1,{\Delta }_2,\dots <\varphi }\text{Amalgamation}(<)$

Note the formal difference between Cut ( $<$ ) and Cut ( $⩽$ ): one gets Cut ( $⩽$ ) from Cut ( $<$ ) by substituting $⩽$ for $<$ and taking $\Gamma =\varnothing$ . I will call the condition on $<$ expressed by Cut ( $<$ ) strong cut and the condition on $⩽$ expressed by Cut ( $⩽$ ) weak cut. It is easy to see that granted that $⩽$ satisfies weak cut and that Identity holds, $⩽$ also satisfies strong cut.

On the semantic side, the logic is characterized within Fine’s general truthmaker semantical framework.Footnote ⁸ The framework’s core semantic notion is that of truthmaking or exact verification. A truthmaker or exact verifier for a statement is wholly relevant to the truth of the statement. Fine contrasts exact verification with inexact verification and with loose verification – which Fine takes to be the notion standardly used in possible worlds semantics. An inexact verifier for a statement must be at least partly relevant to the truth of the statement, whereas a loose verifier for a statement is simply something that necessitates the truth of the statement and hence does not even need to be relevant to the truth of that statement. Trivially, any exact verifier is an inexact verifier. The view, upheld by Fine, that every inexact verifier is a loose verifier is plausible but substantial. To illustrate the three notions of verification, consider the state of my being both sitting and nervous. It exactly verifies the statement ‘Fabrice is sitting and Fabrice is nervous’, and it inexactly verifies ‘Fabrice is sitting’ without exactly verifying it. The same state loosely verifies the statement ‘2 + 2 = 4’, but it fails to inexactly, and hence to exactly, verify it.

For the purpose of semantically characterizing PLG, Fine introduces what he calls ‘generalized fact models’, but which – in order to stick to the terminology he has come to adopt since then – I will call ‘generalized state models’.

Let a state frame be a tuple $⟨S,\prod ⟩$ such thatFootnote ⁹, Footnote ¹⁰:

• $S$ (states) is a non-empty set;

• $\prod$ (fusion) is an operation taking each subset of $S$ into a member of $S$ , such that (i) for any $s\in S$ , $\prod \left\{s\right\}=s$ and (ii) for any family $(S_i{)}_{i\in I}$ of subsets of $S$ , $\prod \{\prod S_i:i\in I\}=\prod \bigcup _{i\in I}{S}_i$ .

Instead of writing $\prod \{s_1,s_2,\dots \}$ we may simply write $s_1{s}_2\dots$ to improve readability. Say that a set of states $T$ in a state frame $⟨S,\prod ⟩$ is closed under $\prod$ iff for any non-empty subset $T^{*}$ of $T$ , $\prod T^{*}\in T$ . The facts of a state frame are the non-empty sets of states of that state frame that are closed under its fusion operation.Footnote ¹¹ A generalized state frame is a tuple $⟨S,\prod ,V⟩$ , where $⟨S,\prod ⟩$ is a state frame and $V$ (verification space) is a non-empty set of facts of $⟨S,\prod ⟩$ . Finally, a generalized state model is defined as a tuple $⟨S,\prod ,V,\left[\right]⟩$ where $⟨S,\prod ,V⟩$ is a generalized state frame and $\left[\right]$ (verification valuation) is a function which takes each basic sentence of the language into a member of $V$ .

The fusion operation of a state frame is informally to be understood as conjunctive in nature, for example, as taking the state of my being sitting and the state of my being nervous into the state of my being both sitting and nervous. The verification space of a generalized state frame is thought of as the set of all the facts $F$ of the underlying state frame such that $F$ is capable of being the ‘semantic value’ of a statement, that is, the set of all the exact verifiers of a statement. Finally, where $\varphi$ is a basic sentence and $\left[\right]$ the verification valuation of a generalized state model, $\left[\varphi \right]$  – $\varphi$ ’s verification-set – is accordingly thought of as the set of all the states that exactly verify $\varphi$ .

In order to interpret the sequents by means of generalized state models, it is useful to introduce a fusion operation on sets of states in addition to the fusion operation on states. Where $F$ is a state frame or a generalized state frame with fusion operation $\prod$ , let me use ${⨅}_F$ for the corresponding fusion operation on $F$ ’s sets of states (when no confusion threatens, I will feel free to omit the subscript). For any sets of states $S_1$ and $S_2$ of the frame, ${⨅}_F\{S_1,S_2\}$ is the set of all $s_1{s}_2$ with $s_1\in S_1$ and $s_2\in S_2$ . We may generalize this idea to any set of sets of states by appealing to choice functions. Where $S$ is a non-empty set of sets, a choice function on $S$ is any function $f$ that takes each $s\in S$ into an element of $s$ . A selection from a non-empty set of sets $S$ is the image of some choice function on $S$  – that is, a set $T$ is a selection from $S$ iff $T=\left\{f\right(s):s\in S\}$ for some choice function $f$ on $S$ . (Note that in case $S$ contains $\varnothing$ , there is no choice function on $S$ , and therefore no selection from $S$ either.) The formal definition of ${⨅}_F$ goes as follows:

• For $S$ a non-empty set of sets of states, ${⨅}_{F}S{=}_{\text{df}}\{\prod T:T\text{ a selection from }S\}$ ;

• ${⨅}_F\varnothing {=}_{\text{df}}\{\prod \varnothing \}$ .

An alternative but equivalent way of defining ${⨅}_F$ in the non-degenerate cases, which some may find more perspicuous, defines it as operating on indexed families of sets of states rather than on sets of sets of states, as follows:

• For any non-empty family $(S_i{)}_{i\in I}$ of sets of states, ${⨅}_F\left(S_i{)}_{i\in I}{=}_{\text{df}}\right\{\prod (s_i{)}_{i\in I}:(s_i{)}_{i\in I}\text{ is a family of states such that }{s}_i\in S_i\text{ for all }i\in I\}$ .

One can verify that if $S$ is a non-empty set of facts, then ${⨅}_{F}S$ is itself a fact (and that if $(S_i{)}_{i\in I}$ is a non-empty family of facts, then ${⨅}_F(S_i{)}_{i\in I}$ is itself a fact).

Given any generalized state frame $F$ with underlying verification space $V$ , four ground-theoretic relations are defined, the first two between sets of members of $V$ and members of $V$ , and the other ones between members of $V$ and members of $V$ (here I use $⨅$ instead of ${⨅}_F$ ):

• $F{⩽}_{F}F$ (read: $F$ is a weak full ground for $F$ in $F$ ) iff ${}_{\text{df}}⨅F\subseteq F$ ;

• $G{\preccurlyeq }_{F}F$ (read: $G$ is a weak partial ground for $F$ in $F$ ) iff ${}_{\text{df}}$ for some $F\subseteq V$ such that $G\in F$ , $F{⩽}_{F}F$ ;

• $F{<}_{F}F$ (read: $F$ is a strict full ground for $F$ in $F$ ) iff ${}_{\text{df}}F{⩽}_{F}F$ and for no $G\in F$ does $F{\preccurlyeq }_{F}G$ ;

• $G{\prec }_{F}F$ (read: $G$ is a strict partial ground for $F$ in $F$ ) iff ${}_{\text{df}}G{\preccurlyeq }_{F}F$ but not $F{\preccurlyeq }_{F}G$ .

Let $M$ be a generalized state model with underlying generalized state frame $F$ and verification valuation $\left[\right]$ . Let $\left[\Delta \right]$ be $\left\{\right[\varphi ]:\varphi \in \Delta \}$ . The relations just defined allow one to define a notion of ‘holding in $M$ ’ for each type of sequent of the language in the obvious way:

• $\Delta ⩽\varphi$ holds in $M$ iff $\left[\Delta \right]{⩽}_F\left[\varphi \right]$

• $\varphi \preccurlyeq \psi$ holds in $M$ iff $\left[\varphi \right]{\preccurlyeq }_F\left[\psi \right]$

• $\Delta <\varphi$ holds in $M$ iff $\left[\Delta \right]{<}_F\left[\varphi \right]$

• $\varphi \prec \psi$ holds in $M$ iff $\left[\varphi \right]{\prec }_F\left[\psi \right]$

A sequent $\sigma$ is then said to be a PLG-consequence of a set of sequents $\Sigma$ iff there is no generalized state model in which all the members of $\Sigma$ hold and $\sigma$ fails to hold. Fine’s (Reference Fine2012b) main result is that consequence so defined and derivability in PLG coincide:

In the same paper, Fine also examines systems formulated in languages poorer than the language of PLG, that is, in languages which comprise less than the four types of sequents defined above. Of particular interest are two systems involving only one type of sequent, a system PLWFG for the pure logic of weak full grounding and a system PLSFG for the pure logic of strict full grounding. They are presented in the same format as PLG but with their own sets of rules – see Figures 2 and 3.

Figure 2 Rules for PLWFG

$\frac{{\Delta }_1⩽{\varphi }_1{\Delta }_2⩽{\varphi }_2\dots {\varphi }_1,{\varphi }_2,\dots ⩽\varphi }{{\Delta }_1,{\Delta }_2,\dots ⩽\varphi }$	Cut ( $⩽$ )
$\frac{ }{\varphi ⩽\varphi }$	Identity

Figure 3 Rules for PLSFG

$\frac{{\Delta }_1<{\varphi }_1{\Delta }_2<{\varphi }_2\dots {\varphi }_1,{\varphi }_2,\dots ,\Gamma <\psi }{{\Delta }_1,{\Delta }_2,\dots ,\Gamma <\psi }$	Cut ( $<$ )
$\frac{\Delta ,\varphi <\varphi }{\perp }$	Non-Circularity ( $<$ )
$\frac{{\Delta }_1<\varphi {\Delta }_2<\varphi \dots }{{\Delta }_1,{\Delta }_2,\dots <\varphi }$	Amalgamation ( $<$ )

Fine establishes that both PLWFG and PLSFG are fragments of PLG (or, to use another standard terminology, that PLG is a conservative extension of both PLWFG and PLSFG), in the following sense:

The semantics for PLG can of course be used almost as it is to interpret the language of PLWFG and that of PLSFG: one simply has to remove the semantic clauses for the sequents that are not in the relevant language. We thus have a notion of PLWFG-consequence and one of PLWFG-consequence, and the previous theorem together with the soundness and completeness theorem for PLG allows one to establish without effort the following:

Fine’s approach to the pure logic of grounding has been criticized in a number of ways. Some criticisms question the properties that PLG attributes to strict full grounding. The three rules for PLSFG, or consequences thereof, have indeed been subject to objections: it has been argued that strict full grounding is not irreflexive (see Correia Reference Correia2014 and Woods Reference Woods2018),Footnote ¹² from which it follows that Non-Circularity ( $<$ ) fails; it has been argued that partial strict ground (the relation defined on page 8 and symbolized by ${\prec }^{*}$ , not the relation symbolized by $\prec$ ) is not transitive (see Schaffer Reference Schaffer, Correia and Schnieder2012), from which it follows that Cut ( $<$ ) fails; and the validity of Amalgamation ( $<$ ) has been questioned (see deRosset Reference deRosset2015, Litland Reference Litland, Bliss and Priest2018a and Litland Reference Litland2018b). These objections are important and would therefore deserve extensive discussion, but for lack of space I will leave them aside.Footnote ¹³

Let me elaborate a bit on a further objection to Fine’s approach, which will give me the opportunity to emphasize an important aspect of Fine’s truthmaker framework. Fine’s pure logic of grounding features the notion of weak full grounding. Moreover, as I announced at the beginning of this section, Fine’s logic reflects the view that weak full grounding is the basic grounding relation in terms of which the other three grounding relations are defined, in the manner I mentioned there. This last point is absolutely clear from the semantics. But what is weak full grounding? deRosset (Reference deRosset2013a, Reference deRosset2014) has argued that what Fine (Reference Fine, Correia and Schneider2012a, Reference Fine2012b) says by way of clarifying the notion is insufficient or even problematic.

I agree with deRosset on some of the objections he makes, but for the sake of the line of argumentation I am pursuing here let me just mention one particular objection which I take to be ineffective. One suggestion for making sense of weak full grounding is to take the proposed truthmaker semantics seriously, that is, as providing genuine truth-conditions for ground-theoretic claims in addition to providing a mathematically handy way of characterizing links of logical consequence between such claims. Taking the semantics seriously means holding that for any interpreted language of the sort under consideration here, there is a privileged generalized state model $M$ (an ‘intended model’) such that a sequent of the language – in particular, a sequent with $⩽$ as ground-theoretic operator – is true tout court iff it is true relative to $M$ . deRosset denies that this suggestion allows one to correctly interpret $⩽$ . His argument goes essentially as follows:

As the reader may already know or will grant after reading Section 3, there are various ways in which one may justify the claim that $\varphi ⩽\psi$ is not true. Let us just take the claim for granted. What is wrong in deRosset’s argument is the claim that relative to the intended model $M$ , $\varphi$ and $\psi$ have exactly the same exact verifiers. On Fine’s approach, the verifiers of a sentence are states; states may or may not obtain; and a sentence is true just in case at least one of its verifiers obtains. This distinction between obtaining and non-obtaining (or ‘actual’ and ‘non-actual’) states and the connection between truth and obtainment are absent from Fine Reference Fine, Correia and Schneider2012a and Fine Reference Fine2012b, but are made explicit in later work on the truthmaker framework (e.g., in Fine Reference Fine, Hale, Wright and Miller2017a). Now relative to $M$ , $\varphi$ and $\psi$ have the same obtaining exact verifiers, but their exact verifiers tout court are distinct: for instance, the (non-obtaining) state of Sam’s being happy is an exact verifier for $\varphi$ but not for $\psi$ . Hence, by the semantics’ own lights, $\varphi ⩽\psi$ is false – as desired.

2.2 deRosset’s ‘On Weak Ground’

As I have just emphasized, deRosset is dissatisfied with Fine’s treatment of the pure logic of grounding because it invokes the notion of weak full grounding, a notion which he finds obscure. In deRosset (Reference deRosset2014), he presents a logic which features only a notion of strict full grounding ( $<$ ) (deRosset has plausibly in mind the canonical notion) and the companion notion of partial strict grounding ( ${\prec }^{*}$ ).Footnote ¹⁴ His system for the ‘logic of strict grounding’ (LSG), as he calls it, is defined by the rules listed in Figure 4.

Figure 4 Rules for LSG

$\frac{\Delta ,\varphi <\psi }{\varphi {\prec }^{*}\psi }$	Subsumption ( $</{\prec }^{*}$ )
$\frac{\varphi {\prec }^{*}\psi \psi {\prec }^{*}\chi }{\varphi {\prec }^{*}\chi }$	Transitivity ( ${\prec }^{*}$ )
$\frac{\varphi {\prec }^{*}\varphi }{\perp }$	Non-Circularity ( ${\prec }^{*}$ )
$\frac{{\Delta }_1<{\varphi }_1{\Delta }_2<{\varphi }_2\dots {\varphi }_1,{\varphi }_2,\dots ,\Gamma <\psi }{{\Delta }_1,{\Delta }_2,\dots ,\Gamma <\psi }$	Cut ( $<$ )
$\frac{{\Delta }_1<\varphi {\Delta }_2<\varphi \dots }{{\Delta }_1,{\Delta }_2,\dots <\varphi }$	Amalgamation ( $<$ )

By the definition of ${\prec }^{*}$ in terms of $<$ given on page 8, Subsumption ( $</{\prec }^{*}$ ) directly follows, Transitivity ( ${\prec }^{*}$ ) follows from Cut ( $<$ ), and Non-Circularity ( ${\prec }^{*}$ ) follows from Non-Circularity ( $<$ ). Non-Circularity ( $<$ ), Cut ( $<$ ) and Amalgamation ( $<$ ) define Fine’s system PLSFG which, as we saw, is a fragment of his PLG. Since Non-Circularity ( $<$ ) follows from Non-Circularity ( ${\prec }^{*}$ ) and Subsumption ( $</{\prec }^{*}$ ), PLSFG is also a fragment of LSG.

On the semantic side, deRosset follows Fine: he invokes generalized state models, interprets the sequents of the language of LSG using these models, and define consequence for this language – LSG-consequence – in the same way as described above. He interprets sequents of type $\Delta <\varphi$ in the same way as Fine does, and sequents of type $\varphi {\prec }^{*}\psi$ in the way Fine interprets sequents of type $\varphi \prec \psi$ . (This is important to emphasize since, once again, ${\prec }^{*}$ and $\prec$ express distinct notions.) deRosset then establishes that LSG is sound and complete relative to the proposed semantics:

The way he proceeds, in effect, is as follows.Footnote ¹⁵ Let LSG ${}^{-}$ be the system defined exactly like LSG except that every occurrence of a sequent of type $\varphi {\prec }^{*}\psi$ is replaced by the sequent $\varphi \prec \psi$ , and define LSG ${}^{-}$ -consequence simply as PLG-consequence on the language of LSG ${}^{-}$ . deRosset establishes that LSG ${}^{-}$ is a fragment of PLG:

Given the definition of LSG ${}^{-}$ -consequence, it immediately follows that LSG ${}^{-}$ is sound and complete relative to the proposed semantics for LSG ${}^{-}$ :

Now the difference between LSG and LSG ${}^{-}$ is merely notational – the only difference is that LSG has the symbol ${\prec }^{*}$ where LSG ${}^{-}$ has the symbol $\prec$ . Therefore, from the soundness and completeness result for LSG ${}^{-}$ one can infer the soundness and completeness result for LSG.

Theorem 4 certainly has some value from a formal point of view – soundness + completeness results, in general, are indeed formally valuable. But it is not philosophically satisfactory, at least when evaluated against deRosset’s initial motivation for introducing LSG – namely, to put it briefly, to get rid of weak grounding. Given its intended interpretation, the proof system is all about the familiar notion of strict full grounding and partial strict grounding, weak grounding is completely out of the picture. So far so good. But semantically, weak full grounding still plays the central role: the truth-clauses for $<$ are the same as in the semantics for PLG, the truth-clauses for ${\prec }^{*}$ are those for $\prec$ in the semantics for PLG, and the latter are ultimately formulated in terms of the semantic embodiment of weak full grounding. In a later paper (deRosset Reference deRosset2015), however, he proposes an alternative semantics where weak full grounding plays no role at all. This is the topic of the next section.

2.3 deRosset’s ‘Better Semantics for the Pure Logic of Ground’

deRosset (Reference deRosset2015) cashes out the intuitive content of his alternative semantics in terms of the notion of immediate (or unmediated, as he sometimes puts it) grounding. He defines a corresponding notion of mediate grounding in terms of chains of immediate links, and he identifies the canonical notion of grounding with that mediate notion (following, in effect, Fine Reference Fine, Correia and Schneider2012a – see the end of Section 1.2). The semantics he proposes is then ‘homophonic’: a sequent of type $\Delta <\varphi$ is taken to hold just in case the facts expressed by the members of $\Delta$ ground, in the canonical sense, the fact expressed by $\varphi$ (and likewise for sequents of type $\varphi {\prec }^{*}\psi$ ).

Let me go through the semantics in a more precise way. The basic structures invoked by deRosset are so-called hypergraphs.Footnote ¹⁶ Each hypergraph generates a set of labelled trees (modulo replacement of nodes by other nodes), and each such labelled tree is taken to represent a link of strict full grounding. I here follow the spirit but not the letter of deRosset’s semantics: I directly start off with labelled trees (the detour via hypergraphs strikes me as unnecessary).

The labelled trees that are invoked are those defined in the Appendix (the various tree-theoretic notions that I use below are all defined there). For present purposes, I call them grounding trees and I call the labels of a grounding tree its facts. Let me adopt the following definitions:

• Let $T$ be a grounding tree and $(T_i{)}_{i\in I}$ a family of grounding trees. $T$ can be extended with $(T_i{)}_{i\in I}$ iff ${}_{\text{df}}$ there is a non-empty family $(l_i{)}_{i\in I}$ of leaves of $T$ such that for each $i\in I$ , $l_i$ is occupied by the same fact as $T_i$ ’s root.

• Let $T$ be a grounding tree and $(T_i{)}_{i\in I}$ a family of grounding trees such that the former can be extended with the latter. A grounding tree $U$ extends $T$ with $(T_i{)}_{i\in I}$ iff ${}_{\text{df}}$ there is an initial subtree $U^{*}$ of $U$ and an isomorphism $f$ from $T$ to $U^{*}$ such that for any $i\in I$ , the final subtree of $U$ whose root is $f\left(l_i\right)$ is isomorphic to $T_i$ .

In Figure 5, $U$ extends $T$ with $T_1$ and $T_2$ (the notation $X/x$ indicates that fact $X$ occupies node $x$ ).

Figure 5 Extension of a tree

A grounding frame is defined as a set $T$ of grounding trees that satisfy the following closure condition:

As the reader may anticipate, this condition will guarantee that Cut ( $<$ ) is validated. Two further conditions on grounding frames, that of being acyclic and that of being additive, play a central role in the semantics, where these conditions are defined as follows:

• A grounding frame is acyclic iff ${}_{\text{df}}$ none of its grounding trees has a fact that appears twice on one of its branches.

• A grounding frame is additive iff ${}_{\text{df}}$ for every fact $F$ and family of non-empty sets of facts $(F_i{)}_{i\in I}$ such that for each $i\in I$ , the frame contains a grounding tree with top $F$ and bottom $F_i$ , the frame also contains a grounding tree with top $F$ and bottom $\bigcup _{i\in I}{F}_i$ .

As the reader has certainly anticipated, imposing the first condition will secure Non-Circularity ( $<$ ), and imposing the second condition will secure Amalgamation ( $<$ ).

Where $T$ is a grounding frame, define the relation ${<}_T$ between sets of facts in $T$ (where a fact in $T$ is a fact of some grounding tree in $T$ ) and facts in $T$ , and the binary relation ${\prec }_T^{*}$ between facts in $T$ , as follows:

• $F{<}_{T}F$ iff ${}_{\text{df}}$ there is a grounding tree $T$ in $T$ such that (i) $F$ = $T$ ’s top and (ii) $F$ = $T$ ’s bottom;

• $G{\prec }_T^{*}F$ iff ${}_{\text{df}}$ for some set of facts $F$ in $T$ such that $G\in F$ , $F{<}_{T}F$ .

The language deRosset focuses on is the same as in his 2014 paper: the sequents are those constructed with $<$ and ${\prec }^{*}$ .Footnote ¹⁷ A grounding model for that language is a pair $⟨T,\left[\right]⟩$ , where $T$ is a grounding frame and $\left[\right]$ (interpretation) is a function taking each basic sentence of the language into a fact of some tree in $T$ . A grounding model is said to be acyclic / additive iff the underlying grounding frame is acyclic / additive. The notion of holding in a grounding model $M$ with underlying grounding frame $T$ and interpretation function $\left[\right]$ is then naturally defined as follows:

• $\Delta <\varphi$ holds in $M$ iff $\left[\Delta \right]{<}_F\left[\varphi \right]$

• $\psi {\prec }^{*}\varphi$ holds in $M$ iff $\left[\psi \right]{\prec }_F^{*}\left[\varphi \right]$

deRosset characterizes four systems using this semantics. One of them is LSG as previously axiomatized (see page 17). The other three are subsystems of LSG, obtained by removing rules from its charaterization: B (the ‘base logic’) is the system defined by Cut ( $<$ ), Subsumption ( $</{\prec }^{*}$ ) and Transitivity ( ${\prec }^{*}$ ) only, system BNC is defined by adding Non-Circularity ( ${\prec }^{*}$ ) and system BA by adding Amalgamation ( $<$ ) instead. Without much surprise, the characterization results he establishes are as follows:

As I emphasized at the outset, deRosset advertises his semantics as being based on the idea that every link of grounding in the canonical sense can be seen as the result of chaining links of immediate grounding. Let me close this section with two remarks about this gloss on the semantics.

My first remark is that the gloss is not formally implemented in the semantics. deRosset thinks of a grounding tree of height 2 (i.e., whose nodes are, apart from its root, only children of the root) as representing the fact occupying the root as being immediately grounded in the facts whose set occupies the set of the tree’s leaves. But nothing forces this interpretation of the grounding trees: as far as the characterization results are concerned, the grounding trees of height 2 may just as well be interpreted as representing the fact occupying the root as being grounded in the canonical sense in the facts whose set occupies the set of the tree’s leaves.

The second remark is that this very fact about the interpretation of the semantics, far from being a problem, may actually be argued to be a positive feature of the semantics: as I have argued elsewhere (Correia Reference Correia2021a: 5968), the view that there are facts that are grounded in the canonical sense without being immediately grounded cannot be lightly discarded.

2.4 Litland on Bicollective Grounding

As I emphasized in Section 1.2, Litland takes seriously the idea that there can be cases where several facts are metaphysically strictly fully grounded in some facts without the grounded facts being individually grounded in (some of) the grounding facts. To use Litland’s (Reference Litland, Bliss and Priest2018a) terminology, the idea is that metaphysical strict full grounding is bicollective rather than, as orthodoxy has it, (merely) left-collective.Footnote ¹⁸ Litland (Reference Litland2016, Reference Litland, Bliss and Priest2018a) proposes two very different semantics for the logic of bicollective grounding. The first one is a truthmaker semantics, the second one a graph-theoretic semantics.

2.4.1 Litland (Reference Litland2016)

The semantics in Litland (Reference Litland2016) is very much like Fine’s semantics for PLG.Footnote ¹⁹ The object language Litland focuses on is like the language of Fine’s PLG but with a few differences: it has, in addition to the four Finean ground-theoretic operators $<$ , $⩽$ , $\preccurlyeq$ and $\prec$ , the extra operator $⋠$ ; and the sequents of the language all take a set of basic sentences on the left and on the right, with no cardinality restrictions on these sets. $\Delta ⋠\Gamma$ is intended to express the negation of $\Delta \preccurlyeq \Gamma$ .

Litland, like Fine, uses generalized state models to interpret his sequents. Relative to every generalized state frame $F$ with underlying verification space $V$ , five ground-theoretic relations between sets of facts and sets of facts are defined (here again I use $⨅$ for ${⨅}_F$ ):

• $F{⩽}_{F}G$ iff ${}_{\text{df}}⨅F\subseteq ⨅G$ ;

• $F{\preccurlyeq }_{F}G$ iff ${}_{\text{df}}$ for some $F^{*}\subseteq V$ such that $F\subseteq F^{*}$ , $F^{*}{⩽}_{F}G$ ;Footnote ²⁰

• $F{⋠}_{F}G$ iff ${}_{\text{df}}$ it is not the case that $F{\preccurlyeq }_{F}G$ ;

• $F{<}_{F}G$ iff ${}_{\text{df}}F{⩽}_{F}G$ and $G{⋠}_{F}F$ ;

• $F{\prec }_{F}G$ iff ${}_{\text{df}}F{\preccurlyeq }_{F}G$ and $G{⋠}_{F}F$ .

Without surprise, the notion of holding in a generalized state model $M$ is defined as follows, where $F$ is $M$ ’s underlying generalized state frame and $\left[\right]$ is $M$ ’s valuation function:

• $\Delta ⩽\Gamma$ holds in $M$ iff $\left[\Delta \right]{⩽}_F\left[\Gamma \right]$

• $\Delta \preccurlyeq \Gamma$ holds in $M$ iff $\left[\Delta \right]{\preccurlyeq }_F\left[\Gamma \right]$

• $\Delta ⋠\Gamma$ holds in $M$ iff $\left[\Delta \right]{⋠}_F\left[\Gamma \right]$

• $\Delta <\Gamma$ holds in $M$ iff $\left[\Delta \right]{<}_F\left[\Gamma \right]$

• $\Delta \prec \Gamma$ holds in $M$ iff $\left[\Delta \right]{\prec }_F\left[\Gamma \right]$

Consequence is defined as before.

Even though Litland’s semantics is a truthmaker semantics of roughly the same sort as Fine’s semantics for PLG, it cannot be said to be strictly speaking an extension of it. The semantics for the sequents of type $\Delta ⩽\varphi$ in Fine’s logic is the same as the semantics for the sequents of type $\Delta ⩽\left\{\varphi \right\}$ in Litland’s logic, and therefore the two logics fully agree regarding the behaviour of the restriction of weak full grounding to cases involving individual groundees. But things are different when it comes to strict full grounding. For instance, as Litland notes, Amalgamation ( $<$ ) as formulated in the language of the bicollective logic, namely:

$\frac{{\Delta }_1<\left\{\varphi \right\}{\Delta }_2<\left\{\varphi \right\}\dots }{{\Delta }_1,{\Delta }_2,\dots <\left\{\varphi \right\}}$

is not validated by his semantics. This fact need not be seen as a problem – as I have stressed in Section 2.1, Litland (Reference Litland, Bliss and Priest2018a) himself explicitly argues against Amalgamation ( $<$ ). But let me mention two consequences of the semantics that look more problematic. Both are discussed by Litland (Reference Litland2016).

The first consequence is that the following rule is validated (I take the label from Litland Reference Litland, Bliss and Priest2018a):

$\frac{\Delta <\Gamma }{\Delta <\Gamma ,\Delta }\text{Self-Ground}$

Granted that $<$ expresses an explanatory relation, this does not sound acceptable. In the 2016 paper, Litland plays down the problem (page 548), but in Litland (Reference Litland, Bliss and Priest2018a) he takes it seriously (page 147). A natural way out, which he does not himself consider in that paper, is to adopt the following definition of ${<}_F$ instead of the original oneFootnote ²¹:

• $F{<}_{F}G$ iff ${}_{\text{df}}F{⩽}_{F}G$ and for all $G^{*}\subseteq G$ with $G^{*}\ne \varnothing$ , $G^{*}{⋠}_{F}F$ .

On this account, $\Delta <\Gamma ,\Delta$ fails to hold in any model provided that $\Delta \ne \varnothing$ .

The second consequence concerns the question of what grounds conjunctive facts, a question we will discuss in some detail in Section 3. As we will see, the standard treatment of conjunctions in truthmaker semantics has it that a conjunction is exactly verified by a state $s$ iff $s$ is the fusion of two states $s_1$ and $s_2$ such that $s_1$ exactly verifies one of the conjuncts and $s_2$ exactly verifies the other conjunct. Given this treatment of conjunctions, all sequents of type $\varphi \wedge \psi ⩽\varphi$ ,  $\psi$ hold in every model, and therefore no sequent of type $\varphi$ ,  $\psi <\varphi \wedge \psi$ can hold in a model. Litland admits that this is a problem if we think of strict full grounding as being explanatory. Since $\Delta <\Gamma$ holds in a model under my alternative definition of ${<}_F$ only if $\Delta <\Gamma$ holds in that model under Litland’s definition, my alternative definition does nothing to solve the problem.

2.5 Litland’s ‘Grounding Ground’ and ‘Pure Logic of Iterated Full Ground’

In his 2017 and 2018b papers, Litland develops in proof-theoretic fashion a logic of (merely left-collective) strict full grounding. The logic is based on an account of strict full grounding which in turn is based on two assumptions: (a) there is a distinction between arguments that are metaphysically explanatory (arguments whose pre-mises provide metaphysical explanations of why their conclusions hold) and arguments that are not, and (b) there is a distinction between factive ( $<$ ) and non-factive ( $\Rightarrow$ ) strict full grounding. The core of the account features the following two biconditionals:

1. (i) $\Delta \Rightarrow \varphi$ holds iff there is an explanatory argument from (exactly) $\Delta$ to $\varphi$ ;

2. (ii) $\Delta <\varphi$ holds iff $\Delta \Rightarrow \varphi$ and all the members of $\Delta$ hold.

(ii) records an obvious connection between factive and non-factive strict full grounding which is standardly acknowledged. (i) is Litland’s own contribution.

Litland (Reference Litland2017) offers an introduction rule and an elimination rule for both $\Rightarrow$ and $<$ . Litland (Reference Litland2018b) keeps the same rules but add two elimination rules, one for each operator, in order to guarantee that the system conforms to the view that the introduction rule(s) for an operator define that operator – a view that Litland adopts but which is not forced upon those who are sympathetic to (i) and (ii) above. The elimination rules present in both Litland (Reference Litland2017) and Litland (Reference Litland2018b) are called plain, those that are added in Litland (Reference Litland2018b) are called explanatory. I will leave the latter rules aside in what follows.

The proof-theory offered by Litland is quite complicated, especially because of the elimination rules. But the introduction rules are easy to state, and from them plus a few consequences of the plain elimination rules one can already derive interesting results.

The introduction rules are as follows:

$\begin{array}{c}{\bar{\Delta }}^1\\ E\\ \frac{\varphi }{\Delta \Rightarrow \varphi }\end{array}\Rightarrow \text{-Introduction}$

$\frac{\Delta \Delta \Rightarrow \varphi }{\Delta <\varphi }<-\text{Introduction}$

The second introduction rule can be immediately extracted from the right-to-left direction of biconditional (ii) above. The first introduction rule can also be extracted from the right-to-left direction of the corresponding biconditional, namely (i) above, but with a little twist. Unlike the second rule, it is a rule with discharge of assumptions. It may be read: conclude $\Delta \Rightarrow \varphi$ from any explanatory argument $E$ with $\varphi$ as conclusion where $\Delta$ are all and only the premisses on which $\varphi$ depends, and discharge all the premisses when drawing the conclusion.

Litland takes both introduction rules to generate explanatory arguments. The view that $<$ -Introduction generates explanatory arguments may be justified in a natural way by invoking the view that (a) for $\Delta <\varphi$ to hold just is for the members of $\Delta$ and $\Delta \Rightarrow \varphi$ to hold and the view that (b) the truth of a conjunction is explained, in the relevant sense, in the truth of its conjuncts. By contrast, it is not clear (to me, at least) how to justify the view that $\Rightarrow$ -Introduction generates explanatory arguments. However, the view that it does has an important consequence:

1. (C1) If $\Delta \Rightarrow \varphi$ has been established by an application of $\Rightarrow$ -Introduction, then $\Delta \Rightarrow \varphi$ is zero-grounded in the non-factive sense, that is, $\varnothing \Rightarrow (\Delta \Rightarrow \varphi )$ holds.

This consequence is important for two reasons. The first one is that it tells us that certain grounding facts are themselves grounded, and it tells us what they are grounded in. The second reason is that it provides an illustration of the prima facie somewhat obscure notion of zero-grounding.

The view that $<$ -Introduction generates explanatory arguments has the following consequence:

1. (C2) $(\Delta ,\Delta \Rightarrow \varphi )\Rightarrow (\Delta <\varphi )$ holds.

Using (C2) and $<$ -Introduction, one can infer:

1. (C3) If the members of $\Delta$ and $\Delta \Rightarrow \varphi$ hold, then $(\Delta ,\Delta \Rightarrow \varphi )<(\Delta <\varphi )$ holds.

We can get ‘simplified’ versions of (C2) and (C3) by using (C1). The plain elimination rule for $\Rightarrow$ allows one to establish the strong cut rule for $\Rightarrow$ , namely:

$\frac{{\Delta }_1\Rightarrow {\varphi }_1{\Delta }_2\Rightarrow {\varphi }_2\dots {\varphi }_1,{\varphi }_2,\dots ,\Gamma \Rightarrow \psi }{{\Delta }_1,{\Delta }_2,\dots ,\Gamma \Rightarrow \psi }\text{Cut}(\Rightarrow )$

Given Cut ( $\Rightarrow$ ), (C1) and (C2) yield the following:

1. (C4) If $\Delta \Rightarrow \varphi$ has been established by an application of $\Rightarrow$ -Introduction, then $\Delta \Rightarrow (\Delta <\varphi )$ holds.

Using (C4) and $<$ -Introduction, one can then infer:

1. (C5) If $\Delta \Rightarrow \varphi$ has been established by an application of $\Rightarrow$ -Introduction, and if all the members of $\Delta$ hold, then $\Delta <(\Delta <\varphi )$ holds.

This latter principle is a restricted version of the principle which states that factive strict full grounding is superinternal, that is, the principle that if $\Delta <\varphi$ holds, then $\Delta <(\Delta <\varphi )$ also holds – a principle explicitly endorsed by Bennett (Reference Bennett2011) and deRosset (Reference deRosset2013b).

$\Rightarrow$ -Introduction and the plain elimination rule for $\Rightarrow$ together guarantee that something stronger than (C1) is the case, namely:

1. (C1 * ) If $\Delta \Rightarrow \varphi$ holds, then $\varnothing \Rightarrow (\Delta \Rightarrow \varphi )$ holds.