A Simple Sequent Calculus for Weak Full Grounding

Abstract This paper investigates the logic of grounding, a non-causal explanatory relation. While the study of this field is flourishing, it is still in its early stages. This paper contributes to the literature by presenting $$\mathcal {G}_{\textbf{LWG}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>G</mml:mi> <mml:mi>LWG</mml:mi> </mml:msub> </mml:math> , a novel sequent calculus for weak full grounding. While it provides a sequent-style presentation of the existing axiomatic system $$\textbf{LWG}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LWG</mml:mi> </mml:math> proposed by Adam Lovett, our calculus is balanced and avoids the ad-hoc rules contained in $$\textbf{LWG}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LWG</mml:mi> </mml:math> . An important fact shown in this paper is that if a sequent $$\Gamma \Rightarrow \Delta $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>Γ</mml:mi> <mml:mo>⇒</mml:mo> <mml:mi>Δ</mml:mi> </mml:mrow> </mml:math> is derivable in $$\mathcal {G}_{\textbf{LWG}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>G</mml:mi> <mml:mi>LWG</mml:mi> </mml:msub> </mml:math> , then any variable occurring positively (or negatively) in $$\Gamma $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>Γ</mml:mi> </mml:math> also occurs positively (or negatively) in $$\Delta $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>Δ</mml:mi> </mml:math> . This highlights a deep connection between grounding and variable inclusion. This property, in particular, suggests a similarity to Rohan French’s sequent calculus for analytic containment, $$\mathcal {G}_{\textbf{AC}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>G</mml:mi> <mml:mi>AC</mml:mi> </mml:msub> </mml:math> . Indeed, we demonstrate that $$\mathcal {G}_{\textbf{LWG}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>G</mml:mi> <mml:mi>LWG</mml:mi> </mml:msub> </mml:math> is the negation dual of $$\mathcal {G}_{\textbf{AC}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>G</mml:mi> <mml:mi>AC</mml:mi> </mml:msub> </mml:math> . The paper concludes by proving the equivalence between $$\mathcal {G}_{\textbf{LWG}}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>G</mml:mi> <mml:mi>LWG</mml:mi> </mml:msub> </mml:math> and $$\textbf{LWG}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LWG</mml:mi> </mml:math> .