New Work for a (Formal) Theory of Grounds

Abstract: In this talk, I provide two different models for a theory of grounds meeting the following desiderata:\(\def\yright{\succ}\)

1. Grammar: There are objects, which we call grounds, which can be grounds for propositions or grounds against propositions.
2. Derivation: A derivation of a sequent \(X\yright A,Y\) gives us a systematic way to construct a ground for \(A\) out of grounds for each member of \(X\) and grounds against each member of \(Y\), and a derivation of a sequent \(X,A\yright Y\) gives us a systematic way to construct a ground against \(A\) out of grounds for each member of \(X\) and grounds against each member of \(Y\). So, a derivation of \(\yright A\) gives us a way to construct a ground for \(A\), and a derivation of \(A\yright\) gives us a way to construct a ground against \(A\).
3. Interpretation: This theory can be interpreted in an epistemic sense, where grounds are our means to access the truth or falsity of a proposition, or a metaphysical sense, where grounds show how a proposition is made true by the world.
4. Grasp: Grounds are the kinds of things we can possess.
5. Hyperintensionality: Not every ground is a ground for every tautology. A ground for \(A\) need not also be a ground for each logical consequence of \(A\).
6. Structure: A ground for \(A\to B\) can be seen as a function from grounds for \(A\) to grounds for \(B\). A ground for \(A\land B\) can be seen as consisting of a ground for \(A\) and a ground for \(B\). A ground against \(A\lor B\) can be seen as consisting of a ground against \(A\) and a ground against \(B\). A ground for \(\neg A\) can be obtained from a ground against \(A\), and a ground against \(\neg A\) can be obtained from a ground for \(A\).

The result is a model of grounds with significant similarities to the BHK interpretation of constructive logic, but for the classical sequent calculus.

• This is a talk for the Melbourne Logic Seminar.

• The slides of the talk are available here.