A Direct Characterisation of Logical Grounds and a Decidability Proof

TL;DR

The paper addresses formalizing logical grounding and proving the decidability of the grounding relation. It introduces a standard grounding calculus $\mathbf{G}$ over the language $\mathcal{L}$ and a direct syntactic-tree based characterization using selection trees and grounding bars. The central result is that a grounding claim $\{\alpha_1,\dots,\alpha_n\}<\alpha$ is provable in $\mathbf{G}$ if and only if $\{\alpha_1,\dots,\alpha_n\}$ is the union of grounding bars for $\alpha$, which yields a finite, decidable procedure to enumerate all grounds. The authors prove soundness and completeness of the characterization and discuss the role of disjunction-star rules and amalgamation, grounding the method in established grounding principles and providing a practical decision procedure for grounding relations.

Abstract

We present a standard calculus for logical grounding based on well-established grounding principles [Schnieder, 2011, Fine, 2012, Correia, 2014, Correia, 2024] and provide a very direct characterisation of the provable grounding claims exclusively relying on the syntactic tree of the grounded formula. The technical features of the characterisation imply that the grounding relation induced by the calculus is decidable.

Figures (4)

• Figure 1: $0$-premiss rules.
• Figure 2: Introduction rules.
• Figure 3: Elimination rules.
• Figure 4: Structural rules

Theorems & Definitions (11)

• Definition 2.1
• Definition 3.1: Positive and negative nodes of a syntactic tree
• Definition 3.2: Feeble nodes of a syntactic tree
• Definition 3.3: Selection tree
• Definition 3.4: Grounding bar
• Theorem 3.1
• Theorem 3.2
• Theorem 3.3
• proof
• Theorem 3.4