Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Calculi of epistemic grounding based on Prawitz's theory of grounds

Antonio Piccolomini d'Aragona

TL;DR

A class of formal systems inspired by Prawitz's theory of grounds is defined, a semantics that aims at accounting for epistemic grounding, namely, at explaining why and how deductively valid inferences have the power to epistemically compel to accept the conclusion.

Abstract

We define a class of formal systems inspired by Prawitz's theory of grounds. The latter is a semantics that aims at accounting for epistemic grounding, namely, at explaining why and how deductively valid inferences have the power to epistemically compel to accept the conclusion. Validity is defined in terms of typed objects, called grounds, that reify evidence for given judgments. An inference is valid when a function exists from grounds for the premises to grounds for the conclusion. Grounds are described by formal terms, either directly when the terms are in canonical form, or indirectly when they are in non-canonical form. Non-canonical terms must reduce to canonical form, and two terms may be said to be equal when they converge towards equivalent grounds. In our systems these properties can be proved through rules distinguished according to whether they concern types or logic. Type rules involve type introduction and elimination, equality for application of operational symbols, and re-writing equations for non-canonical terms. The logic amounts to a sort of intuitionistic system in a Gentzen format. To conclude, we show that each system of our class enjoys a normalization property.

Calculi of epistemic grounding based on Prawitz's theory of grounds

TL;DR

A class of formal systems inspired by Prawitz's theory of grounds is defined, a semantics that aims at accounting for epistemic grounding, namely, at explaining why and how deductively valid inferences have the power to epistemically compel to accept the conclusion.

Abstract

We define a class of formal systems inspired by Prawitz's theory of grounds. The latter is a semantics that aims at accounting for epistemic grounding, namely, at explaining why and how deductively valid inferences have the power to epistemically compel to accept the conclusion. Validity is defined in terms of typed objects, called grounds, that reify evidence for given judgments. An inference is valid when a function exists from grounds for the premises to grounds for the conclusion. Grounds are described by formal terms, either directly when the terms are in canonical form, or indirectly when they are in non-canonical form. Non-canonical terms must reduce to canonical form, and two terms may be said to be equal when they converge towards equivalent grounds. In our systems these properties can be proved through rules distinguished according to whether they concern types or logic. Type rules involve type introduction and elimination, equality for application of operational symbols, and re-writing equations for non-canonical terms. The logic amounts to a sort of intuitionistic system in a Gentzen format. To conclude, we show that each system of our class enjoys a normalization property.
Paper Structure (32 sections, 7 theorems)

This paper contains 32 sections, 7 theorems.

Table of Contents

  1. Introduction
  2. Background: grounds and languages of grounding
  3. Gentzen-languages
  4. Background language and atomic base
  5. Basic Gentzen-language of grounding
  6. An enriched Gentzen-language
  7. A formal system of grounding over $\texttt{Gen}^\varepsilon$
  8. The system
  9. Typing rules
  10. Type introductions
  11. Type eliminations
  12. Equivalence rules
  13. Reflexivity, symmetry, transitivity, preservation of denotation
  14. Application of operational symbols to equivalent terms (and vice versa in the canonical case)
  15. Equations for computing non-canonical terms
  16. ...and 17 more sections

Key Result

Theorem 3

Let $U : \beta \in \texttt{TERM}_\texttt{Gen}$ with $FV^T(U) = \{\xi^{\alpha_1}, ..., \xi^{\alpha_n}\}$. Then $\xi^{\alpha_1} : \alpha_1, ..., \xi^{\alpha_n} : \alpha_n \vdash_{\texttt{GG}} U : \beta$.

Theorems & Definitions (21)

  • Definition 1
  • Definition 2
  • Theorem 3
  • proof
  • Definition 4
  • Definition 7
  • Definition 8
  • Definition 9
  • Definition 10
  • Definition 11
  • ...and 11 more