New Work for a (Formal) Theory of Grounds

December 14, 2018

Abstract: In this talk, I provide two different models for a theory of grounds meeting the following desiderata:$$

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\succ 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\succ 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 $\succ A$ gives us a way to construct a ground for $A$, and a derivation of $A\succ$ 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\wedge B$ can be seen as consisting of a ground for $A$ and a ground for $B$. A ground against $A\vee B$ can be seen as consisting of a ground against $A$ and a ground against $B$. A ground for $\mathrm{\neg }A$ can be obtained from a ground against $A$, and a ground against $\mathrm{\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.