The Logic of Grounding

Summary

The concept of grounding – of a fact obtaining in virtue of other facts – has been a topic of intensive philosophical and logical investigation over roughly the past two decades. Many philosophers take grounding to deserve a central place in metaphysical theorizing, in great part because it is thought to do a better job than other concepts – e.g., reduction and supervenience – at capturing certain phenomena. Studies on the logic of grounding have largely been conducted with this philosophical background in mind. In this Element, I try to give a faithful picture of the contemporary development of the logic of grounding in a way that is both reasonably comprehensive and reasonably systematic.

Introduction

Although the concept of grounding has been widely used throughout the history of western philosophy (see Raven 2020, part I), it has almost never been a proper topic of investigation until the beginning of the twenty-first century. Bolzano (1837) is a significant counterexample – to my knowledge, the only one – to the claim that grounding has never up to that period been a proper topic of investigation (see Roski and Schnieder 2022). The starting point of current theorizing about grounding can be traced back to the works of Fine (2001, 2010, 2012a, 2012b), Correia (2005, 2010), Schaffer (2009, 2010), Rosen (2010) and Schnieder (2010, 2011).

The topic of this Element – the logic of grounding – is part and parcel of the study of grounding, just like modal logic is part and parcel of the study of necessity and possibility and tense logic is part and parcel of the study of the concepts of past, present and future.

The logic of grounding does not have the grandiose pedigree of modal logic and tense logic, and it has achieved much less than them. One sometimes hears sceptical complaints against the very concept of grounding based precisely on the fact that the logic of grounding is not even close to its venerable cousins in terms of systematicity and other theoretical virtues. But it should not be surprising that logical theorizing about grounding is in the state it currently is, for two reasons. The first one is that – leaving (again) Bolzano aside – work on the logic of grounding is very recent: the first published works on the topic are from 2010. Bear in mind that about 50 years elapsed from the impetus of C. I. Lewis’s work on modal logic to the beauties of Kripke-style semantics, at a time when there was not shortage of talented logicians. The second reason is that grounding is, unlike modal and tense-logical notions as standardly understood, hyperintensional rather than ‘merely intensional’. Kripke-style semantics is a wonderful tool to model intensional notions. We do not have comparable tools to handle hyperintensionality. Hyperintensional notions, such as grounding and (plausibly) essence, knowledge, obligation and many others, are notoriously very difficult to handle in a satisfactory way.

In what follows, I try to give a faithful picture of the development of the logic of grounding over the twelve years or so preceding the writing of this Element, in a way that is at the same time reasonably comprehensive and reasonably systematic. Due to space limitation, some sacrifices had to be made in both respects – I explicitly mention some of them in due course – but hopefully they are not too many or too significant.

The plan is as follows. Section 1 introduces the notion of grounding in its multiple variants or species. Sections 2 and 3 deal with the logic of grounding, the ‘pure’ logic and the ‘impure’ logic, respectively. Section 4 is devoted to two further topics: the theory of ground-theoretic equivalence and cognate notions and the puzzles of grounding.

1 The Jungle of Grounding

A great number of notions of grounding have been distinguished in the literature, and different logics of grounding often target different such notions. In this section, I try to give a reasonably comprehensive survey of these notions.

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 holds¹:

(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 2014 and Skiles 2015). 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 holds²:

(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.³ 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 2015 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. 2021).

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 2012a and Litland 2017). 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 2014 and Litland 2016).

Being factive.

Several authors countenance notions of grounding that are not factive (see for instance Correia 2014, 2017; Fine 2012a and Litland 2017).

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 2005, 2014 and Fine 2012a).

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 2012a). 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 (2012a) 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.⁴ Other notions of grounding discussed in the literature lack one or both of these features:

Being full.

Fine (2012a) 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 (2012a) 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 2012a 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 2012a). 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 Pure Logics

Following established terminology, I call a logic of grounding pure if it only deals with the structural properties of grounding, that is, the properties that grounding has irrespective of the logical structure of the grounds and the groundees. The studies discussed in Section 2.5 are purely proof-theoretic. Those discussed in the previous sections put forward semantics for the logic of grounding, some together with corresponding sound and complete proof systems. These semantics are of two kinds. Fine (2012b) (discussed in Section 2.1) invokes what is often called a ‘truthmaker semantics’. deRosset (2014) (discussed in Section 2.2) and Litland (2016) (discussed in Section 2.4) also put forward such semantics. The remaining studies – deRosset (2015) and Litland (2018a) (discussed in Sections 2.3 and 2.4, respectively) – invoke graph-/tree-theoretic semantics.

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.⁵ 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.⁶ 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.⁷ 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.⁸ 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 that⁹, ¹⁰:

• $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.¹¹ 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 (2012b) main result is that consequence so defined and derivability in PLG coincide:

Theorem 1 (Soundness and completeness for PLG). A sequent $\sigma$ is derivable from a set of sequents $\Sigma$ in PLG iff $\sigma$ is a PLG-consequence of $\Sigma$ .

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:

1. 1. Let $\sigma$ be a sequent from the language of PLWFL and $\Sigma$ a set of sequents from the same language. Then $\sigma$ is derivable from $\Sigma$ in PLWFG iff $\sigma$ is derivable from $\Sigma$ in PLG.

2. 2. Let $\sigma$ be a sequent from the language of PLSFL and $\Sigma$ a set of sequents from the same language. Then $\sigma$ is derivable from $\Sigma$ in PLSFG iff $\sigma$ is derivable from $\Sigma$ in PLG.

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:

1. 1. A sequent $\sigma$ is derivable from a set of sequents $\Sigma$ in PLWFG iff $\sigma$ is a PLWFG-consequence of $\Sigma$ .

2. 2. A sequent $\sigma$ is derivable from a set of sequents $\Sigma$ in PLSFG iff $\sigma$ is a PLSFG-consequence of $\Sigma$ .

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 2014 and Woods 2018),¹² 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 2012), from which it follows that Cut ( $<$ ) fails; and the validity of Amalgamation ( $<$ ) has been questioned (see deRosset 2015, Litland 2018a and Litland 2018b). These objections are important and would therefore deserve extensive discussion, but for lack of space I will leave them aside.¹³

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 (2013a, 2014) has argued that what Fine (2012a, 2012b) 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:

Let $\psi$ be a sentence expressing that Maria is sad and $\varphi$ a sentence expressing that Maria is sad or Sam is happy, and suppose that Maria is sad and Sam is not happy. Let then $M$ be a privileged model for a language comprising the sequent $\varphi ⩽\psi$ . Relative to $M$ , $\psi$ and $\varphi$ have exactly the same exact verifiers, and therefore $\varphi ⩽\psi$ comes out as true. But $\varphi ⩽\psi$ is not true.

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 2012a and Fine 2012b, but are made explicit in later work on the truthmaker framework (e.g., in Fine 2017a). 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 (2014), 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 }^{*}$ ).¹⁴ 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:

Theorem 4 (Soundness and completeness for LSG). A sequent $\sigma$ is derivable from a set of sequents $\Sigma$ in LSG iff $\sigma$ is an LSG-consequence of $\Sigma$ .

The way he proceeds, in effect, is as follows.¹⁵ 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:

Theorem 5. Let $\sigma$ be a sequent from the language of LSG ${}^{-}$ and $\Sigma$ a set of sequents from the same language. Then $\sigma$ is derivable from $\Sigma$ in LSG ${}^{-}$ iff $\sigma$ is derivable from $\Sigma$ in PLG.

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

Theorem 6 (Soundness and completeness for LSG − ). A sequent $\sigma$ is derivable from a set of sequents $\Sigma$ in LSG ${}^{-}$ iff $\sigma$ is an LSG ${}^{-}$ -consequence of $\Sigma$ .

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 2015), 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 (2015) 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 2012a – 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.¹⁶ 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:

For any tree $T$ and family of trees $(T_i{)}_{i\in I}$ in $T$ such that the former can be extended with the latter, there is a grounding tree in $T$ that does extend $T$ with $(T_i{)}_{i\in I}$ .

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 }^{*}$ .¹⁷ 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:

Theorem 7 (Soundness and completeness for LSG and its subsystems). Let $\sigma$ be a sequent and $\Sigma$ a set of sequents of the language. Then:

1. 1. $\sigma$ is derivable from $\Sigma$ in B iff $\sigma$ holds in every grounding model in which all the members of $\Sigma$ hold.

2. 2. $\sigma$ is derivable from $\Sigma$ in BNC iff $\sigma$ holds in every acyclic grounding model in which all the members of $\Sigma$ hold.

3. 3. $\sigma$ is derivable from $\Sigma$ in BA iff $\sigma$ holds in every additive grounding model in which all the members of $\Sigma$ hold.

4. 4. $\sigma$ is derivable from $\Sigma$ in LSG iff $\sigma$ holds in every acyclic and additive grounding model in which all the members of $\Sigma$ hold.

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 2021a: 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 (2018a) terminology, the idea is that metaphysical strict full grounding is bicollective rather than, as orthodoxy has it, (merely) left-collective.¹⁸ Litland (2016, 2018a) 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 (2016)

The semantics in Litland (2016) is very much like Fine’s semantics for PLG.¹⁹ 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$ ;²⁰

• $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 (2018a) himself explicitly argues against Amalgamation ( $<$ ). But let me mention two consequences of the semantics that look more problematic. Both are discussed by Litland (2016).

The first consequence is that the following rule is validated (I take the label from Litland 2018a):

$\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 (2018a) 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 one²¹:

• $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.4.2 Litland (2018a)

As previously announced, Litland (2018a) offers another, graph-theo-retic semantics for bicollective grounding. In fact, he also puts forward a graph-theoretic semantics for the Finean notions of grounding, which is essentially the same semantics as deRosset’s (2015) when restricted to the notions deRosset aims to characterize.²² It would take me too far to give the reader a faithful summary of the account, so let me just get to the bare bones.

Just like deRosset’s (2015) semantics, Litland’s semantics can be reformulated directly in terms of labelled trees, without appealing to hypergraphs. The basic idea is to define a grounding tree, not as a labelled tree tout court, but as a labelled tree whose labels are sets. In contrast with the semantics presented in Section 2.3, we take the facts of a grounding tree to be the members of its labels rather than the labels themselves. As before, we then define grounding frames as sets of grounding trees satisfying certain properties (meant to guarantee that bicollective notions of grounding satisfy desired conditions, e.g., transitivity / cut conditions), and grounding models as grounding frames equipped with an interpretation function. The definition of bicollective strict full grounding relative to a grounding frame $T$ is then taken to go as follows:

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

(Compare with the definition of ${<}_T$ on page 20, especially the second clause.)

It is clear that even after suitable conditions on grounding frames have been imposed to ensure that bicollective $<$ satisfies desired principles of cut and irreflexivity, Self-Ground will not be validated. It also seems clear that the proposed semantics is not inhospitable to the view that sequents of type $\varphi$ , $\psi <\varphi \wedge \psi$ can hold.

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 (2017) offers an introduction rule and an elimination rule for both $\Rightarrow$ and $<$ . Litland (2018b) 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 (2017) and Litland (2018b) are called plain, those that are added in Litland (2018b) 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 (2011) and deRosset (2013b).

$\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.

Using this, one of course obtains strengthened versions of (C4) and (C5):

1. (C4 * ) If $\Delta \Rightarrow \varphi$ holds, then $\Delta \Rightarrow (\Delta <\varphi )$ holds.

2. (C5 * ) If $\Delta \Rightarrow \varphi$ holds, and if all the members of $\Delta$ hold, then $\Delta <(\Delta <\varphi )$ holds.

Taking on board the plain elimination rule for $<$ , one gets the left-to-right direction of biconditional (ii) above.²³ Using (C5 ${}^{*}$ ), one then gets:

1. (C6) If $\Delta <\varphi$ holds, then $\Delta <(\Delta <\varphi )$ holds.

This is the unrestricted principle of superinternality.

As we saw, the 2017 logic has Cut ( $\Rightarrow$ ). It also has Cut ( $<$ ). We also saw that the logic has left-factivity for $<$ : if $\Delta <\varphi$ holds, then all the members of $\Delta$ hold. It also has right-factivity: if $\Delta <\varphi$ holds, then $\varphi$ holds. Non-Circularity ( $<$ ) is also validated by the logic, thanks to a specific non-circularity principle governing certain arguments containing explanatory arguments introduced by Litland. Interestingly, the counterpart of the principle for $\Rightarrow$ is not validated by the logic, and Litland in fact suggests a counterexample (see 2018b: 419). Finally, the logic validates neither Amalgamation ( $<$ ) nor its non-factive counterpart: given that there is an explanatory argument from $\Delta$ to $\varphi$ and another explanatory argument from $\Gamma$ to $\varphi$ , there is no guarantee that there is an explanatory argument from $\Delta ,\Gamma$ to $\varphi$  – whether or not the members of $\Delta ,\Gamma$ hold.²⁴

Let me close this section by pointing to a fact that the reader may have noticed: (C1)–(C6), (C1 ${}^{*}$ ), (C4 ${}^{*}$ ) and (C5 ${}^{*}$ ) all involve iterations of ground-theoretic operators. This is worth emphasizing, because all the other approaches to the pure logic of grounding that I have presented above either impose a grammatical ban on such iterations, or are silent on the principles that govern propositions that involve them.

3 Impure Logics

The pure logic of grounding is of limited interest. It is of course important to be clear on the structural properties of the various grounding relations we are interested in, but we also want to know how grounding interacts with other notions, in particular with the notions expressed by the so-called logical constants. The impure logic of grounding deals with the interaction between grounding and other notions, insofar as these notions are involved in the grounds and the groundees. Thus, for instance, principles of the impure logic of grounding may include the principle that $\varphi$ ,  $\psi <\varphi \wedge \psi$ holds whenever $\varphi$ and $\psi$ both hold, or, where $◊$ is a possibility operator, the principle that $\varphi <◊\varphi$ holds whenever $\varphi$ holds. The literature on the impure logic of grounding has massively focused on the interaction of grounding with conjunction, disjunction and negation. In this section, I will focus exclusively on the interaction with these three notions. Interaction with the quantifiers and with lambda abstraction will be (somewhat briefly) discussed in Section 4.2.²⁵

This section is divided into seven parts. The first four parts (Sections 3.1 to 3.4) discuss logics for notions of grounding that I classify as ‘worldly’, the next two parts (Sections 3.5 and 3.6) logics for notions of grounding that I classify as ‘representational’ (I introduce the worldly / representational distinction briefly in Section 3.5, and say more in Section 4.1). The last part (Section 3.7) briefly presents works that have not been discussed in the previous parts. The decision of which works should feature in this last part as opposed to the previous parts has been guided by my intention to prioritize works which establish soundness and completeness for systems relative to associated semantics, and other works closely related to the latter.

3.1 Fine’s ‘Guide to Ground’ (Semantic Side)

Fine’s (2012b) semantics for the pure logic of grounding can easily be extended to a semantics for an impure logic by interpreting the standard connectives $\wedge$ , $\vee$ and $\neg$ in the exact verification framework. Fine (2012a) suggests a way of doing just that.²⁶ The presentation of the semantics offered in the 2012a paper is somewhat informal; let me be a bit more precise, taking the semantics of the 2012b paper as my starting point (see Correia 2023). I previously stressed (footnote 5) that the extension of the 2012b semantics to be presented here requires a conception of the Finean grounding relations as non-factive. It will be important to keep this in mind.

The language in which the logic is formulated is like the language of the pure logic as specified in Fine (2012b), except that the basic sentences are now taken to be constructed from a pool of atomic sentences, the connectives $\wedge$ , $\vee$ and $\neg$ and a pair of brackets in the usual way. The language is interpreted in structures that are similar to, but not identical with, the ones that were used for the pure logic.

Before introducing these structures, let me define two binary operations ${\sqcap }_F$ and ${\bigsqcup }_F$ on sets of states relative to an arbitrary state frame (generalized or not) $F$ :

• $S_1{\sqcap }_F{S}_2{=}_{\text{df}}{⨅}_F\{S_1,S_2\}$

• $S_1{\bigsqcup }_F{S}_2{=}_{\text{df}}{S}_1\cup S_2\cup \left(S_1{\sqcap }_F{S}_2\right)$

(As with $⨅$ , I will feel free to omit the indices when no confusion threatens.) Given the role ${\sqcap }_F$ and ${\bigsqcup }_F$ play in the semantics of $\wedge$ and $\vee$ (see below), it is appropriate to view ${\sqcap }_F$ as an operation of conjunction on sets of states and ${\bigsqcup }_F$ as an operation of disjunction on sets of states. Given the role ${\sqcap }_F$ plays in the semantics of $\wedge$ , it is also appropriate to view ${⨅}_F$ as a generalized operation of conjunction on sets of states, one that can operate on an arbitrary number (including 0) of sets of states. A generalized operation of disjunction on sets of states can also be defined:

• For $S$ a non-empty set of sets of states, $\underset{F}{⨆}S{=}_{\text{df}}{⨅}_F{S}_1\cup {⨅}_F{S}_2\cup \dots$ , where $S_1$ , $S_2$ , $\dots$ are all the non-empty subsets of $S$ .

(I leave aside the question of how $\underset{F}{⨆}\varnothing$ should be defined.) We will need this operation at a later point.

We still call the models for the new language generalized state models, but they are now taken to be tuples $⟨S,\prod ,V,[{]}^{+},[{]}^{-}⟩$ where:

• $⟨S,\prod ,V⟩$ is a generalized state frame that satisfies the following closure conditions:

  • – for any $F_1,F_2\in V$ , $F_1{\sqcap }_F{F}_2\in V$ ;

  • – for any $F_1,F_2\in V$ , $F_1{\bigsqcup }_F{F}_2\in V$ ;

• $[{]}^{+}$ (verification valuation) and $[{]}^{-}$ (falsification valuation) are two functions which take each atomic sentence of the language into a member of $V$ .

Thus, the new models differ from the original models in three ways. First, the underlying frames are not any generalized state frames: they must satisfy the specified closure conditions. The restriction is motivated by the way conjunction and disjunction are to be interpreted. Second, instead of involving one valuation function, they involve two: one that represents exact verification, and another one that represents exact falsification. The latter notion is new, but easy to grasp once one has grasped the notion of exact verification. The idea of having two valuation functions is motivated by the way negation is to be interpreted. The third difference is, without surprise, that these two functions map every atom (rather than every basic sentence) of the language into a member of the verification space of the associated model.

Given a generalized state model $⟨S,\prod ,V,[{]}^{+},[{]}^{-}⟩$ , the verification relation $⊩$ and the falsification relation $⫣$ between states and basic sentences are defined inductively as follows:

• $s⊩\varphi$ iff $s\in [\varphi {]}^{+}$

  $s⫣\varphi$ iff $s\in [\varphi {]}^{-}$    for $\varphi$ atomic

• $s⊩\neg \varphi$ iff $s⫣\varphi$

  $s⫣\neg \varphi$ iff $s⊩\varphi$

• $s⊩\varphi \wedge \psi$ iff for some $s_1$ and $s_2$ such that $s=s_1{s}_2$ , $s_1⊩\varphi$ and $s_2⊩\psi$

  $s⫣\varphi \wedge \psi$ iff $s⫣\varphi$ or $s⫣\psi$ or $s⫣\varphi \vee \psi$

• $s⊩\varphi \vee \psi$ iff $s⊩\varphi$ or $s⊩\psi$ or $s⊩\varphi \wedge \psi$

  $s⫣\varphi \vee \psi$ iff for some $s_1$ and $s_2$ such that $s=s_1{s}_2$ , $s_1⫣\varphi$ and $s_2⫣\psi$

We may extend $[{]}^{+}$ and $[{]}^{-}$ to arbitrary basic formulas by putting $[\varphi {]}^{+}=\{s:s⊩\varphi \}$ and $[\varphi {]}^{-}=\{s:s⫣\varphi \}$ . We then have:

• $[\neg \varphi {]}^{+}=[\varphi {]}^{-}$

  $[\neg \varphi {]}^{-}=[\varphi {]}^{+}$

• $[\varphi \wedge \psi {]}^{+}=[\varphi {]}^{+}\sqcap [\psi {]}^{+}$

  $[\varphi \wedge \psi {]}^{-}=[\varphi {]}^{-}\bigsqcup [\psi {]}^{-}$

• $[\varphi \vee \psi {]}^{+}=[\varphi {]}^{+}\bigsqcup [\psi {]}^{+}$

  $[\varphi \vee \psi {]}^{-}=[\varphi {]}^{-}\sqcap [\psi {]}^{-}$

The requirement that $V$ should satisfy the closure conditions mentioned in the definition of generalized state models guarantees that both $[\varphi {]}^{+}$ and $[\varphi {]}^{-}$ are members of $V$ for any basic sentence $\varphi$ . Importantly, if $S_1$ and $S_2$ are facts of the model (i.e., sets of states closed under $\prod$ ), then not only is it the case that $S_1\sqcap S_2$ is also a fact, but the same also holds of $S_1\bigsqcup S_2$ . It follows that the closure conditions are automatically satisfied if $V$ is the set of all the facts of the model.²⁷ The notion of holding in a model for sequents of the language is defined exactly as it was in the pure logic.

Fine (2012a) does not investigate the principles governing the interaction between grounding and truth-functions that his semantics delivers.²⁸ Let me go some way in that direction, taking inspiration from Correia (2010) (which will be the focus of the next section).

The semantics validates the following interaction principles:

$\frac{\Delta <\varphi \Gamma <\psi }{\Delta ,\Gamma <\varphi \wedge \psi }\wedge -\text{Introduction 1}$

$\frac{\Delta <\varphi }{\Delta <\varphi \vee \psi }\frac{\Delta <\psi }{\Delta <\varphi \vee \psi }\vee \text{-Introduction 1}$

$\frac{\Delta ,\varphi \wedge \psi <\chi }{\Delta ,\varphi ,\psi <\chi }\wedge \text{-Elimination}$

$\frac{\Delta ,\varphi \vee \psi <\chi }{\Delta ,\varphi <\chi }\frac{\Delta ,\varphi \vee \psi <\chi }{\Delta ,\psi <\chi }\vee \text{-Elimination}$

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

$\frac{\Delta ,\neg \neg \varphi <\psi }{\Delta ,\varphi <\psi }\neg \neg \text{-Elimination}$

To this list, one can add the principles that result from the first four principles by replacing $\varphi$ by $\neg \varphi$ , $\psi$ by $\neg \psi$ , $\varphi \wedge \psi$ by $\neg (\varphi \vee \psi )$ and $\varphi \vee \psi$ by $\neg (\varphi \wedge \psi )$  – I will dub principles that result from such replacements duals of the original principles.

The following introduction principles involving weak full grounding, as well as the duals of the first two principles, are also validated:

$\frac{}{\varphi ,\psi ⩽\varphi \wedge \psi }\wedge \text{-Introduction}(⩽)$

$\frac{}{\varphi ⩽\varphi \vee \psi }\frac{}{\psi ⩽\varphi \vee \psi }\vee \text{-Introduction}(⩽)$

$\frac{}{\varphi ⩽\neg \neg \varphi }\neg \neg \text{-Introduction}(⩽)$

Some might expect that a logic of strict full grounding should validate the same principles but with $<$ replacing $⩽$ . This is true of some logics (see Section 3.5), but not of this one. It is immediate that $\varphi <\neg \neg \varphi$ cannot hold in a generalized state model: for any such model with underlying frame $F$ and verification valuation $[{]}^{+}$ , $[\varphi {]}^{+}=[\neg \neg \varphi {]}^{+}$ and therefore $\left[\neg \neg \varphi {]}^{+}{\preccurlyeq }_F\right[\varphi {]}^{+}$ . It is equally clear that $\varphi <\varphi \wedge \varphi$ and $\varphi <\varphi \vee \varphi$ cannot hold in a generalized state model: relative to any such model, $\varphi$ , $\varphi \wedge \varphi$ and $\varphi \vee \varphi$ have the very same verifiers. Likewise, $\neg \varphi <\neg (\varphi \wedge \varphi )$ and $\neg \varphi <\neg (\varphi \vee \varphi )$ cannot hold in a generalized state model.

However, restricted versions of the introduction principles that involve $\wedge$ and $\vee$ , as well as their duals, are validated. Let me borrow Litland’s (2016) symbol $⋠$ , which I take here to stand for the negation of the Finean (non-bicollective) $\preccurlyeq$ . The restricted introduction principles are the following:

$\frac{\varphi \wedge \psi ⋠\varphi \varphi \wedge \psi ⋠\psi }{\varphi ,\psi <\varphi \wedge \psi }\wedge \text{-Introduction 2}$

$\frac{\varphi \vee \psi ⋠\varphi }{\varphi <\varphi \vee \psi }\frac{\varphi \vee \psi ⋠\psi }{\psi <\varphi \vee \psi }\vee \text{-Introduction 2}$

Equivalent principles can be formulated using $\prec$ rather than $⋠$ , but these principles are more perspicuous.²⁹

Let me close this section with the question of how to modify the semantics in order to get a proper semantic characterization of factive notions of grounding. The question is easily answered (see Correia 2023, section 2). Endow each generalized state model with a function that selects a set of states as being, intuitively, the set of states that are the case. A fact of a generalized state model is said to obtain when it contains a state that is the case. Using this notion of fact-obtainment, factive notions of grounding can naturally be defined in terms of the non-factive notions.

3.2 Correia’s ‘Grounding and Truth-Functions’

In Correia (2010), I introduce an algebraic semantics for the logic of grounding that is in some respects quite different from Fine’s (2012a, 2012b) truthmaker semantics. Yet – somewhat surprisingly – the two approaches turn out to have something deep in common.³⁰ In order to show this, and before presenting my algebraic semantics, let me first elaborate a bit on Fine’s account.

Consider a Finean generalized state frame $F$ that is full, that is, whose verification space is the set of all the facts of the frame, with state-fusion operation $\prod$ . Let ${⨅}_F$ be its generalized operation of conjunction on sets of states, ${\sqcap }_F$ the corresponding binary operation, and ${\bigsqcup }_F$ its binary disjunction operation on sets of states. Define the binary relations ${⪕}_F$ of disjunctive parthood and ${⋞}_F$ of partial disjunctive parthood between $F$ ’s facts as follows:

(Def- ${⪕}_F$ )

$F{⪕}_{F}G$ iff ${}_{\text{df}}$ for some fact $H$ , $F{\bigsqcup }_{F}H=G$ ;

(Def- ${⋞}_F$ )

$F{⋞}_{F}G$ iff ${}_{\text{df}}$ for some fact $H$ , $F{\sqcap }_{F}H{⪕}_{F}G$ .

One can show that for any facts $F$ and $G$ of the frame, $F{⪕}_{F}G$ iff $F\subseteq G$ (the fact that facts are closed under $\prod$ is crucial to establish this), and therefore that ${⪕}_F$ is coextensive with the frame’s weak full grounding relation ${⩽}_F$ restricted to grounds with just one member. One can also show that $F{⋞}_{F}G$ iff $F{\preccurlyeq }_{F}G$ , where ${\preccurlyeq }_F$ is the frame’s weak partial grounding relation (here as well the closure property is crucial). It follows that the frame’s strict full grounding relation ${<}_F$ can be given the following characterization:

(Char- ${<}_F$ )

$F{<}_{F}F$ iff ${⨅}_{F}F{⪕}_{F}F$ and for no $G\in F$ does $F{⋞}_{F}G$ .

As we will see shortly, this is essentially the characterization put forward in Correia (2010).

In Correia (2010), the basic structures invoked in the semantics are tuples $⟨F,\sqcap ,-⟩$ , where $F$ is a nonempty set, interpreted as a set of facts (these facts play the same semantic role as Fine’s facts, see below), $\sqcap$ is a binary operation on $F$ , interpreted as an operation of conjunction, and $-$ a unary operation on $F$ , interpreted as an operation of negation. The two operations are required to satisfy certain principles. Define an operation $\bigsqcup$ of disjunction on facts in terms of the two primitive operations in the obvious way:

• $F\bigsqcup G{=}_{\text{df}}-(-F\sqcap -G)$ .

The principles that $\sqcap$ and $-$ are required to satisfy are the following ones:

• $-F\ne F$

• $--F=F$

• $F\sqcap F=F$

• $F\sqcap G=G\sqcap F$

• $F\sqcap (G\sqcap H)=(F\sqcap G)\sqcap H$

• $F\bigsqcup (G\sqcap H)=(F\bigsqcup G)\sqcap (F\bigsqcup H)$

(These properties deserve discussion, of course; see below.) I will call such structures factual structures.³¹

Given a factual structure $S$ with (primitive) conjunction operation $\sqcap$ and (defined) disjunction operation $\bigsqcup$ , a relation ${⪕}_S$ of disjunctive parthood and a relation ${⋞}_S$ of partial disjunctive parthood can be defined as in (Def- ${⪕}_F$ ) and (Def- ${⋞}_F$ ) above (I use different symbols in the 2010 paper). On my 2010 approach, (non-factive) strict full grounding is understood as a relation that is characterized exactly as ${<}_F$ in (Char- ${<}_F$ ), with two minor provisos: the set of grounds is taken to be non-empty and finite, and generalized fact-conjunction is defined in terms of the binary operator $\sqcap$ .³² Thus, the difference between Fine’s approach and mine appears to boil down to this: (a) whereas I take facts to be sui generis entities, Fine’s facts are defined as sets of states closed under the operation of state-fusion, (b) whereas I take fact-conjunction as a primitive operation and fact-disjunction as an operation defined in terms of fact-conjunction and fact-negation, Fine’s fact-conjunction and fact-disjunction are both defined in terms of state-fusion (and set-theoretic union), and (c) unlike Fine, I do not endow my models with a distinguished set of facts capable of being the semantic values of statements.

Factual structures can be used to interpret various languages. Sequent languages like the one in Fine (2012a) provide straightforward examples. Define a factual model for such a language to be a tuple $⟨F,\sqcap ,-,\left[\right]⟩$ , where $⟨F,\sqcap ,-⟩$ is a factual structure and $\left[\right]$ a valuation function that takes each atomic sentence of the language into a member of $F$ . Let $M=⟨F,\sqcap ,-,\left[\right]⟩$ be an arbitrary factual model and let $S$ be the underlying factual structure. $\left[\right]$ is extended to all basic sentences of the language via the obvious clauses:

• $\left[\neg \varphi \right]=-\left[\varphi \right]$

• $[\varphi \wedge \psi ]=\left[\varphi \right]\sqcap \left[\psi \right]$

• $[\varphi \vee \psi ]=\left[\varphi \right]\bigsqcup \left[\psi \right]$

If the language contains sequents of type $\Delta <\varphi$ with $\Delta$ non-empty and finite, then – in conformity with the previous considerations – we put:

• $\Delta <\varphi$ holds in $M$ iff $⨅\left[\Delta \right]{⪕}_S\left[\varphi \right]$ and for no $G\in \left[\Delta \right]$ does $\left[\varphi \right]{⋞}_{S}G$

( $⨅$ is to be defined in terms of $\sqcap$ in the obvious way.) On that account, all the introduction and elimination rules mentioned at the end of Section 3.1 are validated, as well as the rules of Fine’s PLSFG – namely Cut ( $<$ ), Non-Circularity ( $<$ ) and Amalgamation ( $<$ ). For the other types of Finean sequents, we naturally put:

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

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

• $\varphi \prec \psi$ holds in $M$ iff $\left[\varphi \right]{⋞}_S\left[\psi \right]$ but not $\left[\psi \right]{⋞}_S\left[\varphi \right]$

Given these clauses, all the rules of Fine’s PLG are validated.

Unlike the languages that have been introduced so far in this and the previous section, the language I focus on in Correia (2010) is not a pure sequent language: it allows the combination of sequents with truth-function-al connectives, and quantification into sentential position. More precisely, the vocabulary of the language comprises (i) atomic sentences, (ii) sentential variables, (iii) the classical connectives $\wedge$ , $\vee$ and $\neg$ , (iv) the sentential existential quantifier $\exists$ , (v) the operator $<$ for factive strict full grounding (I use another symbol in the paper) and the operator $\approx$ for factual equivalence (this is a new notion, but its semantics is straightforward – see below), (vi) the brackets (and). The basic formulas are built from the atomic sentences and the sentential variables using the classical connectives and the brackets, and the formulas of the language are defined as follows:

• The basic formulas are formulas;

• If $\Delta$ is a non-empty finite set of basic formulas and $\varphi$ a basic formula, $\left(\Delta <\varphi \right)$ is a formula³³;

• If $\varphi$ and $\psi$ are basic formulas, $(\varphi \approx \psi )$ is a formula;

• If $A$ and $B$ are formulas, so are $(A\wedge B)$ and $(A\vee B)$ ;

• If $A$ is a formula, so is $\neg A$ ;

• If $A$ is a formula and $x$ a sentential variable, $\exists xA$ is a formula.

Disjunctive parthood and partial disjunctive parthood are definable in the language (with the variable so chosen as to avoid unwanted binding):

• $\varphi ⪕\psi :=\exists x\left(\right(\varphi \vee x)\approx \psi )$

• $\varphi ⋞\psi :=\exists x\left(\right(\varphi \wedge x)⪕\psi )$

I will adopt standard definitions and notational conventions. I will use $\varphi ⋠\psi$ for $\neg (\varphi ⋞\psi )$ , and where $\Delta$ is a non-empty finite set of basic formulas, I will take $\bigwedge \Delta$ to stand for a particular basic formula built from $\Delta$ ’s members and $\wedge$ such that every member of $\Delta$ appears exactly once in the formula (which formula it is exactly does not matter since all such formulas are logically equivalent from the point of view of the logic to be introduced below).

The language is interpreted by means of factual models as defined above but enriched with a function that selects a set of facts (intuitively: the facts that obtain) such that the conjunction of two facts obtain iff both facts obtain, and the negation of a fact obtains iff the fact fails to obtain. The reason why there is this extra element in the models is that, unlike in logics we previously encountered, the basic sentences can be assessed as being true or not true relative to models. Having this extra element allows one to semantically characterize, in addition to a non-factive notion of strict full grounding, a factive notion.

Consider an enriched factual model $M=⟨F,\sqcap ,-,ob,\left[\right]⟩$ , where $ob$ is a subset of $F$ that represents the set of all the facts that obtain. Where $\rho$ is an assignment of values to the variables and $\varphi$ is an atomic sentence or a sentential variable, we let $[\varphi {]}_{\rho }$ be $\left[\varphi \right]$ if $\varphi$ is an atomic sentence and $\rho \left(\varphi \right)$ if $\varphi$ is a sentential variable. $[{]}_{\rho }$ is then extended to all basic formulas in the obvious way. The notion of a formula $A$ ’s holding in $M$ relative to an assignment of values to the variables $\rho$  – symbolized by $M,\rho \models A$  – is defined as follows:

• $M,\rho \models \varphi$ iff $[\varphi {]}_{\rho }\in ob$ for $\varphi$ a basic formula;

• $M,\rho \models \Delta <\varphi$ iff (a) $⨅\left[\Delta {]}_{\rho }{⪕}_S\right[\varphi {]}_{\rho }$ and for no $G\in [\Delta {]}_{\rho }$ does $[\varphi {]}_{\rho }{⋞}_{S}G$ , and (b) $G\in ob$ for all $G\in [\Delta {]}_{\rho }$ ;

• $M,\rho \models \varphi \approx \psi$ iff $[\varphi {]}_{\rho }=[\psi {]}_{\rho }$ ;

• $M,\rho \models A\wedge B$ iff $M,\rho \models A$ and $M,\rho \models B$ ;

• $M,\rho \models A\vee B$ iff $M,\rho \models A$ or $M,\rho \models B$ ;

• $M,\rho \models \neg A$ iff it is not the case that $M,\rho \models A$ ;

• $M,\rho \models \exists xA$ iff $M,\mu \models A$ for some assignment $\mu$ that differs from $\rho$ at most on $x$ .

We then have:

• $M,\rho \models \varphi ⪕\psi$ iff $\left[\varphi {]}_{\rho }{⪕}_S\right[\varphi {]}_{\rho }$ ;

• $M,\rho \models \varphi ⋞\psi$ iff $\left[\varphi {]}_{\rho }{⋞}_S\right[\psi {]}_{\rho }$ .

A formula is said to be G-valid iff it is true in all models relative to all assignments to the variables.

Let G be the axiomatic, Hilbert-style system as defined in Figure 6.

Figure 6 The system G

System G consists of a classical axiomatic basis for the propositional calculus, plus a suitable axiomatic basis to handle the sentential quantifier, plus the following specific axioms:

Factual Equivalence

$\varphi \approx \neg \neg \varphi$

$\varphi \approx \varphi \wedge \varphi$

$\varphi \wedge \psi \approx \psi \wedge \varphi$

$\varphi \wedge (\psi \wedge \chi )\approx (\varphi \wedge \psi )\wedge \chi$

$\varphi \vee \psi \approx \neg (\neg \varphi \wedge \neg \psi )$

$\varphi \vee (\psi \wedge \chi )\approx (\varphi \vee \psi )\wedge (\varphi \vee \chi )$

$(\varphi \approx \psi )\supset (\neg \varphi \approx \neg \psi )$

$(\varphi \approx \psi )\supset (\varphi \wedge \chi \approx \psi \wedge \chi )$

$(\varphi \approx \psi )\wedge (\psi \approx \chi )\supset (\varphi \approx \chi )$

$(\varphi \approx \psi )\supset (\psi \approx \varphi )$

$(\varphi \approx \psi )\supset (\varphi \equiv \psi )$

Substitution

$(\Delta <\varphi \wedge \varphi \approx \psi )\supset \Delta <\psi$

$(\Delta ,\varphi <\chi \wedge \varphi \approx \psi )\supset \Delta ,\psi <\chi$

Structure

$(\Delta ,\varphi <\psi \wedge \Gamma <\varphi )\supset \Delta ,\Gamma <\psi$   Cut

$\neg (\Delta ,\varphi <\varphi )$   Irreflexivity

$\Delta <\varphi \supset \bigwedge \Delta \wedge \varphi$   Factivity

Introduction

$(\Delta <\varphi \wedge \Gamma <\psi )\supset \Delta ,\Gamma <\varphi \wedge \psi$   $\wedge$ -Introduction 1

$\Delta <\varphi \supset \Delta <\varphi \vee \psi$   $\vee$ -Introduction 1

$\Delta <\psi \supset \Delta <\varphi \vee \psi$

$(\varphi \wedge \psi ⋠\varphi \wedge \varphi \wedge \psi ⋠\psi )\supset \varphi ,\psi <\varphi \wedge \psi$   $\wedge$ -Introduction 2

$\varphi \vee \psi ⋠\varphi \supset \varphi <\varphi \vee \psi$   $\vee$ -Introduction 2

$\varphi \vee \psi ⋠\psi \supset \psi <\varphi \vee \psi$

Elimination

$\Delta ,\varphi \wedge \psi <\chi \supset \Delta ,\varphi ,\psi <\chi$   $\wedge$ -Elimination

$\Delta ,\varphi \vee \psi <\chi \supset \Delta ,\varphi <\chi$   $\vee$ -Elimination

$\Delta ,\varphi \vee \psi <\chi \supset \Delta ,\psi <\chi$

Subsumption

$\Delta <\varphi \supset \bigwedge \Delta ⪕\varphi$

Note that whereas the amalgamation principle for $<$ is not expressed by means of an axiom of the system, it is derivable from $\wedge$ -Introduction 1, the first substitution principle and the theorem $\varphi \wedge \varphi \approx \varphi$ . Since the formulas of type $\Delta <\varphi$ are built from finitely many basic formulas, the version of Fine’s cut principle for $<$ in the language of G is derivable from G’s cut axiom. G’s introduction and elimination axioms correspond to the introduction and elimination rules of the same name validated by Fine’s (2012a) semantics.³⁴

The main result of Correia (2010) is that G is sound and complete with respect to the proposed semantics:

Theorem 8 (Soundness and completeness for G). A formula is a theorem of G iff it is G-valid.

Soundness and completeness are preserved if we remove the Factivity axiom from G and keep only condition (a) in the semantic clause for $<$ .

The logic determined by the axioms for factual equivalence is R. B. Angell’s (1977) logic of analytic equivalence. As we will see with some illustrations in Section 4.1, there is room for disagreement about which logic factual equivalence should be taken to have.

Factual equivalence has a distinguished role in system G. Semantically, strict full grounding is definable in terms of fact-disjunction and fact-conjunction, as per the truth-clause for $<$ . This definability is manifest in the object language: where $\underset{\psi \in \Delta }{\bigwedge }\left(\varphi ⋠\psi \right)$ stands for a conjunction of the formulas of type $\neg (\varphi ⋞\psi )$ with $\psi \in \Delta$ (which conjunction exactly does not matter),

$\Delta <\varphi \equiv \bigwedge \Delta \wedge (\bigwedge \Delta ⪕\varphi )\wedge \underset{\psi \in \Delta }{\bigwedge }\left(\varphi ⋠\psi \right)$

is indeed a theorem of G / a G-valid formula. (If $<$ is interpreted as non-factive, just drop the first conjunct.) In Correia (2010), I expressed doubts about the idea that strict full grounding is definable in terms of factual equivalence in that way – more precisely, I expressed doubts about the idea that the Subsumption axiom $\Delta <\varphi \supset \bigwedge \Delta ⪕\varphi$ should be deemed universally true. But I changed my mind since then: see Correia and Skiles (2019) for a defence of the idea.

3.3 Lovett’s ‘The Logic of Ground’

Lovett (2020a) devises a proof system for the logic of (non-factive) weak full grounding that is inspired by Fine’s (2012a) views, and which is closely related to the system G put forward in Correia (2010). Indeed, as Lovett shows, the two systems are ‘definitionally equivalent’, in a sense I will make precise below.

Lovett’s system, LWFG, is a Hilbert-style system formulated in a language that is just like G’s language except that (i) it has no quantifiers and no variables and (ii) its sole non-standard operator is the operator $⩽$ for weak full grounding, which is given the grammar that $<$ has in G. The system is defined as in Figure 7.

Figure 7 The system LWFG

System LWFG consists of a classical axiomatic basis for the propositional calculus, plus the following specific axioms:

Structure

$({\Delta }_1⩽{\varphi }_1\wedge {\Delta }_2⩽{\varphi }_2\wedge \dots \wedge {\varphi }_1,{\varphi }_2,\dots ⩽\varphi )\supset {\Delta }_1,{\Delta }_2,\dots ⩽\varphi$   Cut

$\varphi ⩽\psi \supset (\varphi \supset \psi )$   Implication

Right-Introduction

$\varphi ,\psi ⩽\varphi \wedge \psi$

$\varphi ⩽\varphi \vee \psi$

$\psi ⩽\varphi \vee \psi$

$\neg \varphi ,\neg \psi ⩽\neg (\varphi \vee \psi )$

$\neg \varphi ⩽\neg (\varphi \wedge \psi )$

$\neg \psi ⩽\neg (\varphi \wedge \psi )$

$\varphi ⩽\neg \neg \varphi$

Left-Introduction

$\Delta ,\varphi ,\psi ⩽\chi \supset \Delta ,\varphi \wedge \psi ⩽\chi$

$(\Delta ,\varphi ⩽\chi \wedge \Gamma ,\psi ⩽\chi )\supset \Delta ,\Gamma ,\varphi \vee \psi ⩽\chi$

$\Delta ,\neg \varphi ,\neg \psi ⩽\chi \supset \Delta ,\neg (\varphi \vee \psi )⩽\chi$

$(\Delta ,\neg \varphi ⩽\chi \wedge \Gamma ,\neg \psi ⩽\chi )\supset \Delta ,\Gamma ,\neg (\varphi \wedge \psi )⩽\chi$

$\neg \neg \varphi ⩽\varphi$

Bilateral Introduction

$(\varphi ⩽\psi \wedge \psi ⩽\varphi )\supset \neg \varphi ⩽\neg \psi$

Since $⩽$ -sequents are built from finitely many basic formulas, the cut axiom could be formulated in the same manner as the cut axiom for $<$ in G: $(\Delta ,\varphi ⩽\psi \wedge \Gamma ⩽\varphi )\supset \Delta ,\Gamma ⩽\psi$ . Lovett’s formulation of the bilateral introduction axiom is (in effect) the more complex $(\varphi ⩽\psi \wedge \psi ⩽\varphi )\supset (\neg \varphi ⩽\neg \psi \wedge \neg \psi ⩽\neg \varphi )$ , but the latter formula is derivable from the bilateral introduction axiom as I formulate it. Lovett adds $\varphi ⩽\varphi$ as an axiom to his system, but this is not needed thanks to the cut axiom and axioms $\varphi ⩽\neg \neg \varphi$ and $\neg \neg \varphi ⩽\varphi$ .

Each axiom except for Implication corresponds in an obvious way to a rule of the sort used in the formulation of Fine’s logics, that is, rules that licence derivations of one sequent from a collection of zero or more sequents. One can easily verify that the rules distinct from those that correspond to the second and the fourth Left-Introduction axioms and to the Bilateral Introduction axiom are validated by Fine’s truthmaker semantics (see Section 3.1). The rule corresponding to the Bilateral Introduction axiom is not validated, and the reason is immediate: there are models where two basic sentences have the same verifiers but not the same falsifiers. The rules that correspond to the second and the fourth Left-Introduction axioms are not validated either.³⁵ Take the rule that corresponds to the second Left-Introduction axiom as an illustration. Set $\Delta =\varnothing$ , $\Gamma =\left\{\xi \right\}$ and $\chi =\varphi \vee (\xi \wedge \psi )$ . Both $\varphi ⩽\varphi \vee (\xi \wedge \psi )$ and $\xi ,\psi ⩽\varphi \vee (\xi \wedge \psi )$ are valid (i.e., hold in all models), and so if the Finean semantics validated the rule, $\xi ,\varphi \vee \psi ⩽\varphi \vee (\xi \wedge \psi )$ would also be valid. But it is not.³⁶

These last two rules deserve a bit more discussion. In Fine’s truthmaker semantics, $\wedge$ distributes over $\vee$ in the sense that $\varphi \wedge (\psi \vee \chi )$ and $(\varphi \wedge \psi )\vee (\varphi \wedge \chi )$ have the same verifiers in any model. By contrast, $\vee$ does not distribute over $\wedge$ : whereas every verifier of $\varphi \vee (\psi \wedge \chi )$ is a verifier of $(\varphi \vee \psi )\wedge (\varphi \vee \chi )$ in every model, there are models where some instances of $(\varphi \vee \psi )\wedge (\varphi \vee \chi )$ have verifiers that do not verify the corresponding instances of $\varphi \vee (\psi \wedge \chi )$ .³⁷ Translated in terms of weak full grounding, the situation can thus be summarized as follows:

• Both $\varphi \wedge (\psi \vee \chi )⩽(\varphi \wedge \psi )\vee (\varphi \wedge \chi )$ and its converse $(\varphi \wedge \psi )\vee (\varphi \wedge \chi )⩽\varphi \wedge (\psi \vee \chi )$ are valid (i.e., hold in every model).

• Whereas $\varphi \vee (\psi \wedge \chi )⩽(\varphi \vee \psi )\wedge (\varphi \vee \chi )$ is valid, its converse $(\varphi \vee \psi )\wedge (\varphi \vee \chi )⩽\varphi \vee (\psi \wedge \chi )$ is not.

Now the following can be shown³⁸:

Proposition 9. Let $M$ be a Finean model. All the instances of $(\varphi \vee \psi )\wedge (\varphi \vee \chi )⩽\varphi \vee (\psi \wedge \chi )$ hold in $M$ iff every instance of the rule

$\frac{\Delta ,{\varphi }^{\prime }⩽{\chi }^{\prime }\Gamma ,{\psi }^{\prime }⩽{\chi }^{\prime }}{\Delta ,\Gamma ,{\varphi }^{\prime }\vee {\psi }^{\prime }⩽{\chi }^{\prime }},$

where $\Delta$ and $\Gamma$ are finite, is validated by $M$ , that is, if its premisses hold in $M$ , then so does its conclusion.

Since, as I stressed, $(\varphi \vee \psi )\wedge (\varphi \vee \chi )⩽\varphi \vee (\psi \wedge \chi )$ is not valid in the Finean semantics, it immediately follows that, as previously announced, the rule corresponding to Lovett’s second Left-Introduction is not validated by the semantics. The fact that the rule corresponding to the fourth Left-Introduction is not validated by the semantics can then be easily shown.

Let me now turn to the connection between LWFG and G. In G, fact-disjunction distributes over fact-conjunction as well as vice versa, and so it is natural to suspect that LWFG and G have a lot in common. This is the case, as Lovett shows. In G, the following are theorems (see Correia 2010: 265–6):

• $\varphi ⪕\psi \equiv \left(\right(\varphi \vee \psi )\approx \psi )$

• $\varphi ⋞\psi \equiv \left(\right(\varphi \wedge \psi )⪕\psi )$

This implies that $⪕$ and $⋞$ could have been defined without using quantifiers. Consider now the system pG, formulated in a language just like G’s but without the quantifier and the variables, and axiomatized like G but with the following differences: (i) the postulates for the quantifier are dropped, and, in line with the previous remark, (ii) $\varphi ⪕\psi$ is defined as $(\varphi \vee \psi )\approx \psi$ and $\varphi ⋞\psi$ as $(\varphi \wedge \psi )⪕\psi$ . pG may thus properly be called a propositional version of G. The connection that Lovett establishes is, to be precise, between LWFG and pG.

Assume LWFG and pG are defined on the basis of the same the set of atomic sentences. Define the systems LWFG ${}^{+}$ and pG ${}^{+}$ as follows:

LWFG ${}^{+}$ :

• LWFG ${}^{+}$ ’s language is like LWFG’s except that it has the two extra operators $\approx$ and $<$ with the same grammar as in pG

• The postulates of LWFG ${}^{+}$ are those of LWFG (formulated in LWFG ${}^{+}$ ’s language), plus the following axioms:

  $\varphi \approx \psi \equiv (\varphi ⩽\psi \wedge \psi ⩽\varphi )$
  $\Delta <\varphi \equiv \bigwedge \Delta \wedge (\Delta ⩽\varphi )\wedge \underset{\psi \in \Delta }{\bigwedge }\left(\varphi ⋠\psi \right)$
  where $\underset{\psi \in \Delta }{\bigwedge }\left(\varphi ⋠\psi \right)$ stands for a conjunction of the formulas of type $\neg (\varphi ,\psi ⩽\psi )$ with $\psi \in \Delta$ (exactly which conjunction does not matter)

pG ${}^{+}$ :

• pG ${}^{+}$ ’s language is like pG’s except that it has the extra operator $⩽$ with the same grammar as in LWFG

• The postulates of pG ${}^{+}$ are those of pG (formulated in pG ${}^{+}$ ’s language), plus the following axiom:

  $\Delta ⩽\varphi \equiv \bigwedge \Delta ⪕\varphi$

LWFG ${}^{+}$ is thus naturally seen as a system that defines $\approx$ and $<$ in terms of $⩽$ , and pG ${}^{+}$ as a system that defines $⩽$ in terms of $\approx$ . Lovett establishes, in effect, the following fact:

Theorem 10. LWFG ${}^{+}$ and pG ${}^{+}$ have exactly the same theorems.

This is the sense in which LWFG and pG are definitionally equivalent.

Variants of Lovett’s result can easily be established. If $<$ is understood as non-factive, the Factivity axiom in the formulation of pG is to be dropped; Theorem 10 still holds if the conjunct $\bigwedge \Delta$ is removed from LWFG ${}^{+}$ ’s second extra axiom. Or start with G instead of its propositional version pG, and with the quantified version of LWFG obtained by adding G’s quantificational apparatus (quantifier plus variables plus the relevant postulates) to LWFG. Then Theorem 10 still holds mutatis mutandis. Likewise if G’s Factivity axiom is dropped and the conjunct $\bigwedge \Delta$ is removed from the definitional axiom for $<$ .

3.4 Correia’s ‘A New Semantic Framework for the Logic of Worldly Grounding (and Beyond)’

In Correia (2023), I compare the algebraic semantics of Correia (2010) with the Finean truthmaker semantics as developed in Fine (2012a, 2012b), highlighting what is common to the two semantics as well as what is different. I also argue that each semantics has advantages over the other one, along the following lines (the summary is very rough, the reader should consult the paper for details):

• I argue that it is better to treat negation as a purely linguistic phenomenon, as Fine does, rather than as corresponding to an operation on facts, as I do.

• In my logic, fact-disjunction distributes over fact-conjunction, where-as in Fine’s semantics is does not (see the discussion in the previous section). As I (2016) and Krämer and Roski (2015) independently argued, the distributivity principle conflicts with certain intuitive views about grounding (I will come back to this in Section 4.1). Hence, the Finean semantics score points in this respect.

• In Fine’s semantics, each fact has disjunctive parts which are disjunctively atomic, that is, disjunctive parts that have no proper disjunctive parts, and I argue that this rules out certain coherent views regarding what grounds what. Here it is my algebraic semantics which scores points, since it leaves room for facts without disjunctively atomic disjunctive parts.

• In Fine’s semantics, disjunctive parthood satisfies the principle of Weak Supplementation (if $F$ has a proper disjunctive part $G$ , then it also has a disjunctive part $H$ such that $G$ and $H$ do not disjunctively overlap, that is, such that $G$ and $H$ do not share a disjunctive part), and I argue that this rules out certain coherent views regarding what grounds what. My algebraic semantics scores points once again, since it does not force disjunctive parthood to satisfy Weak Supplementation.

And I finally raise an objection to both semantics – or rather, to Fine’s semantics and to the natural extension of my semantics that accommodates infinite disjunctions of facts: they countenance a disjunctively universal fact in every model, that is, a fact that has all the facts as disjunctive parts, and there are reasons to deny that there are such facts.³⁹

In light of these considerations, I put forward a new, ‘best of both worlds’ semantic framework, one that is in the spirit of what is common to the Finean semantics and my algebraic semantics but which escapes the various criticisms that I have just listed. The basic structures that I invoke are triples $⟨F,⨅,⨆⟩$ , where $F$ (facts) is a non-empty set, and $⨅$ (conjunction) and $⨆$ (disjunction) are (not necessarily total) mappings from subsets of $F$ to $F$ . For some applications – in particular if one wants to semantically characterize factive notions of grounding – one may add an element that specifies which facts of the structure obtain, as in the structures used in Correia (2010). Which conditions conjunction and disjunction should be taken to satisfy in such structures is to a large extent open for discussion, but some conditions seem to impose themselves, such as for instance:

• $⨅$ and $⨆$ are defined on the very same sets of facts

• For all facts $F$ , $⨅$ and $⨆$ are defined on $\left\{F\right\}$ , and $⨅\left\{F\right\}=⨆\left\{F\right\}=F$

Given my purposes in the paper, I focus on structures in which the operations satisfying the conditions just mentioned plus the following conditions on any family $(F_1,F_2,\dots )$ of sets of facts for which the relevant conjunctions / disjunctions exist:

• $⨅\{⨅F_1,⨅F_2,\dots \}=⨅\{F_1\cup F_2\cup \dots \}$   Associativity ( $⨅$ )

• $⨆\{⨆F_1,⨆F_2,\dots \}=⨆\{F_1\cup F_2\cup \dots \}$   Associativity ( $⨆$ )

• $⨅\{⨆F_1,⨆F_2,\dots \}=⨆\{⨅G_a,⨅G_b,\dots \}$

  where $G_a,G_b,\dots$ are all the selections from $\{F_1,F_2,\dots \}$

  Distributivity ( $⨅/⨆$ )

Given a structure $S=⟨F,⨅,⨆⟩$ as initially characterized, disjunctive parthood ( ${⪕}_S$ ), partial disjunctive parthood ( ${⋞}_S$ ), (non-factive) weak full grounding ( ${⩽}_S$ ) and (non-factive) weak partial grounding ( ${\preccurlyeq }_S$ ) are naturally defined as follows:

• $F{⪕}_{S}G$ iff ${}_{\text{df}}$ for some $G\subseteq F$ such that $F\in G$ , $⨆G$ exists and $⨆G=G$

• $F{⋞}_{S}G$ iff ${}_{\text{df}}$ for some $G\subseteq F$ such that $F\in G$ , $⨅G$ exists and $⨅G⪕G$

• $G{⩽}_{S}F$ iff ${}_{\text{df}}⨅G$ exists and $⨅G{⪕}_{S}F$

• $F{\preccurlyeq }_{S}G$ iff ${}_{\text{df}}$ for some $G\subseteq F$ such that $F\in G$ , $G{⩽}_{S}G$

Of course, ${⋞}_S$ and ${\preccurlyeq }_S$ are coextensive. With these relations in place, one can define a relation of (non-factive) strict full grounding ( ${<}_S$ ) in the Fine (2012a/b)-Correia (2010) spirit, either in Finean letter:

• $G{<}_{S}F$ iff ${}_{\text{df}}G{⩽}_{S}F$ and for no $G\in G$ is it the case that $F{\preccurlyeq }_{S}G$

or, equivalently, in Correian letter:

• $G{<}_{S}F$ iff ${}_{\text{df}}⨅G{⪕}_{S}F$ and for no $G\in G$ is it the case that $F{⋞}_{S}G$

It is then obvious how the ground-theoretic languages described in previous sections can be interpreted using the structures under consideration, in line with the Finean treatment of negation: endow each structure with two interpretation functions $[{]}^{+}$ and $[{]}^{-}$ , each function associating a fact of the structure to each atomic sentence of the language, and provide the relevant semantic clause for each operator / quantifier of the language.

In Correia (2023), I semantically characterize three systems in the new framework, two systems for factual equivalence (see footnote 48) and one system for (non-factive) weak full grounding. Let me here I present the latter system. The language of the system is like the Finean language of Section 3.1 except that (i) it has only one ground-theoretic operator, $⩽$ , and sequents of type $\varnothing ⩽\varphi$ are ignored, and (ii) instead of having the standard binary conjunction and disjunction operators, the language has a generalized conjunction operator $\bigwedge$ and a generalized disjunction operator $\bigvee$ , each being able to take a set $\Delta$ of one, two or more basic formulas to make a further basic formula – $\bigwedge \Delta$ or $\bigvee \Delta$ , depending on the case. The models for this language are the models described above in which conjunction and disjunction operate on all and only the non-empty sets of facts. The system is, like PLG and other systems previously discussed, a system for deriving sequents from sets of sequents. Where $\Delta$ is a set of basic formulas, let $\neg \Delta$ be the set of all formulas $\neg \varphi$ for $\varphi \in \Delta$ . The rules of the system – which I will call here ‘ILWFG’ (‘I’ is for ‘infinitary’) – are listed in Figure 8.

Figure 8 Rules for ILWFG

Structure

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

Right-Introduction

$\frac{ }{\Delta ⩽\bigwedge \Delta }$

$\frac{ }{\varphi ⩽\bigvee \Delta }$    $\varphi \in \Delta$

$\frac{ }{\neg \Delta ⩽\neg \bigvee \Delta }$

$\frac{ }{\neg \varphi ⩽\neg \bigwedge \Delta }$    $\varphi \in \Delta$

$\frac{ }{\varphi ⩽\neg \neg \varphi }$

Left-Introduction

$\frac{{\Delta }_1,{\Delta }_2,\dots ⩽\varphi }{\bigwedge {\Delta }_1,\bigwedge {\Delta }_2,\dots ⩽\varphi }$

$\frac{{\Gamma }_a⩽\varphi {\Gamma }_b⩽\varphi \dots }{\bigvee {\Delta }_1,\bigvee {\Delta }_2,\dots ⩽\varphi }$    ${\Gamma }_a,{\Gamma }_b,\dots$ = all the selections from $\{{\Delta }_1,{\Delta }_2,\dots \}$

$\frac{\neg {\Delta }_1,\neg {\Delta }_2,\dots ⩽\varphi }{\neg \bigvee {\Delta }_1,\neg \bigvee {\Delta }_2,\dots ⩽\varphi }$

$\frac{{\Gamma }_a⩽\varphi {\Gamma }_b⩽\varphi \dots }{\neg \bigwedge {\Delta }_1,\neg \bigwedge {\Delta }_2,\dots ⩽\varphi }$    ${\Gamma }_a,{\Gamma }_b,\dots$ = all the selections from $\{\neg {\Delta }_1,\neg {\Delta }_2,\dots \}$

$\frac{ }{\neg \neg \varphi ⩽\varphi }$

Given Cut ( $⩽$ ) and the two rules which feature $\neg \neg$ , the Identity rule (which states that $\varphi ⩽\varphi$ may be inferred no matter what) is derivable. Interestingly, given Cut and the first four Right-Introduction rules, the first four Left-Introduction rules are revertible: for each of these rules, one can prove the premiss(es) starting from the conclusion. Also, given Cut, one can derive the first four Right-Introduction rules if we assume the reversed versions of the first four Left-Introduction rules. This means that one could axiomatize the system using the latter instead of the former.⁴⁰

In Correia (2023), I establish the adequacy of ILWFG with respect to the proposed semantics:

Theorem 11 (Soundness and completeness for ILWFG). A sequent $\sigma$ is derivable from a set of sequents $\Sigma$ in ILWFG iff $\sigma$ holds in every model (of the sort introduced above) in which the members of $\Sigma$ hold.

Fine’s operators of conjunction and disjunction on facts satisfy the conditions imposed on fact-conjunction and fact-disjunction in the proposed semantics. It follows that the proposed system is also sound with respect the Finean semantics – that is, given the appropriate interpretation of the language of the system within that semantics. I do not know whether it is complete.

System ILWFG is importantly different from Lovett’s LWFG. Of course, the language of LWFG has binary conjunction and disjunction rather than the generalized operators of ILWFG’s language, and LWFG’s sequents are all built from finitely many basic sentences. But there is a deeper difference. System LWFG’s axioms correspond to rules that are derivable in ILWFG, except for the rules corresponding to LWFG’s second and fourth Left-Introduction axioms and to its Bilateral Introduction axiom. In this respect, ILWFG sides with the logic determined by Fine’s truthmaker semantics. This is of course not surprising in light of the discussion in Section 3.3, given that (i) the semantics for ILWFG deals with negation in the same way as Fine’s truthmaker semantics does, and (ii) on the semantics for ILWFG as well as on Fine’s semantics, fact-disjunction does not distribute over fact-conjunction in all models.

3.5 Fine’s ‘Guide to Ground’ (Proof-Theoretic Side) and Correia’s ‘An Impure Logic of Representational Grounding’

Consider the introduction rules for strict full grounding listed in Figure 9, which Fine (2012a) puts forward.

Figure 9 Fine’s (2012a) introduction rules for $<$

$\frac{ }{\varphi ,\psi <\varphi \wedge \psi }\frac{ }{\varphi <\varphi \vee \psi }\frac{ }{\psi <\varphi \vee \psi }$

$\frac{ }{\neg \varphi <\neg (\varphi \wedge \psi )}\frac{ }{\neg \psi <\neg (\varphi \wedge \psi )}\frac{ }{\neg \varphi ,\neg \psi <\neg (\varphi \vee \psi )}$

$\frac{ }{\varphi <\neg \neg \varphi }$

As I pointed out in Section 3.1, these rules are at odds with the semantics he develops in the same paper: no sequent of type $\varphi <\varphi \wedge \varphi$ , $\varphi <\varphi \vee \varphi$ , $\neg \varphi <\neg (\varphi \wedge \varphi )$ , $\neg \varphi <\neg (\varphi \vee \varphi )$ or $\varphi <\neg \neg \varphi$ holds in a model. The same is true on all the approaches to the impure logic of grounding previously discussed. What are we to do with these rules?

One option is of course to say that they have to be rejected. But a more plausible view is that they are unproblematic if they are understood as concerning a notion of grounding that is distinct from the notion that Fine’s (2012a) semantics – and the logics in Correia (2010), Lovett (2020a) and Correia (2023), for that matter – aimed to capture. I like to put the contrast between the two notions as a contrast between worldly notions and representational notions of grounding. Roughly put, a notion of grounding is worldly if it is sensitive only to how the world is and not to factors that merely have to do with how the world is represented; and a notion of grounding is representational if, by contrast, it is sensitive to merely representational factors (see Correia 2020; I will elaborate on the distinction in Section 4.1). The difference between, say, any instance of $\varphi$ and the corresponding instance of $\varphi \wedge \varphi$ is purely representational: both sentences, if they represent the world as being some way, represent it as being the same way. Or so it is plausible to claim. If this is correct, then granted that $<$ expresses a worldly notion of grounding and that it is irreflexive, no sequent of type $\varphi <\varphi \wedge \varphi$ can be true. By contrast, if $<$ expresses a representational notion, then it may well be that some, or even all, sequents of type $\varphi <\varphi \wedge \varphi$ are true. The view I am suggesting is that the introduction rules above are suited for some representational notion(s) of strict full grounding.

In addition to these introduction rules, Fine (2012a) lays down elimination rules. One of them has a form we are already familiar with, but the other ones have (except in degenerate cases) disjunctive conclusions. These rules have the following general form, where $\Sigma$ , $T_1$ , $T_2$ , $\dots$ are sets of sequents:

$\frac{\Sigma }{T_1|T_2|\dots }$

Such a rule ‘says’ that from the assumption that all the sequents in $\Sigma$ hold, one may infer that all the sequents in some $T_i$ hold. We may take rules of the form

$\frac{\Sigma }{T}$

to be of the previous form but with only one disjunct in the conclusion. On that account, the rules we have been dealing with previously can be seen as rules of the above general form but with only one disjunct in the conclusion, this disjunct being a singleton. The elimination rules proposed by Fine are as displayed in Figure 10, where the pairs $⟨{\Delta }_{\varphi }^1,{\Delta }_{\psi }^1⟩$ , $⟨{\Delta }_{\varphi }^2,{\Delta }_{\psi }^2⟩$ , $\dots$ are all the pairs $⟨{\Delta }_a,{\Delta }_b⟩$ such that ${\Delta }_a\cup {\Delta }_b=\Delta$ .

Figure 10 Fine’s (2012a) elimination rules for $<$

$\frac{\Delta <\varphi \wedge \psi }{{\Delta }_{\varphi }^1⩽\varphi {\Delta }_{\psi }^1⩽\psi |{\Delta }_{\varphi }^2⩽\varphi {\Delta }_{\psi }^2⩽\psi |\dots }$

$\frac{\Delta <\varphi \vee \psi }{\Delta ⩽\varphi |\Delta ⩽\psi |\Delta <\varphi \wedge \psi }$

$\frac{\Delta <\neg (\varphi \wedge \psi )}{\Delta ⩽\neg \varphi |\Delta ⩽\neg \psi |\Delta <\neg (\varphi \vee \psi )}$

$\frac{\Delta <\neg (\varphi \vee \psi )}{{\Delta }_{\varphi }^1⩽\neg \varphi {\Delta }_{\psi }^1⩽\neg \psi |{\Delta }_{\varphi }^2⩽\neg \varphi {\Delta }_{\psi }^2⩽\neg \psi |\dots }$

$\frac{\Delta <\neg \neg \varphi }{\Delta ⩽\varphi }$

In Correia (2017), I set myself the task of devising a system which comprises the Finean introduction and elimination rules that I have just presented and of devising a semantics relative to which the system is sound and complete. The language of the system is a sequent language with the following types of sequents, where $\Delta$ is a set of basic sentences and $\varphi$ a basic sentence:

• $\Delta <\varphi$

• $\Delta ⩽\varphi$

• $\Delta \approx \varphi$

• $\Delta \nless \varphi$

• $\Delta ⪇\varphi$

• $\Delta \not\approx \varphi$

$<$ is intended to express a non-factive notion of strict full grounding, $⩽$ a non-factive notion of weak full grounding, and $\approx$ a notion of propositional equivalence. (I use ‘propositional equivalence’ rather than ‘factual equivalence’ in order to emphasize the representational character of the ground-theoretic notions involved in the system.) The intended meanings of the other three operators are the obvious ones. The syntax of $\approx$ is significantly different from the one it had in the language of system G (see Section 3.2). $\Delta \approx \varphi$ is intended to mean that ( $\Delta$ is non-empty and) all the members of $\Delta$ are propositionally equivalent to $\varphi$ . The rules of the system – that I will call ‘ILFG’, for ‘impure logic of full grounding’ – are as displayed in Figure 11.

Figure 11 Rules for ILFG

Structural rules for $\approx$

$\frac{ }{\varphi \approx \varphi }$    $\frac{\varphi \approx \psi }{\psi \approx \varphi }$    $\frac{\varphi \approx \psi \psi \approx \chi }{\varphi \approx \chi }$

$\frac{{\varphi }_1\approx \varphi {\varphi }_2\approx \varphi \dots }{{\varphi }_1,{\varphi }_2,\dots \approx \varphi }$    $\frac{\varphi ,\Delta \approx \psi }{\varphi \approx \psi }$    $\frac{\varnothing \approx \varphi }{\perp }$

Introduction rules for $\approx$

$\frac{ }{\varphi \wedge \psi \approx \psi \wedge \varphi }$    $\frac{ }{\varphi \vee \psi \approx \psi \vee \varphi }$

$\frac{\varphi \approx \psi }{\varphi \wedge \theta \approx \psi \wedge \theta }$    $\frac{\varphi \approx \psi }{\varphi \vee \theta \approx \psi \vee \theta }$    $\frac{\varphi \approx \psi }{\neg \varphi \approx \neg \psi }$

Elimination rules for $\approx$

$\frac{\psi \approx \varphi \wedge \chi }{\perp }$    where $\psi$ is non-conjunctive

$\frac{\psi \approx \varphi \vee \chi }{\perp }$    where $\psi$ is non-disjunctive

$\frac{\psi \approx \neg \varphi }{\perp }$    where $\psi$ is non-negative

$\frac{\varphi \wedge \psi \approx {\varphi }^{\prime }\wedge {\psi }^{\prime }}{\varphi \approx {\varphi }^{\prime }\psi \approx {\psi }^{\prime }|\varphi \approx {\psi }^{\prime }\psi \approx {\varphi }^{\prime }}$

$\frac{\varphi \vee \psi \approx {\varphi }^{\prime }\vee {\psi }^{\prime }}{\varphi \approx {\varphi }^{\prime }\psi \approx {\psi }^{\prime }|\varphi \approx {\psi }^{\prime }\psi \approx {\varphi }^{\prime }}$

$\frac{\neg \varphi \approx \neg \psi }{\varphi \approx \psi }$

Structural rules for $<$

$\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 ( $<$ )

$\frac{\Delta <\varphi \varphi \approx \psi }{\Delta <\psi }$

$\frac{{\varphi }_1,{\varphi }_2,\dots <\psi {\psi }_1\approx {\varphi }_1{\psi }_2\approx {\varphi }_2\dots }{{\psi }_1,{\psi }_2,\dots <\psi }$

Definitive rules for $⩽$

$\frac{\Delta \approx \varphi }{\Delta ⩽\varphi }$    $\frac{\Delta <\varphi }{\Delta ⩽\varphi }$    $\frac{{\Delta }_1\approx \varphi {\Delta }_2<\varphi }{{\Delta }_1,{\Delta }_2⩽\varphi }$

$\frac{\Delta ⩽\varphi }{\Delta \approx \varphi |\Delta <\varphi |{\Delta }_{\approx }^1\approx \varphi {\Delta }_{<}^1<\varphi |{\Delta }_{\approx }^2\approx \varphi {\Delta }_{<}^2<\varphi |\dots }$

where the pairs $⟨{\Delta }_{\approx }^1,{\Delta }_{<}^1⟩$ , $⟨{\Delta }_{\approx }^2,{\Delta }_{<}^2⟩$ , $\dots$ are all the pairs $⟨{\Delta }_a,{\Delta }_b⟩$ such that ${\Delta }_a\cup {\Delta }_b=\Delta$

Introduction rules for $<$

See Figure 9

Elimination rules for $<$

See Figure 10

Complexity rule

$\frac{\Delta <\varphi }{\perp }$    where $\varphi$ is a literal and some member of $\Delta$ is not

Non-Contradiction and Excluded Middle

$\frac{\Delta \approx \varphi \Delta \not\approx \varphi }{\perp }$    $\frac{\Delta <\varphi \Delta \nless \varphi }{\perp }$    $\frac{\Delta ⩽\varphi \Delta ⪇\varphi }{\perp }$

$\frac{ }{\Delta \approx \varphi |\Delta \not\approx \varphi }$    $\frac{ }{\Delta <\varphi |\Delta \nless \varphi }$    $\frac{ }{\Delta ⩽\varphi |\Delta ⪇\varphi }$

The definitive rules for $⩽$ state, in effect, that $⩽$ is definable in terms of $<$ and $\approx$ , along the following lines: $\Delta ⩽\varphi$ iff ${}_{\text{df}}\Delta \approx \varphi$ or $\Delta <\varphi$ or ${\Delta }_1\approx \varphi$ and ${\Delta }_2<\varphi$ for some ${\Delta }_1$ , ${\Delta }_2$ such that ${\Delta }_1\cup {\Delta }_2=\Delta$ .

Due to the peculiar shape of some of the rules, viz. the ones with disjunctive conclusions, the notion of derivability cannot be defined in the same way as in Section 3.1. Let us represent the disjunctive item $T_1|T_2|\dots$ by the set $\{T_1,T_2,\dots \}$ , and call such sets requirements. The relevant notion of derivability is that of a requirement being derivable from a set of sequents. A requirement $R$ generates a requirement $S$ iff every member of $R$ contains (as a subset) some member of $S$ . We say that $\{T_1,T_2,\dots \}$ is derivable from $\Sigma$ iff there is a proof of a requirement that generates $\{T_1,T_2,\dots \}$ from a subset of $\Sigma$ . A proof of a requirement $\{T_1,T_2,\dots \}$ from a set of sequents $\Sigma$ is a labelled tree without infinite branches with top $\{T_1,T_2,\dots \}$ and bottom $\Sigma$ , such that each transition from the occupant of a parent node to the occupants of the corresponding children is licensed by one or more (possibly infinitely many) applications of a given rule (see Correia 2017 for a precise definition).⁴¹

The semantics is of the same general spirit as deRosset’s (2015) and Litland’s (2018a) graph-theoretic semantics: each model specifies in a somewhat direct way links of strict full grounding between contents – which I call ‘propositions’ rather than ‘facts’. But there is a big difference: the semantics identifies a set of ‘simple’ propositions, and it initially only specifies what grounds these propositions – what grounds the other propositions being then defined recursively on that basis. Let me be more precise.

Let a propositional structure be a tuple $⟨P,\sqcap ,\bigsqcup ,-⟩$ where $P$ (propositions) is a non-empty set, $\sqcap$ (conjunction) and $\bigsqcup$ (disjunction) are binary operations on $P$ , and $-$ (negation) is a unary operation on $P$ . A proposition in a propositional structure is

• negative iff it is the negation of some proposition

• conjunctive iff it is the conjunction of a pair of propositions

• disjunctive iff it is the disjunction of a pair of propositions

• atomic iff it is neither conjunctive, nor disjunctive, nor negative

• simple iff it is atomic or the negation of an atomic proposition

A propositional structure $⟨P,\sqcap ,\bigsqcup ,-⟩$ is representational iff the following conditions are satisfied:

• Being negative, being conjunctive and being disjunctive are pairwise incompatible properties of propositions

• $\sqcap$ and $\bigsqcup$ are commutative

• If $P\sqcap Q=P^{\prime }\sqcap Q^{\prime }$ , then either $P=P^{\prime }$ and $Q=Q^{\prime }$ or $P=Q^{\prime }$ and $Q=P^{\prime }$

• If $P\bigsqcup Q=P^{\prime }\bigsqcup Q^{\prime }$ , then either $P=P^{\prime }$ and $Q=Q^{\prime }$ or $P=Q^{\prime }$ and $Q=P^{\prime }$

• If $-P=-Q$ , then $P=Q$

And it is regular iff it is representational and its set of propositions is generated by the set of its atomic propositions via $\sqcap$ , $\bigsqcup$ , and $-$ .

Let a ground-theoretic structure be a tuple $S=⟨P,\sqcap ,\bigsqcup ,-,{<}^0⟩$ , where $⟨P,\sqcap ,\bigsqcup ,-⟩$ is a regular propositional structure and ${<}^0$ (strict full grounding) is a relation between sets of propositions and simple propositions that satisfies the following conditions:

• If $P_1{<}^0{P}_1,P_2{<}^0{p}_2,\dots$ and $P_1,P_2,\dots ,P{<}^{0}Q$ , then $P_1,P_2,\dots ,P{<}^{0}Q$    Cut

• If $P{<}^{0}P$ , then $P\notin P$    Irreflexivity

• If $P_1{<}^{0}P$ , $P_2{<}^{0}P$ , $\dots$ , then $P_1,P_2,\dots {<}^{0}P$   Amalgamation

• If $P{<}^{0}P$ , then all the members of $P$ are simple  Complexity

A weak companion ${⩽}^0$ of ${<}^0$ is defined as follows:

• $P{⩽}^{0}P$ iff ${}_{\text{df}}P=\left\{P\right\}$ , or $P{<}^{0}P$ , or for some $P^{\prime }$ such that $P=\left\{P\right\}\cup P^{\prime }$ , $P^{\prime }{<}^{0}P$

The propositions in a regular propositional structure are very similar to the formulas of a classical propositional language, and can be assigned degrees of complexity in just the same ways. This makes it possible to recursively extend ${<}^0$ and ${⩽}^0$ to relations ${<}^{\omega }$ and ${⩽}^{\omega }$ between sets of propositions and arbitrary propositions. I skip the details but nevertheless mention that ${<}^{\omega }$ , just like ${<}^0$ , satisfies Cut, Irreflexivity and Amalgamation, and that the following principles hold:

• $P{⩽}^{\omega }P$ iff $P=\left\{P\right\}$ , or $P{<}^{\omega }P$ , or for some $P^{\prime }$ such that $P=\left\{P\right\}\cup P^{\prime }$ , $P^{\prime }{<}^{\omega }P$

• $P{<}^{\omega }P\sqcap Q$ iff for some $P_1$ , $P_2$ with $P=P_1\cup P_2$ , $P_1{⩽}^{\omega }P$ and $P_2{⩽}^{\omega }Q$

• $P{<}^{\omega }P\bigsqcup Q$ iff $P{⩽}^{\omega }P$ or $P{⩽}^{\omega }Q$ or $P{<}^{\omega }P\sqcap Q$

• $P{<}^{\omega }-(P\sqcap Q)$ iff $P{⩽}^{\omega }-P$ or $P{⩽}^{\omega }-Q$ or $P{<}^{\omega }-(P\bigsqcup Q)$

• $P{<}^{\omega }-(P\bigsqcup Q)$ iff for some $P_1$ , $P_2$ with $P=P_1\cup P_2$ , $P_1{⩽}^{\omega }-P$ and $P_2{⩽}^{\omega }-Q$

• $P{<}^{\omega }--P$ iff $P{⩽}^{\omega }P$

Let a ground-theoretic model be a ground-theoretic structure endowed with an interpretation function, which assigns an atomic proposition of the structure to each atomic sentence of the language. Given a ground-theoretic model $M$ with interpretation function $\left[\right]$ , $\left[\right]$ is extended to all basic sentences of the language in the obvious way (put $[\varphi \wedge \psi ]=\left[\varphi \right]\sqcap \left[\psi \right]$ and so on), and where ${<}^{\omega }$ and ${⩽}^{\omega }$ are the extended strict and weak grounding relation of the underlying structure, respectively, we put:

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

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

• $\Delta \approx \varphi$ holds in $M$ iff $\left[\Delta \right]=\left[\varphi \right]$

• $\Delta \nless \varphi$ holds in $M$ iff $\Delta <\varphi$ does not hold in $M$

• $\Delta ⪇\varphi$ holds in $M$ iff $\Delta ⩽\varphi$ does not hold in $M$

• $\Delta \not\approx \varphi$ holds in $M$ iff $\Delta \approx \varphi$ does not hold in $M$

A requirement $\{T_1,T_2,\dots \}$ is an ILFG-consequence of a set of sequents $\Sigma$ iff for every ground-theoretic model $M$ in which all the members of $\Sigma$ hold, there is an $i$ such that all the members of $T_i$ hold in $M$ .

In the paper, I establish the adequacy of ILFG with respect to the proposed semantics:

Theorem 12 (Soundness and completeness for ILFG). A requirement $\{T_1,T_2,\dots \}$ is derivable from a set of sequents $\Sigma$ in ILFG iff $\{T_1,T_2,\dots \}$ is an ILFG-consequence of $\Sigma$ .

Propositional equivalence as characterized by ILFG is very fine grained, perhaps too fine-grained even for many friends of representational grounding. Another likely target of criticism is the complexity rule, at least if the rule is intended to concern a notion of metaphysical grounding. In the paper, I am explicit that $<$ is intended to express such a notion, and I try to defend the complexity rule against objections; but the defence may not convince every sceptic. The rule bears some resemblance to Bolzano’s principle that grounded truths cannot be less complex than their grounds (1837: II, § 221). Bolzano states this principle for what he calls ‘conceptual truths’. Some might wish to argue that my complexity rule is likewise to be restricted to certain kinds of ground-theoretic connections, say to connections of logical grounding.

3.6 deRosset and Fine’s ‘A Semantics for the Impure Logic of Ground’

Impure logic of full grounding embodies a definite conception of propositional equivalence – as I have just stressed, one that is very fine-grained. This contrasts with deRosset and Fine’s (2023) impure logic of grounding: the logic is intended to be a ‘minimal’ logic, that can be enriched in various ways so as to capture various conceptions of propositional equivalence, all quite fine-grained but to various degrees.

Their minimal system, which they call ‘GG’, is roughly Fine’s (2012b) pure logic of grounding PLG (see Figure 1) plus the introduction and elimination rules put forward in Fine (2012a) and appearing in ILFG (see Figures 9 and 10). The qualification ‘roughly’ is important because there are subtle yet important differences between this description of GG and a properly accurate description of the system. Let me be more precise.

The following two points mark important formal differences between GG on one hand, and PLG and ILFG on the other hand:

1. (1) In PLG, derivability is of a sequent from a set of sequents. Since some elimination rules for $<$ involve disjunctive conclusions, enriching PLG with these rules forces one to invoke a different kind of derivability relation. In ILFG, derivability is of a requirement from a set of sequent, where requirements behave like disjunctions of conjunctions: a requirement $\{T_1,T_2,\dots \}$ holds just in case for some $i$ , all the members of $T_i$ hold. GG’s derivability relation could be taken to be of the same sort, but deRosset and Fine adopt a slightly simpler option and take the derivability relation of be a relation between two sets of sequents, where one is treated conjunctively, as in PLG and ILFG, and the other one disjunctively: the semantic counterpart of the claim that set of sequents $T$ is derivable from set of sequents $\Sigma$ is the claim that whenever all the members of $\Sigma$ hold, at least one member of $T$ holds. Adopting their approach instead of the approach I adopted in the formulation of ILFG involves no loss (or gain): any principle to the effect that a requirement $\{T_1,T_2,\dots \}$ follows from a set of sequents $\Sigma$ can be replaced without loss (or gain) by the principle that for any selection $T$ from $\{T_1,T_2,\dots \}$ , $T$ follows from $\Sigma$ . (And conversely, the deRosset and Fine derivability relation could be used instead of the one I used in order to characterize ILFG, without any loss or gain.)

2. (2) Instead of defining derivability in terms of proofs of a set of sequents from a set of sequents (which would be to follow the pattern exemplified in PLG and ILFG), deRosset and Fine introduce a new symbol $⊩$ for derivability and devise a system of rules for deriving expressions of type $\Sigma ⊩T$  – read: set of sequent $T$ is derivable from set of sequents $\Sigma$  – from (possibly empty) sets of such expressions. The formulation of the system thus involves a meta-notion of derivability which is of the same formal kind as the notion of derivability at work in PLG: in both cases, derivability is always of one item from a set of items of the same sort, and it is defined in terms of rules with 0 or more premisses and just one conclusion.

The language in which the sequents of GG are formulated is the same as the language of the impure logic of Fine (2021a) (see Section 3.1), except that each sequent is built from only finitely many basic formulas. Likewise, in a derivability statement $\Sigma ⊩T$ , $\Sigma$ and $T$ are required to be finite. As they stress at the end of the paper, these restrictions can be dropped modulo minor modifications of the system and its semantics.

The rules of GG are divided into two categories, the structural and the non-structural. The structural rules are those listed in Figure 12. The non-structural rules in turn divide into two categories, the pure and the impure. Where

Figure 12 Structural rules for GG

$\frac{ }{\sigma ⊩\sigma }$	Identity
$\frac{\Sigma ⊩T}{\Sigma ,{\Sigma }^{\prime }⊩T,T^{\prime }}$	Thinning
$\frac{\sigma ,\Sigma ⊩T{\Sigma }^{\prime }⊩T^{\prime },\sigma }{\Sigma ,{\Sigma }^{\prime }⊩T,T^{\prime }}$	Snip

$\frac{\Sigma }{\sigma }$

is a rule with $\Sigma$ a set of sequents and $\sigma$ a sequent, let its $⊩$ -transform be the rule

$\frac{ }{\Sigma ⊩\sigma }$

GG’s pure non-structural rules are the rule

$\frac{ }{\varphi ⪯\psi ⊩\{\varphi \prec \psi ,\psi ⪯\varphi \}}\text{Irreversibility}$

plus the $⊩$ -transforms of all the rules of PLG (formulated in GG’s language) except for the transitivity rule

$\frac{\varphi \prec \psi \psi \preccurlyeq \chi }{\varphi \prec \chi }$

(The latter can be obtained from the rest of the system.) GG’s impure non-structural rules include the $⊩$ -transforms of Fine’s (2012a) introduction rules (see Figure 9) and the $⊩$ -transform of Fine’s (2012a) $\neg \neg$ -elimination rule (see Figure 10). The remaining impure rules correspond to Fine’s (2012a) elimination rules with disjunctive conclusions (see again Figure 10). In conformity with the approach to derivability as a relation between two sets of sequents rather than between a requirement and a set of sequents (see point (1) above), corresponding to each of these elimination rules

$\frac{\Sigma }{T_1|T_2|\dots }$

GG contains all the rules

$\frac{ }{\Sigma ⊩T}$

where $T$ is a selection from $\{T_1,T_2,\dots \}$ .

A statement of type $\Sigma ⊩T$ may then be said to be derivable from a set of such statements iff the former can be obtained from the latter by means of the rules just laid down (which can in turn be made precise in various ways, see the characterization of derivability in PLG). We will say that a set of sequents $T$ follows in GG from a set of sequents $\Sigma$ iff for some (finite) ${\Sigma }^{\prime }\subseteq \Sigma$ and $T^{\prime }\subseteq T$ , ${\Sigma }^{\prime }⊩T^{\prime }$ is derivable from the empty set.

The basic structures invoked in the semantics are selection systems. A selection system is a tuple $⟨F,⨅,⨆⟩$ , where $F$ (conditions) is a non-empty set and $⨅$ (combination) and $⨆$ (choice) are two mappings that take finite (possibly empty) sequences of pairs of elements of $F$ into elements of $F$ , such that $⨅⟨v⟩=⨆⟨v⟩$ for any pair $v$ of elements of $F$ .⁴² Pairs of conditions in selection systems are called contents, and they indeed play the role of semantic values of (basic) sentences (see below).

deRosset and Fine give an informal interpretation of the operations of a selection system in terms of menus. Very roughly, on that interpretation, the combination operation generates conjunctive menus like a menu that would feature only ‘bacon and eggs’ (a strange kind of menu which offers no choice) and the choice operation generates disjunctive menus like a menu that would feature only ‘bacon or eggs’ (a standard kind of menu, which does offer a choice). But there is another interpretation which is fully justified by the semantic treatment of object language conjunction and disjunction (see below), and which motivated my use of the symbol $⨅$ for combination and of $⨆$ for choice (deRosset and Fine use significantly different symbols): combination and choice are at bottom mappings of conjunction and disjunction, respectively. Seen that way, selection systems are thus in some important ways similar to the structures I invoke in Correia (2023): they take a mapping of conjunction and a mapping of disjunction as sui generis mappings on semantic values of sentences. A big difference, though, is that whereas I took the mappings to be mappings from sets of unanalysed objects to unanalysed objects of the same sort (facts), deRosset and Fine take them to be mappings from sequences of pairs of unanalysed objects to unanalysed objects of the same sort (conditions).

Each selection system $S=⟨F,⨅,⨆⟩$ comes with a relation ${\ll }_S$ of immediate selection between sets of contents and conditions. It is defined as follows (where $S$ is a set of contents and $F\in F$ ):

• $S{\ll }_{S}F$ iff ${}_{\text{df}}$

  1. – either there is a sequence of contents $Z$ such that $F=⨅Z$ and $S$ and $Z$ have the same members

  2. – or there is a sequence of contents $Z$ such that $F=⨆Z$ and $S=\left\{v\right\}$ for some $v\in Z$

(Despite the ‘either-or’ phrasing, the disjunction is intended to be inclusive.) The relation ${<}_S$ of strict selection is defined as the smallest relation $⊳$ between sets of contents and contents that satisfies the following conditions, where $S{⊳}^{*}v$ iff ${}_{\text{df}}$ for some $F\in F$ , $S⊳⟨⨅⟨v⟩,F⟩$ :

• If $S{\ll }_{S}F$ , then $S⊳⟨f,G⟩$   Basis

• If $S⊳v$ , then $S⊳⟨⨅⟨v⟩,F⟩$   Ascent

• If $S_1{⊳}^{*}{v}_1$ , …, $S_n{⊳}^{*}{v}_n$ and $v_1,\dots ,v_n⊳v$ ,  then $S_1,\dots ,S_n⊳v$   Lower Cut

• If $S_1⊳v_1$ , …, $S_n⊳v_n$ and $v_1,\dots ,v_n{⊳}^{*}v$ ,  then $S_1,\dots ,S_n⊳v$   Upper Cut

The corresponding starred relation, the relation of weak selection of the selection system, is denoted by ${⩽}_S$ . Partial notions are then defined as follows: $v{⪯}_{S}w$ iff ${}_{\text{df}}$ for some set of contents $S$ with $v\in S$ , $S{⩽}_{S}w$ ; $v{\prec }_{S}w$ iff ${}_{\text{df}}v{⪯}_{S}w$ but not $w{⪯}_{S}v$ .

The selection systems that are invoked to interpret the language of GG are selection systems that satisfy two further conditions⁴³:

• If $S{<}_{S}v$ iff $S{⩽}_{S}v$ and for no $w\in S$ is it  the case that $v{⪯}_{S}w$   Irreversibility

• If $S{<}_S⟨⨅⟨v_1,\dots ,v_n⟩,F⟩$ , then for some covering $\{S_1$ , $\dots$ ., $S_n\}$ of $S$ , $S_i{⩽}_S{v}_i$ for each $i$

• If $S{<}_S⟨⨆⟨v_1,\dots ,v_n⟩,F⟩$ , then for some non-empty subset $\{w_1,\dots ,w_k\}$ of members of $\{v_1,\dots ,v_n\}$ and some  covering $\{S_1$ , $\dots$ ., $S_k\}$ of $S$ , $S_i{⩽}_S{w}_i$ for each $i$   Maximality

We call them selection frames. A selection model is a selection frame endowed with an interpretation function that takes each atomic sentence into a content of the selection frame. Given a selection model $M=⟨F,⨅,⨆,\left[\right]⟩$ , the interpretation function $\left[\right]$ is extended to all basic sentences of the language via the following clauses:

• $\left[\neg \varphi \right]=⟨G,⨅⟨\left[\varphi \right]⟩⟩$ where $\left[\varphi \right]=⟨f,G⟩$

• $[\varphi \wedge \psi ]=⟨⨅⟨\left[\varphi \right],\left[\psi \right]⟩,⨆⟨\left[\neg \varphi \right],\left[\neg \psi \right]⟩⟩$

• $[\varphi \vee \psi ]=⟨⨆⟨\left[\varphi \right],\left[\psi \right]⟩,⨅⟨\left[\neg \varphi \right],\left[\neg \psi \right]⟩⟩$

Where $F=⟨F,⨅,⨆⟩$ , the semantic clauses for the sequents of the language are then, unsurprisingly:

• $\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 set of sequents $T$ is said to be a GG-consequence of a set of sequents $\Sigma$ iff for every model $M$ in which all the members of $\Sigma$ hold, some member of $T$ holds in $M$ .

deRosset and Fine establish that GG is sound and complete with respect to the proposed semantics:

Theorem 13 (Soundness and completeness for GG). For all sets of sequents $\Sigma$ and $T$ , $T$ follows in GG from $\Sigma$ iff $T$ is a GG-consequence of $\Sigma$ .

deRosset and Fine’s logic of grounding is subject to an objection somewhat akin to the second objection against ILFG mentioned at the end of Section 3.5. The immediate selection relation ${\ll }_S$ of a selection system $S$ only takes as ‘right-hand side’ relata items that are combinations or choices. As a consequence, a strict full grounding sequent $\Delta <\varphi$ holds in a selection model only if in that model, $\varphi$ expresses a content of type $⟨F,G⟩$ where $F$ is a combination or a choice. Now consider a ‘real life’ sentence of strict full grounding such as ‘the fact that Socrates exists metaphysically grounds the fact that $\{$ Socrates $\}$ exists’, and assume it is true. Suppose we want to build a selection model in which the sentence, understood as a sequent of type $\varphi <\psi$ , holds. Then by the previous remark, we will have to treat the sentence ‘ $\{$ Socrates $\}$ exists’ as expressing a content whose first element is a combination or a choice. But a combination or a choice of what? If the sentence were conjunctive or disjunctive, for instance, then there would be a natural answer. But the sentence does not have any logical complexity (or so am I assuming for the sake of the argument), and therefore, it would seem, the only models that we can come up with will be artificial models, models that do not faithfully represent the real content of the sentence. The objection, stated in a nutshell, is that the proposed semantics cannot be applied in a non-artificial way to all sentences that express links of strict full metaphysical grounding.

3.7 Further Works

Other studies on the logic of grounding would deserve to be duly presented, but for lack of space I offer here only a brief survey. I would classify all the studies mentioned below as representational (in the sense introduced on page 47). With the exception of Poggiolesi’s (2016, 2018) work, they all target a notion of strict full grounding that obey the Finean introduction rules (see Figure 9) or a partial notion that obeys the rules for partial strict grounding (i.e., the relation Fine symbolizes by ${\prec }^{*}$ , see page 8) that can be derived from them.

Batchelor (2010) and Schnieder (2011) are two very early works on the logic of grounding. Batchelor starts with a theory of a relation $I$ of immediate partial grounding and defines a relation $G$ of partial grounding as the ancestral of $I$ . He then takes a fact $F$ to be strictly fully grounded in some facts iff (i) the latter facts are all partial grounds, in the sense of $G$ , of $F$ and (ii) they together necessarily imply $F$ . Schnieder focuses exclusively on partial strict grounding. He gives an axiomatic proof system for the notion and establishes its consistency.

Korbmacher (2018a, 2018b) also focuses exclusively on partial strict grounding. In Korbmacher (2018a), he introduces and develops an axiomatic theory of (type-free) truth and partial strict grounding based on an axiomatic theory of Peano arithmetic, in the spirit of the axiomatic theories of truth discussed in Halbach (2011). In Korbmacher (2018b), he studies an extension of the previous theory with a Tarski-style hierarchy of typed truth predicates.

In Correia (2014), I offer a tree-theoretic characterization of logical grounding and use that notion (i) to characterize well-known consequence relations, among them classical consequence and the consequence relation corresponding to Anderson and Belnap’s (1962, 1963) first-degree entailments (FDEs), and (ii) to formulate a ground-theoretic version of (part of) Kripke’s (1975) celebrated theory of truth. In Correia (2015), I develop further the study of the connections between logical grounding and FDEs: I axiomatize the logic of FDEs understood as multiple-conclusion sequents and then show that various notions of logical grounding can be axiomatized by modifying in very simple ways the system for FDEs.

Poggiolesi, (2016, 2018) also focuses on logical grounding, but her target notion is a peculiar notion of logical grounding she dubs ‘complete immediate grounding’. The notion can be grasped by means of a couple of examples: the complete immediate ground of a conjunctive truth $\varphi \wedge \psi$ is the plurality of truths $\varphi$ , $\psi$ ; by contrast, the complete immediate ground of a disjunctive truth $\varphi \vee \psi$ is not always the same – it is $\varphi$ if $\psi$ is false, $\psi$ if $\varphi$ is false, and the plurality $\varphi$ , $\psi$ if none is false. In order to take this sort of variability into account, Poggiolesi takes complete immediate grounding to be a ternary relation linking a groundee, its complete immediate ground and an extra relatum intended to specify under which condition the link of complete immediate grounding holds. More precisely, her basic notion is that of a multiset of formulas $\Delta$ grounding a formula $\varphi$ under the condition that a formula $\psi$ holds.

Krämer’s (2018) starting point is Fine’s truthmaker semantics, but he enriches the conceptual framework with the idea of modes of verification: the new idea is that of a verifier verifying a proposition by verifying other propositions. Disjunctive propositions provide straightforward illustrations of this idea: any verifier of $P$ ( $Q$ ) verifies $P\vee Q$ by verifying $P$ ( $Q$ ). Krämer actually works with two types of propositions, ‘unilateral’ propositions and ‘bilateral’ propositions. Krämer identifies unilateral propositions with sets of modes of verification, and bilateral propositions with pairs of such sets, where the first member of such a pair (its ‘positive’ component) corresponds to the ways of verifying the proposition and the second member (its ‘negative’ component) to the ways of falsifying it. He accordingly introduces two types of grounding relations, those which relate unilateral propositions and those which relate bilateral propositions. On his account, unilateral propositions $P_1$ , $\dots$ , $P_n$ strictly ground unilateral proposition $P$ just in case (i) there is such a thing as the mode of verifying ‘by verifying $P_1$ , $\dots$ , $P_n$ ’ and (ii) this mode is a member of $P$ . Grounding between bilateral propositions is simply defined by ‘focusing on positive components’: for instance, Krämer takes $⟨P_1,Q_1⟩$ , $\dots$ , $⟨P_n,Q_n⟩$ to strictly ground $⟨P,Q⟩$ just in case $P_1$ , $\dots$ , $P_n$ strictly ground $P$ .

In Correia (2021b), I present a logic (semantics + adequate proof system) for relative fundamentality – more precisely, for the notion of being more fundamental than, or as fundamental as – as well as a modal extension of that logic. I then suggest a definition of strict full grounding in terms of necessity and relative fundamentality, and I investigate the logical properties of the notion given this definition and the underlying modal logic of relative fundamentality.

4 Further Topics

In this last section, I would like to elaborate a bit on two important topics within the formal theory of grounding. The first topic, discussed in Section 4.1, has been touched upon in previous parts of this work. The second topic, discussed in Section 4.2, has not yet been addressed at all.

4.1 Ground-Theoretic Equivalence, Metaphysical Equival-ence and Identity

In this section, I will assume that grounding statements express, at the semantic level, relations between certain entities. This is of course a natural view to have if one takes grounding statements to involve predicates for the corresponding notions of grounding, but one may also hold that view while taking grounding statements to involve operators rather than predicates for the corresponding notions. In fact, even though the approaches to the logic of grounding presented in Sections 3.1 to 3.6 have it that the linguistic expressions for grounding are sentential operators rather than predicates, they all treat grounding statements as corresponding, at the semantic level, to relations between certain entities. I called these entities ‘facts’ or ‘propositions’, depending on the particular view at stake. For the sake of neutrality, I will here use the label ‘g-contents’ instead.⁴⁴

Three equivalence relations between g-contents have been of particular importance in studies about grounding: ground-theoretic equivalence, metaphysical equivalence and identity. The latter relation is plain numerical identity. The other two relations can be defined as follows, where $<$ is here used as a predicate for non-factive strict full grounding understood as a relation between g-contents:

• $x$ is ground-theoretically equivalent to $y$ iff ${}_{\text{df}}$ (i) whatever grounds one grounds the other and (ii) whatever one helps to ground, the other also grounds in the same way – with symbols: (i) for all pluralities of g-contents $Z$ , $Z<x$ iff $Z<$ and (ii) for all pluralities of g-contents $Z$ and all g-contents $z$ , $Z,x<z$ iff $Z,y<z$ .

• $x$ is metaphysically equivalent to $y$ iff ${}_{\text{df}}$ to say that $x$ holds and to say that $y$ holds is to describe the world as being the same way.⁴⁵

Once equipped with the notions of ground-theoretic equivalence and metaphysical equivalence as they have just been defined, one can define corresponding relations for sentences of some language or languages, by saying that two sentences are ground-theoretically equivalent (metaphysically equivalent) just in case the g-contents they express are ground-theoret-ically equivalent (metaphysically equivalent). Depending on the context, it may be relevant to directly invoke these sentential notions rather than their content-theoretic counterparts, and vice versa.

4.1.1 Two Applications: The Granularity Question and the Worldly / Representational Distinction

The previous point is illustrated by the formulation of the ‘granularity question’ for grounding and the characterization of the worldly / representational distinction. The granularity question for grounding is the question of ‘how fine-grained grounding is’. A very natural precisification of the question invokes sentential ground-theoretic equivalence:

• Which sentences (of a given language or of given languages) are ground-theoretically equivalent?⁴⁶

In Section 3.5, I introduced the worldly / representational distinction by saying that a notion of grounding is worldly if it is sensitive only to how the world is, and that it is representational otherwise. A more precise characterization of being worldly goes as follows, where only content-theoretic notions are invoked:

• A notion of grounding is worldly iff any two g-contents are ground-theoretically equivalent (where ground-theoretic equivalence is defined in term of the notion of grounding in question) if they are metaphysically equivalent.⁴⁷

A direct consequence of this characterization is that for any notion of grounding, if metaphysical equivalence between g-contents entails identity, then that notion of grounding is worldly.

4.1.2 Relations between the Three Notions

What are the relations between ground-theoretic equivalence, metaphysical equivalence and identity? By Leibniz’s Law, of course, g-content identity entails both ground-theoretic and metaphysical equivalence. But are there other entailments between the three relations, and if so, which ones? Various theories give various answers to the question. Let me run through some of them.

As we saw, the logics put forward in Correia (2010, 2017) contain an explicit logic of factual / propositional equivalence – sym-bol-ized in both papers by $\approx$  – and semantically, factual / propositional equivalence is interpreted as g-content identity. In Correia (2010), I stipulate that factual equivalence stands for metaphysical equivalence understood as defined above. Therefore, on the view I explore there, metaphysical equivalence entails identity. (From which it follows that the notion targeted by the view is worldly – see two paragraphs back.) Not so on the view explored in Correia (2017), at least given some assumptions about what is metaphysically equivalent to what that I find plausible. Given any $\varphi$ , the 2017 logic takes the contents of $\varphi$ , $\varphi \wedge \varphi$ , $\varphi \vee \varphi$ and $\neg \neg \varphi$ to be pairwise distinct. Yet I am very much inclined to take $\varphi$ , $\varphi \wedge \varphi$ , $\varphi \vee \varphi$ and $\neg \neg \varphi$ to be metaphysically equivalent, for any $\varphi$ .

Does ground-theoretic equivalence entail identity on these views? Correia (2017) contains a proof that this is the case in the logic it puts forward. I do not know whether the entailment holds in the logic explored in Correia (2010).

An upshot of the previous considerations is that metaphysical equivalence entails ground-theoretic equivalence in the logic of Correia (2010) but not in the logic of Correia (2017). Another upshot is that the converse entailment holds in the logic of Correia (2017), and that I do not know whether it holds in the logic of Correia (2010).

In Correia (2016), I present a proof system for the logic of factual equivalence, which, as in Correia (2010), I understand as standing for metaphysical equivalence. I provide two alternative semantic characterizations of the system. One of them is within Fine’s truthmaker framework, and it deems a sentence of type $\varphi \approx \psi$ true when $\varphi$ and $\psi$ have the same ‘positive content’ in Fine’s (2012a) sense, that is, when the set of verifiers of $\varphi$ = the set of verifiers of $\psi$ (see Section 3.1). If we assume, in line with Fine (2012a) and Fine (2012b), that a g-content is a set of states closed under fusion, then the view put forward in Correia (2016) naturally extends to a view according to which two g-contents are metaphysically equivalent only if they are identical. On such a view, of course, metaphysical equivalence entails ground-theoretic equivalence.⁴⁸

Correia (2016) does not offer a specific account of grounding, but it presupposes that the kind of account put forward in Correia (2010) and Fine (2012a, 2012b) is correct. I have a proof, too long to include here, that on Fine’s truthmaker version of the account, ground-theoretic equivalence between g-contents entails identity (and hence metaphysical equivalence). The proof assumes that a state has a proper part only if it admits of a decomposition into proper parts. The assumption is not built into the truthmaker framework, but is it a rather natural assumption to make.

As we saw (Section 3.7), Krämer (2018) features two relations of strict full grounding, one relating unilateral propositions and the other one relating bilateral propositions. Each gives rise to its own notion of ground-theoretic equivalence. Let us first focus on the unilateral notion.

It can be shown that ground-theoretic equivalence between unilateral propositions entails identity.⁴⁹ Krämer does not discuss metaphysical equivalence, but its connections with identity and ground-theoretic equivalence in his framework can nevertheless be identified, in part with the help of extra assumptions. Given that ground-theoretic equivalence between unilateral propositions entails identity, it ipso facto entail metaphysical equivalence. I find it utterly plausible that $\varphi$ and $\varphi \wedge \varphi$ are metaphysically equivalent for any $\varphi$ . On Krämer’s account, $\varphi$ and $\varphi \wedge \varphi$ always express distinct unilateral propositions. Hence, assuming I am right about self-conjunctions, on his account, metaphysical equivalence between unilateral propositions does not entail identity. It follows that metaphysical equivalence between unilateral propositions does not entail ground-theoretic equivalence.

Let us move on to the bilateral case. Krämer establishes that bilateral propositions $⟨P,P^{\prime }⟩$ and $⟨Q,Q^{\prime }⟩$ are ground-theoretically equivalent iff $P=Q$ . It immediately follows that ground-theoretic equivalence between bilateral propositions does not entail identity. Self-conjunctions can again be used to show that bilateral propositions may be metaphysically equivalent without being identical. On Krämer’s account, if $\varphi$ expresses the bilateral proposition $⟨P,Q⟩$ , then $\varphi \wedge \varphi$ expresses a bilateral proposition $⟨f\left(P\right),g\left(Q\right)⟩$ where $f\left(P\right)\ne P$ (it is not important for my purposes to specify exactly the nature of functions $f$ and $g$ ). Granted that $\varphi$ and $\varphi \wedge \varphi$ are metaphysically equivalent, it follows that on Krämer’s account, metaphysical equivalence between bilateral propositions does not entail identity. It also follows, via the result established by Krämer mentioned above, that metaphysical equivalence between bilateral propositions does not entail ground-theoretic equivalence. Does ground-theoretic equivalence between bilateral propositions entail metaphysical equivalence? Krämer’s account of ground-theoretic equivalence alone does not decide the question.

4.1.3 Interaction with Conjunction, Disjunction and Negation

Let me finally turn to the question of how ground-theoretic equivalence, metaphysical equivalence and g-content identity interact with conjunction, disjunction and negation. There are actually two questions here, depending on whether conjunction, disjunction and negation are understood as operations on g-contents or as sentential operators. Let me call the first question content-theoretic and the second question linguistic. A theory which addresses the content-theoretic question for, say, ground-theoretic equivalence will decide whether claims such as the following ones are true, where $\sqcap$ is an operation of g-content-conjunction and $-$ an operation of g-content-negation:

• $X\sqcap Y$ is ground-theoretically equivalent to $Y\sqcap X$

• $--X$ is ground-theoretically equivalent to $X$

• If $X$ is ground-theoretically equivalent to $Y$ , then so is $-X$ to $-Y$

By contrast, a theory which addresses the linguistic question for ground-theoretic equivalence will take as given a mapping $\left[\right]$ from sentences of some language to g-contents, and will decide whether claims such as the following ones are true, where $\wedge$ is a conjunction operator and $\neg$ a negation operator:

• $[\varphi \wedge \psi ]$ is ground-theoretically equivalent to $[\psi \wedge \varphi ]$

• $\left[\neg \neg \varphi \right]$ is ground-theoretically equivalent to $\left[\varphi \right]$

• If $\left[\varphi \right]$ is ground-theoretically equivalent to $\left[\psi \right]$ , then so is $\left[\neg \varphi \right]$ to $\left[\neg \psi \right]$

All the theories of g-content that have been discussed so far feature an operation of conjunction and an operation of disjunction on g-contents. Some also feature an operation of negation, but some do not. Since these theories are nevertheless all coupled with a semantics for (linguistic) conjunction, disjunction and negation, let me put aside the content-theoretic question and focus on the linguistic question instead.

As before, let us suppose given a pool of atomic sentences and define the basic sentences relative to that pool as the sentences that can be built from the atomic sentences using $\wedge$ , $\vee$ , $\neg$ and the brackets (and). For the purpose of theorizing about ground-theoretic equivalence, metaphysical equivalence and g-content identity, we may introduce the sentential operators ${\approx }_{GT}$ , ${\approx }_M$ and ${\approx }_I$ , respectively, together with the following intended intuitive semantics:

• $\varphi {\approx }_{GT}\psi$ is true iff $\varphi$ ’s g-content is ground-theoretically equivalent to $\psi$ ’s g-content

• $\varphi {\approx }_M\psi$ is true iff $\varphi$ ’s g-content is metaphysically equivalent to $\psi$ ’s g-content

• $\varphi {\approx }_I\psi$ is true iff $\varphi$ ’s g-content = $\psi$ ’s g-content

(As far as the discussion to come is concerned, we could take the three symbols to be predicates of sentences rather than sentential operators.)

As we saw, Correia (2010) puts forward a logic for ${\approx }_M$ , which also counts as a logic for ${\approx }_I$ , and Correia (2017) puts forward a logic for ${\approx }_I$ , which also counts as a logic for ${\approx }_{GT}$ . In these logics, equivalence sentences can be parts of more complex sentences. Let us here focus on languages that only have equivalence sentences, and address the question of which such sentences are true in virtue of their logical form. And let me use the symbol $\approx$ without specifying which notion it is supposed to express.

In Correia (2020), following Krämer (2021), I discuss five relevant systems. I reproduce some of the discussion here, and make connections with previous parts of this Element. The five systems are the Hilbert-style systems defined in Figures 13 to 17 (the labels are from Correia 2020).

Figure 13 System C${}_{\text{2017}}$

Axioms

1. A1. $\varphi \wedge \psi \approx \psi \wedge \varphi$

2. A2. $\varphi \vee \psi \approx \psi \vee \varphi$

3. A3. $\varphi \approx \varphi$

Rules

1. R1. $\varphi \approx \psi /\psi \approx \varphi$

2. R2. $\varphi \approx \psi ,\psi \approx \chi /\varphi \approx \chi$

3. R3. $\varphi \approx \psi /\varphi \wedge \chi \approx \psi \wedge \chi$

4. R4. $\varphi \approx \psi /\varphi \vee \chi \approx \psi \vee \chi$

5. R5. $\varphi \approx \psi /\neg \varphi \approx \neg \psi$

Figure 14 System K${}_{\text{int}}$

Axioms

Like C ${}_{\text{2017}}$ , plus:

1. A4. $\neg (\varphi \wedge \psi )\approx \neg \varphi \vee \neg \psi$

2. A5. $\neg (\varphi \vee \psi )\approx \neg \varphi \wedge \neg \psi$

Rules

Like C ${}_{\text{2017}}$ , minus R5, plus:

1. R6. $\varphi \approx \psi /\neg \neg \varphi \approx \neg \neg \psi$

Figure 15 System K${}_{\text{ext}}$

Axioms

Like K ${}_{\text{int}}$ , plus:

1. A6. $\varphi \wedge \varphi \approx \varphi \vee \varphi$

2. A7. $\varphi \vee \varphi \approx \neg \neg \varphi$

Rules

Like K ${}_{\text{int}}$ , plus:

1. R7. $\varphi ⋐\psi ,\varphi ⋐\chi /\varphi ⋐(\psi \wedge \chi )$

2. R8. $\varphi ⋐\psi /\varphi ⋐(\psi \vee \chi )$

where $\varphi ⋐\psi$ is used for $\varphi \vee \psi \approx \psi \vee \psi$

Figure 16 System C${}_{\text{2016}}$

Axioms

Like K ${}_{\text{int}}$ , minus A3, plus:

1. A8. $\varphi \approx \neg \neg \varphi$

2. A9. $\varphi \approx \varphi \wedge \varphi$

3. A10. $\varphi \approx \varphi \vee \varphi$

4. A11. $\varphi \wedge (\psi \wedge \chi )\approx (\varphi \wedge \psi )\wedge \chi$

5. A12. $\varphi \vee (\psi \vee \chi )\approx (\varphi \vee \psi )\vee \chi$

6. A13. $\varphi \wedge (\psi \vee \chi )\approx (\varphi \wedge \psi )\vee (\varphi \wedge \chi )$

Rules

Like K ${}_{\text{int}}$ , minus R6

Figure 17 System C${}_{\text{2010}}$

Axioms

Like C ${}_{\text{2016}}$ , plus:

1. A14. $\varphi \vee (\psi \wedge \chi )\approx (\varphi \vee \psi )\wedge (\varphi \vee \chi )$

Rules

Like C ${}_{\text{2016}}$

C ${}_{\text{2017}}$ is a system which captures the logically true formulas of type $\varphi \approx \psi$ that one gets on the basis of the logic discussed in Correia (2017). As we saw, in that logic $\approx$ expresses g-content identity, and can also be understood as expressing ground-theoretic equivalence. K ${}_{\text{int}}$ and K ${}_{\text{ext}}$ are the ‘intermediate’ system and the ‘extensional’ system, respectively, of Krämer (2021). Krämer interprets $\approx$ in both systems as expressing ground-theoretic equivalence between bilateral propositions, as they are defined in his 2018 paper. C ${}_{\text{2016}}$ is the system for metaphysical equivalence discussed in Correia (2016). As we saw, given certain assumptions, $\approx$ as semantically characterized there can also be understood as expressing both g-content identity and ground-theoretic equivalence. Finally, C ${}_{\text{2010}}$ has the same theorems as R. B. Angell’s (1989) system for ‘analytic equivalence’ (see Fine 2016 for the axiomatization presented here), and it is a system which captures the logically true formulas of type $\varphi \approx \psi$ that one gets on the basis of the system discussed in Correia (2010). As we saw, in that system $\approx$ is interpreted as metaphysical equivalence and is semantically interpreted as expressing g-content identity. These systems are related as follows, where $⟶$ represents strict inclusion between systems ( $S_1⟶S_2$ means that all theorems of $S_1$ are theorems of $S_2$ but not vice versa)⁵⁰:

${\text{C}}_{\text{2017}}⟶{\text{K}}_{\text{int}}⟶{\text{K}}_{\text{ext}}⟶{\text{C}}_{\text{2016}}⟶{\text{C}}_{\text{2010}}$

In the proposed axiomatizations, the axioms and rules of C ${}_{\text{2016}}$ are exactly those of C ${}_{\text{2010}}$ , minus the distributivity axiom A14. What justification can be given for not having A14 as an axiom?

We saw in Section 3.3 that $\varphi \vee (\psi \wedge \chi )$ and $(\varphi \vee \psi )\wedge (\varphi \vee \chi )$ need not have the same verifiers. If we take seriously the view that metaphysical equivalence corresponds semantically to sameness of g-content, and if we take the g-content associated with a sentence to be the set of its verifiers, then we have a justification for not taking A14 as axiomatic if $\approx$ represents metaphysical equivalence.

There is another justification (or perhaps better: motivation) that I advertised at the beginning of Section 3.4: A14 conflicts with some intuitions about grounding. More precisely, A14, understood with $\approx$ expressing metaphysical equivalence, conflicts with grounding understood as worldly. For assume $\varphi <\varphi \vee \neg \psi$ and $\psi <\varphi \vee \psi$ , where $<$ stands for worldly strict full grounding (factive or non-factive, it does not matter). As an illustration, we may take $\varphi =$ ‘Snow is white’ and $\psi$ = ‘Socrates is human’. From these two assumptions, one can plausibly infer $\varphi ,\psi <(\varphi \vee \neg \psi )\wedge (\varphi \vee \psi )$ . It actually turns out that all the impure logics featuring $<$ that we previously discussed validate the inference from ${\varphi }_1<{\psi }_1$ and ${\varphi }_2<{\psi }_2$ to ${\varphi }_1,{\varphi }_2<({\psi }_1\wedge {\psi }_2)$ . Suppose now for reductio that A14 holds, where $\approx$ expresses metaphysical equivalence. Since $<$ is worldly, one can infer $\varphi ,\psi <\varphi \vee (\neg \psi \wedge \psi )$ . But intuitively, $\psi$ plays no role in fully grounding $\varphi \vee (\neg \psi \wedge \psi )$ . For more details, see Correia (2016) and Krämer and Roski (2015).⁵¹

4.2 Puzzles

It has been argued, first by Fine (2010) in the very early days of the contemporary research on grounding, that several sets of ground-theoretic principles which have some plausibility are nevertheless inconsistent – on their own or in conjunction with other, non-ground-theoretic principles that are themselves plausible. In this section, I discuss the Finean puzzles and some other ground-theoretic puzzles that have been recently discussed in the literature.

4.2.1 Fine-Style Puzzles

Fine (2010) puts forward a series of similar sets of ground-theoretic principles whose members are all plausible but which are inconsistent given a background of classical logical principles. Krämer (2013) formulates a particularly simple version of the Fine-style puzzles, which has the effect of narrowing down the reasonable options for solving the other puzzles.⁵²

Fine’s puzzles as well as Krämer’s invoke the concept of partial strict grounding, where a partial strict ground is a part of a strict full ground. In Section 2.1, following Fine (2012a), I used the operator ${\prec }^{*}$ for that notion, but here I will use $\prec$ instead, thereby following Fine (2010) and Krämer (2013). Both Fine and Krämer assume that partial strict grounding is factive, but the puzzles arise, actually in a more straightforward way, if the notion is assumed to be non-factive.

Here is one of Fine’s argument that leads to inconsistency, almost verbatim:

1. (1) Something exists – in symbols: $\exists xEx$ .

2. (2) Therefore, the fact that something exists exists – in symbols: $E\left[\exists xEx\right]$ .

3. (3) Given (2), $E\left[\exists xEx\right]\prec \exists xEx$ .

4. (4) Given (2), $\exists xEx\prec E\left[\exists xEx\right]$ .

5. (5) $\prec$ is asymmetric.

6. (6) (3)–(5) are inconsistent.

The starting point of the argument, (1), is hard to reject. The justification of steps (2)–(4) relies on the following general principles (Fine has slightly different formulations of the principles, but the differences are immaterial for our discussion)⁵³:

Factual Existence:

If $\varphi$ , then $E\left[\varphi \right]$ ;

Existential Grounding:

If $Fa$ , then $Fa\prec \exists xFx$ ;

Factual Grounding:

If $E\left[\varphi \right]$ , then $\varphi \prec E\left[\varphi \right]$ .

Factual Existence justifies (2), Existential Grounding justifies (3), and Factual Grounding justifies (4). Instead of invoking the asymmetry of $\prec$ , Fine invokes its transitivity and irreflexivity. But since asymmetry is weaker than the combination of transitivity and irreflexivity, one gets a more compelling argument if one invokes, as I did here, the former rather than the latter.

The other puzzling arguments that Fine presents also involve the assumption that $\prec$ is transitive and irreflexive – but which could, as with the previous argument, be replaced by the assumption that $\prec$ is asymmetric. They concern either facts, like the previous argument, or propositions or sentences. And – crucially – they all involve either Existential Grounding or a corresponding principles for universal quantification⁵⁴:

Universal Grounding:

If $\forall xFx$ , then $Fa\prec \forall xFx$ .

Importantly, contrary to Factual Grounding and other ground-theoretic principles used in Fine’s arguments, Existential Grounding and Universal Grounding do not feature expressions for facts, propositions or sentences.

Krämer’s puzzle is very similar to the Finean puzzle introduced above. It is based on the following principle, akin to Existential Grounding but involving quantification into sentential rather than nominal position⁵⁵:

Higher-Order Existential Grounding:

If $\varphi \left[\psi /p\right]$ , then $\varphi \left[\psi /p\right]\prec \exists p\varphi$ ,

where $p$ is the only free variable in $\varphi$ , $\psi$ has no free variable, and $\varphi \left[\psi /p\right]$ is the result of replacing each free occurrence of $p$ in $\varphi$ by $\psi$ . The argument leading to inconsistency is very short:

1. (1) Something is the case – in symbols: $\exists pp$ .

2. (2) Given (1), $\exists pp\prec \exists pp$ .

3. (3) $\prec$ is irreflexive.

4. (4) (1)–(3) are inconsistent.

Step (2) is justified by Higher-Order Existential Grounding: take $p$ for $\varphi$ and $\exists pp$ for $\psi$ . Note that condition (3) could have been replaced by the stronger condition that $\prec$ is asymmetric.

Putting aside misgivings about higher-order quantification or Modus Ponens, the options for escaping Krämer’s puzzle are (i) to reject Higher-Order Existential Grounding and (ii) to reject the view that $\prec$ is irreflexive. The corresponding options to escape Fine’s puzzle are (a) to reject Existential Grounding and (b) to reject the view that $\prec$ is asymmetric. Of course, Fine’s puzzle involves extra principles, namely Factual Existence and Factual Grounding, but if there is a solution of Krämer’s puzzle along the lines of (i) or (ii), then presumably there should at least be a solution to Fine’s puzzle along the lines of (a) or (b).⁵⁶ This can generalized to each of the Finean puzzles, replacing ‘Existential Grounding’ by ‘Universal Grounding’ if needed, according to the principle at work in the puzzle.

In light of the previous sections, what are the options on the table? Most of the logics discussed in Section 3 validate the following principle for $\prec$ ⁵⁷:

Disjunctive Grounding:

If $\varphi$ , then $\varphi \prec \varphi \vee \psi$ ;

If $\psi$ , then $\psi \prec \varphi \vee \psi$ .

Among the logics which countenance Disjunctive Grounding and which also deal with the interaction between grounding and the quantifiers, most also countenance Existential Grounding. This is not surprising: given the similarities between existential quantification and disjunction, it is indeed hard to see how one could accept Disjunctive Grounding and reject Existential Grounding. Even if it is not formally impossible to do it (see for instance Fine 2010, § 7), it is not clear – to me at least! – that going that way is philosophically satisfactory. For the logics under consideration, rejecting the asymmetry of $\prec$ as a way out of the Finean puzzle presented above strikes me as the best way to go – and I have the same opinion about the other Finean puzzles, on similar grounds.⁵⁸ Likewise, I take it that for these logics, rejecting the irreflexivity of $\prec$ is the best way to go in reaction to Krämer’s puzzle.⁵⁹

The logics discussed in Section 3 that do not validate Disjunctive Grounding are the logics of worldly grounding of Fine (2012a) (semantic side), Correia (2010), Lovett (2020a) and Correia (2023) (see Sections 3.1–3.4). (It is easy to see why they reject Disjunctive Grounding: they reject the possibility that $\varphi \prec \varphi \vee \varphi$ .) Given that they reject Disjunctive Grounding, it is natural to suspect that they also reject Existential Grounding, or that they would reject it once suitably extended to take care of quantified statements if this is not already the case. I think the suspicion is correct.⁶⁰

As we saw, in these logics, factive strict full grounding is definable in terms of a non-factive notion of weak full grounding – or, equivalently, a notion of disjunctive parthood – in the very same way. Indeed – focusing on definability in terms of weak full grounding for the sake of illustration – these logics all agree on the following biconditional:

(Def)

Some facts $F_1$ , $F_2$ , $\dots$ factively strictly fully ground a fact $G$ iff (i) $F_1$ , $F_2$ , $\dots$ all obtain, (ii) $F_1$ , $F_2$ , $\dots$ non-factively weakly fully ground $G$ , and (iii) $G$ does not help non-factively weakly fully ground any of the $F_i$ s.

All the logics in question also validate the following principle, akin to Disjunctive Grounding (but without the conditional form since $⩽$ is non-factive):

Weak Disjunctive Grounding:

$\varphi ⩽\varphi \vee \psi$ ;

$\psi ⩽\varphi \vee \psi$ .

Given (Def), and given that a partial strict ground is a part of a strict full ground, the logics validate the following restricted version of Disjunctive Grounding, where $\preccurlyeq$ is the partial notion corresponding to $⩽$ :

Restricted Disjunctive Grounding:

If $\varphi$ and $\varphi \vee \psi ⋠\varphi$ , then $\varphi \prec \varphi \vee \psi$ ;

If $\psi$ and $\varphi \vee \psi ⋠\psi$ , then $\psi \prec \varphi \vee \psi$ .

Turning now to the quantifiers, given that Weak Disjunctive Grounding is accepted, so should presumably be its existential counterpart:

Weak Existential Grounding:

$Fa⩽\exists xFx$ .

From this and (Def) we then only get a restricted version of Existential Grounding:

Restricted Existential Grounding:

If $Fa$ and $\exists xFx⋠Fa$ , then $Fa\prec \exists xFx$ .

There is no way, in the spirit of the logics under consideration, to get the unrestricted version.

With Restricted Existential Grounding rather than Existential Grounding in place, the Finean argument does not go through. At line (3), instead of getting $E\left[\exists xEx\right]\prec \exists xEx$ tout court, we get it conditional on the truth of $\exists xEx⋠E\left[\exists xEx\right]$ . The latter is not guaranteed to be true – even worse, what we arrived at line (4), namely $\exists xEx\prec E\left[\exists xEx\right]$ , entails that $\exists xEx⋠E\left[\exists xEx\right]$ is false! Thus, we cannot infer $E\left[\exists xEx\right]\prec \exists xEx$ and so we cannot conclude to inconsistency via the asymmetry of $\prec$ .⁶¹

Similar considerations hold for the other Finean puzzles – I leave the details aside. Similar considerations also hold for Krämer’s puzzle, but since the details are very few in number let me go through them. In the spirit of the logics under consideration, Higher-Order Existential Grounding should be replaced by the appropriate restriction:

Restricted Higher-Order Existential Grounding:

If $\varphi \left[\psi /p\right]$ and $\exists p\varphi ⋠\varphi \left[\psi /p\right]$ , then $\varphi \left[\psi /p\right]\prec \exists p\varphi$ .

Instantiate in the same way as before and you get: if $\exists pp$ and $\exists pp⋠\exists pp$ , then $\exists pp\prec \exists pp$ . Now the second condition is false since $\preccurlyeq$ is reflexive. Puzzle solved.

The previous discussion of the Fine-style puzzles would deserve more space; the interested reader may consult Krämer (2020) for a very good complement. Before leaving this topic, though, let me briefly comment upon Fritz (2020), which elaborates on Krämer’s puzzle in an interesting way (and which Krämer 2020 does not discuss).

Fritz explores the idea of rejecting Higher-Order Existential Grounding while at the same time accepting another higher-order principle that expresses the same core idea. This other principle, $\left(\exists Q\right)$ , is formulated in a language that allows for both quantification into sentential position and quantification into sentential operator position:

$\left(\exists Q\right)$

$\forall X\forall p(Xp\supset (Xp\prec EX\left)\right)$ .

In $\left(\exists Q\right)$ , $p$ is (as before) a sentential variable, $X$ is a monadic sentential operator variable, and $EX$ is the Frege-friendly way of expressing what in the more standard notation we would express by means of a formula like $\exists qXq$ . (Frege held the view that quantifiers are properties of properties.) Instantiate $X$ with a given operator $T$ and $p$ with $ET$ and you get:

$\left(\exists Q^{+}\right)$

$T\left(ET\right)\supset \left(T\right(ET)\prec ET)$ .

For the purpose of mimicking Krämer’s argument, Fritz takes $T$ to be $\lambda p.p$ .⁶² Since $T\left(ET\right)$ then says that it is the case that something is the case (or something like that), it can safely be taken to be true and so from $\left(\exists Q^{+}\right)$ one can infer:

$\left(\exists Q^{++}\right)$

$\lambda p.p(E\lambda p.p)\prec E\lambda p.p$ .

This is not a counterexample to the irreflexivity of $\prec$ . We do get a counterexample to a standard structural principle for $\prec$ if we assume either $\lambda p.p(E\lambda p.p)\doteq E\lambda p.p$ , where $\doteq$ is akin to standard identity but of the appropriate grammatical type, or $E\lambda p.p\prec \lambda p.p(E\lambda p.p)$ . In the first case, $E\lambda p.p\prec E\lambda p.p$ can be inferred from $\left(\exists Q^{++}\right)$  – a violation of the irreflexivity of $\prec$ . (It is here assumed that the relevant context is not ‘opaque’, i.e., that one can apply Leibniz’s Law for $\doteq$ in the suggested way.) In the second case, we have a violation of the asymmetry of $\prec$ . $\lambda p.p(E\lambda p.p)\doteq E\lambda p.p$ is a consequence of a principle known as $\beta$ -conversion, and $E\lambda p.p\prec \lambda p.p(E\lambda p.p)$ a consequence of a principle Fritz calls ‘ $\beta$ -grounding’, which is advocated by Fine (2012a). In his paper, Fritz sketches a general view on lambda abstraction that rejects both $\beta$ -conversion and $\beta$ -grounding.

Whether the view that Fritz sketches is viable or not, it can be argued that $\left(\exists Q\right)$ yields violations of structural principles about $\prec$ relative to all the impure logics that have been developed so far. Here are indeed two consequences of $\left(\exists Q^{+}\right)$ :

1. (I) If $\prec$ is irreflexive, then there is no operator $T$ such that $T\left(ET\right)$ holds and the inference from $T\varphi \prec \psi$ to $\varphi \prec \psi$ is generally acceptable;

2. (II) If $\prec$ is asymmetric, then there is no operator $T$ such that $T\left(ET\right)$ holds and $\varphi \prec T\varphi$ generally holds.

All the impure logics of grounding that have been developed so far, at least all those I am aware of, are at odds either with the consequent of (I) or with the consequent of (II). Let for instance $T\varphi$ be defined as $\neg \neg \varphi$ . $T\left(ET\right)$ then certainly holds. Some of the logics in question take $\neg \neg \varphi$ to be ground-theoretically equivalent to $\varphi$  – in which case they take the inference from $\neg \neg \varphi \prec \psi$ to $\varphi \prec \psi$ to be generally acceptable. This is the case, for instance, of the logic developed in Correia (2010) and of the logic determined by the semantics in Fine (2012a). All the other logics take $\varphi \prec \neg \neg \varphi$ to generally hold. This is the case, for instance, of the logic determined by the proof-theory in Fine (2012a), the logic developed in Correia (2017) and the one developed in deRosset and Fine (2023).

4.2.2 Fritz’s Puzzles

Fritz (2022) presents two challenges for people taking the concept of immediate grounding to be meaningful, in the form of two arguments which show that given plausible assumptions about the notion, contradiction follows. The two arguments are similar, but one of them is significantly simpler and so I shall mainly focus on it.

The argument is formulated in a language with an operator $\prec$ for (factive) immediate partial grounding, sentential quantifiers which can bind singular variables ( $p$ , $q$ , $\dots$ ) as well as plural variables ( $pp$ , $qq$ , $\dots$ ), a symbol $ϵ$ to express plurality membership, and a sentential operator $\bigwedge$ that takes a plural variable $pp$ to make the sentence $\bigwedge pp$ , intended to express conjunction (of non-fixed arity).

Following Fritz, let me lay down the following definitions:

• $Tpp:=\forall p(pϵpp\supset p)$

• $\bar{\forall }pp\varphi :=\forall pp(Tpp\supset \varphi )$

• $pp\doteqdot qq:=\forall p(pϵpp\equiv pϵqq)$

The first argument consists in showing that the following two principles are inconsistent (here and below I use Fritz’s labels):

( $\bigwedge \prec$ )

$\bar{\forall }pp\forall p(p\prec \bigwedge pp\equiv pϵpp)$

( $\bigwedge T$ )

$\forall pp(\bigwedge pp\equiv Tpp)$

From ( $\bigwedge \prec$ ) one can infer ( $S\bigwedge$ ) and from ( $\bigwedge T$ ) ( $T\bigwedge$ ):

( $S\bigwedge$ )

$\bar{\forall }pp\bar{\forall }qq(\bigwedge pp=\bigwedge qq\supset pp\doteqdot qq)$

( $T\bigwedge$ )

$\bar{\forall }pp\bigwedge pp$

Now these two principles yield a violation of a higher-order version of a corollary of Cantor’s theorem. Cantor’s theorem says that given any set $E$ , there is no surjective function from $E$ to its power set $P\left(E\right)$ . The corollary in question says that given any set $E$ , there is no total injective function from $P\left(E\right)$ to $E$ . What the two principles say, in set-theoretic idiom, is that $\bigwedge$ is a total injective function from the power set of the set of all truths to the set of all truths – in direct violation of the corollary of Cantor’s theorem. A version of this corollary can be established in a suitable higher-order language. Hence the inconsistency of ( $S\bigwedge$ ) and ( $T\bigwedge$ ).

( $\bigwedge T$ ) looks harmless, as it seems to simply record the behaviour of conjunctions relative to the notion of ‘being the case’. ( $\bigwedge \prec$ ) is the specific ground-theoretic source of the inconsistency. What could be said in its favour?

It is true that one sometimes hears or reads statements like ‘what immediately (strictly fully) grounds a conjunctive fact are its conjuncts taken together’, and that prima facie there seems to be some truth that these statements express. Granted that an immediate partial ground is just a part of an immediate strict full ground, the above statement entails ‘what immediately partially grounds a conjunctive fact are its conjuncts taken separately’. ( $\bigwedge \prec$ ) looks like a very good way of formalizing a generalization of the latter statement.

But in order to assess ( $\bigwedge \prec$ ) seriously more than first impressions about a notion are needed. I will not go through a detailed discussion here, but I would simply like to point out that according to some of the conceptions of grounding that have been discussed in Section 3, whatever immediate partial grounding may turn out to be, ( $\bigwedge \prec$ ) must clearly be rejected.

I have in mind the worldly conceptions of grounding at work in Correia (2010), Fine (2012a)-semantic side, Lovett (2020a) and Correia (2023). Let me simply focus on Fine (2012a) for illustration. In order to stick to the Finean talk of facts (or proposition or contents) and their ground-theoretic connections at the semantic level, I will interpret the quantifiers in ( $\bigwedge \prec$ ) not as sentential quantifiers, but as nominal quantifiers ranging over such entities. The following considerations could be made thoroughly higher-order.

Let $s$ and $t$ be two states such that $t$ is not a part of $s$ , and consider the distinct facts $F=\{s,st\}$ and $G=\left\{s\right\}$ , which we suppose obtain. (Here and in the next argument, I use ‘ $st$ ’ for the fusion of $s$ and $t$ .) By ( $\bigwedge \prec$ ) ‘right-to-left’, $F$ should be an immediate partial ground of the conjunction $F\sqcap G$ of $F$ and $G$ . But it turns out that $F\sqcap G=F$ , and I guess that, whatever immediate partial grounding may turn out to be, we do not want to say that $F$ is an immediate partial ground of itself.⁶³

Here is a stronger argument against ( $\bigwedge \prec$ ), one which does not rely on considerations of self-grounding. Consider three states $s$ , $t$ and $u$ that are disjoint (not just distinct) from one another. Consider then the three facts $F=\left\{s\right\}$ , $G=\left\{t\right\}$ and $H=\left\{u\right\}$ , which we suppose obtain. By ( $\bigwedge \prec$ ) ‘right-to-left’, $F$ immediately partially grounds $F\sqcap (G\sqcap H)$ .⁶⁴ Since $F\sqcap (G\sqcap H)=(F\sqcap G)\sqcap H$ , ( $\bigwedge \prec$ ) ‘left-to-right’ allows one to infer that either $F=F\sqcap G$ or $F=H$ . But this requires that either $s=st$ or $s=u$ , and this is ruled out by our initial mereological assumption.

The more complex argument put forward by Fritz is also ineffective if the conceptions of grounding under consideration above are taken for granted. In place of ( $\bigwedge \prec$ ), it invokes three similar principles: the immediate partial grounds of a true binary conjunction are its conjuncts; every true binary disjunction has at least one disjunct as an immediate partial ground, and every immediate partial ground of a disjunction is one of the disjuncts; every true universal quantification has all its instances as immediate partial grounds, and every immediate partial ground of a universal quantification is either one of its instances or a suitable ‘totality fact’. The previous objections against ( $\bigwedge \prec$ ) also apply to the first principle, since these arguments invoked specifically binary conjunctions. Similar objections can be formulated against the other two principles.

4.2.3 Wilhelm’s Inconsistency

Wilhelm (2021) shows that the following principles are inconsistent, where $\prec$ stands for (factive) immediate partial grounding and $\approx$ stands for propositional identity:

1. (1) $\varphi \prec (\psi \wedge \chi )$ iff $(\psi \wedge \chi )$ and ( $\varphi \approx \psi$ or $\varphi \approx \chi$ );

2. (2) $\varphi \prec \neg (\psi \wedge \chi )$ iff $\varphi$ and ( $\varphi \approx \neg \psi$ or $\varphi \approx \neg \chi$ );

3. (3) $\varphi \prec \psi \vee \chi$ iff $\varphi$ and ( $\varphi \approx \psi$ or $\varphi \approx \chi$ );

4. (4) $\varphi \prec \neg (\psi \vee \chi )$ iff $\neg (\psi \vee \chi )$ and ( $\varphi \approx \neg \psi$ or $\varphi \approx \neg \chi$ );

5. (5) $\varphi \prec \neg \neg \psi$ iff $\varphi$ and $\varphi \approx \psi$ ;

6. (6) Sometimes, $\varphi$ but not $\varphi \prec \varphi$ ;

7. (7) $(\varphi \wedge \psi )\approx \neg (\neg \varphi \vee \neg \psi )$ .

And he also shows that the inconsistency remains if (7) is replaced by:

1. (8) $(\varphi \vee \psi )\approx \neg (\neg \varphi \wedge \neg \psi )$ .

Why should these facts be important? Because, Wilhelm suggests, (1)–(5) are – I quote – ‘standard conditions for immediate partial grounding’ and (7) and (8) are ‘standard identity conditions for propositions’. (He does not claim that (6) is also a ‘standard condition’, but it seems clear that he thinks so.)

I grant that (1)–(5) have some intuitive pull (see my comments on ( $\bigwedge \prec$ ) in the discussion of Fritz’s puzzles above). But I am not sure they are standard. Wilhelm mentions Fine (2012a), Correia (2017) and Krämer (2018) as evidence that they are. Fine (2012a) explicitly talks about immediate grounding, and some of the things he says about it suggest indeed a picture on which (1)–(5) hold. By contrast, neither Correia (2017) nor Krämer (2018) talks about immediate grounding at all, and so it is tempting to think that they provide no evidence for Wilhelm’s claim. However, the logics in Correia (2017) and Krämer (2018) validate Fine’s (2012a) elimination rules for strict full grounding (see Figure 10), and we may charitably grant that these may be seen as vindicating, modulo a proper definition of immediate partial grounding, the principles under consideration.

Be that as it may, no one in the literature is vulnerable to Wilhelm’s attack. He says that (7) and (8) are standard identity conditions for propositions, but he does not give references to back his claim. Now, and that is what is important, none of those who can be seen as endorsing (1)–(5) has also endorsed (7) and (8). Take the papers mentioned in the previous paragraph. Correia (2017) has a theory featuring the operator $\approx$ , which is there taken to express identity between propositions. But the theory does not validate (7) and (8). Worse, on that theory, $(\varphi \wedge \psi )\approx \neg (\neg \varphi \vee \neg \psi )$ and $(\varphi \vee \psi )\approx \neg (\neg \varphi \wedge \neg \psi )$ never hold. Krämer 2018 also has the operator $\approx$ , taken to express sameness of content, but on his view $(\varphi \wedge \psi )\approx \neg (\neg \varphi \vee \neg \psi )$ and $(\varphi \vee \psi )\approx \neg (\neg \varphi \wedge \neg \psi )$ also never hold. If $\approx$ is understood as implying ground-theoretic equivalence, then on Fine (2021a) proof-theoretic account of grounding, $(\varphi \wedge \psi )\approx \neg (\neg \varphi \vee \neg \psi )$ must fail since $\varphi \wedge \psi$ and $\neg (\neg \varphi \vee \neg \psi )$ do not have the same strict full grounds; and for the same reason, $(\varphi \vee \psi )\approx \neg (\neg \varphi \wedge \neg \psi )$ must also fail.

Of course, (7) and (8) are validated in some logics – for instance in the logic advocated in Correia (2010) and in the logic determined by Fine’s (2012a) semantics given that $\approx$ is interpreted as factual identity. But as I argued in the previous section, these logics are at odds with (1), and they can be shown to be at odds with (2)–(5) in much the same way.

Thus we see that Wilhelm invokes mixed principles about grounding and propositional identity that belong to quite different general conceptions of these notions. It is therefore not surprising that the mix ends up being inconsistent.⁶⁵