Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Denotational semantics for languages of epistemic grounding based on Prawitz's theory of grounds

Antonio Piccolomini d'Aragona

TL;DR

This paper develops a hierarchical, denotational framework for epistemic grounding inspired by Prawitz's theory of grounds ($ToG$). It defines languages of grounding whose terms denote constructive grounds and operations via a composition-friendly denotation that preserves the structure of ground-objects and their justification procedures, and it analyzes properties such as canonical closure and universal denotation under language expansions. The work connects to Curry–Howard and Martin-Löf-type formalisms while maintaining a distinctive epistemic focus: grounds as both evidence and denotation of proof objects, not mere truth-makers, and operations that model inference as justification procedures. It also examines correctness, completeness, recognisability, and conservativity, including the impact of expansion choices on denotation and the status of Prawitz's completeness conjecture in light of Piecha and Schroeder-Heister's results. The framework lays groundwork for extending to formulas and model-theoretic semantics, offering a rigorous, scalable account of how epistemic grounding can be formalized and studied across expanding languages.

Abstract

We outline a class of term-languages for epistemic grounding inspired by Prawitz's theory of grounds. We show how denotation functions can be defined over these languages, relating terms to proof-objects built up of constructive functions. We discuss certain properties that the languages may enjoy both individually (canonical closure and universal denotation) and with respect to their expansions (primitive/non-primitive and conservative/non-conservative expansions). Finally, we provide a ground-theoretic version of Prawitz's completeness conjecture, and adapt to our framework a refutation of this conjecture due to Piecha and Schroeder-Heister.

Denotational semantics for languages of epistemic grounding based on Prawitz's theory of grounds

TL;DR

This paper develops a hierarchical, denotational framework for epistemic grounding inspired by Prawitz's theory of grounds (). It defines languages of grounding whose terms denote constructive grounds and operations via a composition-friendly denotation that preserves the structure of ground-objects and their justification procedures, and it analyzes properties such as canonical closure and universal denotation under language expansions. The work connects to Curry–Howard and Martin-Löf-type formalisms while maintaining a distinctive epistemic focus: grounds as both evidence and denotation of proof objects, not mere truth-makers, and operations that model inference as justification procedures. It also examines correctness, completeness, recognisability, and conservativity, including the impact of expansion choices on denotation and the status of Prawitz's completeness conjecture in light of Piecha and Schroeder-Heister's results. The framework lays groundwork for extending to formulas and model-theoretic semantics, offering a rigorous, scalable account of how epistemic grounding can be formalized and studied across expanding languages.

Abstract

We outline a class of term-languages for epistemic grounding inspired by Prawitz's theory of grounds. We show how denotation functions can be defined over these languages, relating terms to proof-objects built up of constructive functions. We discuss certain properties that the languages may enjoy both individually (canonical closure and universal denotation) and with respect to their expansions (primitive/non-primitive and conservative/non-conservative expansions). Finally, we provide a ground-theoretic version of Prawitz's completeness conjecture, and adapt to our framework a refutation of this conjecture due to Piecha and Schroeder-Heister.
Paper Structure (37 sections, 10 theorems)

This paper contains 37 sections, 10 theorems.

Table of Contents

  1. Keywords
  2. Introduction
  3. General overview
  4. Forms of judgments and assertions
  5. Bases and (operational) types
  6. Summary scheme
  7. Relations with other approaches
  8. Preliminary definitions: bases and types
  9. First-order logical languages
  10. Bases
  11. Atomic systems
  12. Atomic bases
  13. Operational types
  14. Grounds and operations on grounds
  15. Grounds
  16. ...and 22 more sections

Key Result

Proposition 9

Let $\mathfrak{B}$ be an atomic base, and let $f(\underline{x}, \xi^{\tau_1}, ..., \xi^{\tau_n})$ be a $\mathfrak{B}$-operation on grounds of operational type $\tau_1, ..., \tau_n \rhd \tau_{n + 1}$. Then, for every $h_i(\underline{x}_i, \xi^{\tau^i_1}, ..., \xi^{\tau^i_{m_i}})$ ground on $\mathfrak where Moreover, if the composition of $f$ with $h_i$ is defined on $v \geq 0$ individuals, for any

Theorems & Definitions (38)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Definition 8
  • Proposition 9
  • Definition 10
  • ...and 28 more