A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic

Basic Information

• Paper ID: 2501.03297
• Title: A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
• Author: Antonio Piccolomini d'Aragona (Eberhard Karls Universität Tübingen)
• Classification: math.LO cs.LO
• Publication Date: January 2025 (arXiv preprint)
• Paper Link: https://arxiv.org/abs/2501.03297

Abstract

This paper investigates two approaches to proof-theoretic semantics (PTS): one based on argument structures and reducibility semantics of proofs, and another based on base semantics concerning consequence relations between formulas (sets) over atomic bases. The latter is further divided into a standard interpretation and a variant proposed by Sandqvist. The author establishes results that permit conversion between different approaches under appropriate conditions and analyzes the implications of these results for the completeness problem of recursive logical systems relative to the concept of proof-theoretic validity. The paper emphasizes the concept of base-completeness and analyzes it in conjunction with known completeness results for intuitionistic logic.

Research Background and Motivation

Problem Background

Proof-theoretic semantics (PTS) is a constructive semantic framework where the core concept is not truth values as in model theory, but rather proof. Three main monotonic proof-theoretic semantic approaches exist in this field:

1. Reducibility Semantics: Based on Prawitz's work, employing argument structures and reductions
2. Standard Base Semantics: Based on consequence relations between formulas over sets of atomic rules
3. Sandqvist Base Semantics: A variant of standard base semantics that employs elimination rules rather than introduction rules for disjunction

Research Motivation

1. Theoretical Unification: Understanding the relationships between the three approaches, particularly under what conditions they are equivalent
2. Completeness Problems: Exploring the completeness and incompleteness of intuitionistic logic (IL) under different proof-theoretic semantics
3. Constructive Spirit: Analyzing whether the transition from Prawitz's "witness-based" approach to the base semantics' "witness-free" approach loses constructive content

Existing Limitations

• Systematic comparison of relationships between the three approaches is lacking
• The concept of base-completeness has not been sufficiently studied
• Differences in how intuitionistic logic behaves under different frameworks require explanation

Core Contributions

1. Equivalence Results: Establishes complete equivalence between reducibility semantics and standard base semantics (Theorems 1-2)
2. Conditional Equivalence: Establishes conditional equivalence relations between reducibility semantics and Sandqvist base semantics (Theorem 4)
3. Base Incomparability: Proves that the Prawitz method and Sandqvist method are incomparable at the model level (Theorems 10-12)
4. Base-Completeness Theory: Develops the concept of base-completeness and proves its inconsistency for intuitionistic logic (Theorems 18-19)
5. Compactness of Derivation Principle: Introduces and analyzes the role of the compactness of derivation principle in proof-theoretic semantics

Detailed Methodology

Task Definition

The core task of this paper is to compare three proof-theoretic semantic approaches and analyze their impact on logical system completeness. Specifically, this includes:

• Establishing conversion conditions between different semantic methods
• Analyzing the consistency of the base-completeness concept
• Investigating incompleteness phenomena in intuitionistic logic

Theoretical Framework

Language and Atomic Bases

Language L is defined as:

X ::= p, q, r, s, t, ... | ⊥ | X ∧ X | X ∨ X | X → X

Atomic rules are defined inductively by levels:

• Level 0: Any atom is an atomic rule
• Level 1: Rules of the form A₁...Aₙ/A where all formulas are atoms
• Level κ+1: Rules of the form ℜ₁A₁...ℜₙAₙ/A

Base Semantics

Standard Base Semantics (Γ |=_{B,n} A):

1. When Γ = ∅:
   • A ∈ ATOM_L ⟹ ⊢_B A
   • A = B ∧ C ⟹ |={B,n} B and |={B,n} C
   • A = B ∨ C ⟹ |={B,n} B or |={B,n} C
   • A = B → C ⟹ B |=_{B,n} C
2. When Γ ≠ ∅ ⟹ ∀C ⊇ₙ B (|={C,n} Γ ⟹ |={C,n} A)

Sandqvist Base Semantics differs in the disjunction clause:

• A = B ∨ C ⟹ ∀C ⊇ₙ B ∀D ∈ ATOM_L (B |=ˢ_{C,n} D and C |=ˢ_{C,n} D ⟹ |=ˢ_{C,n} D)

Reducibility Semantics

Based on argument structures ⟨T, ⟨f, h, g⟩⟩, where:

• T is a finite rooted tree with nodes labeled by formulas
• f, h, g are resolution functions

n-Validity (⟨D, J⟩ is n-valid over B):

• When D is closed: if the conclusion is atomic, it reduces to a closed structure in DERB; otherwise it reduces to canonical form
• When D is open: for all σ, J⁺ ⊇ J, C ⊇ₙ B, if assumptions are valid over C, then Dσ is valid over C

Technical Innovations

1. Equivalence Proof Techniques: Establishing equivalence relations between different semantics through induction and acceptability clauses
2. Conditional Equivalence Framework: Introducing the concept of "global comparability" to handle cases of non-pointwise equivalence
3. Base Incomparability Analysis: Utilizing completeness/incompleteness differences to prove divergence of model classes
4. Compactness of Derivation Principle: Transforming the handling of infinite atomic bases into analysis of finite fragments

Experimental Setup

Theoretical Verification Methods

This paper primarily employs mathematical proof methods, verifying theoretical results through the following strategies:

1. Inductive Proofs: Structural induction on formula complexity and derivation length
2. Counterexample Construction: Using specific atomic bases (such as rule R) to demonstrate non-equivalence
3. Application of Known Results: Utilizing Sandqvist's completeness theorem and incompleteness results from Piecha et al.

Key Examples

Atomic Base {R}:

    A
  [B]   [C]
   D     D
   -------
      D

For certain A, B, C ∈ ATOM_L and each D ∈ ATOM_L.

This base satisfies: A |=ˢ_,2 B ∨ C, but A ⊭^α_,2 B ∨ C and A ⊭_,2 B ∨ C.

Experimental Results

Main Theorem Results

Equivalence Results

Theorems 1-2: Γ |={B,n} A ⟺ Γ |=^α{B,n} A and Γ |=ₙ A ⟺ Γ |=^α_n A

This establishes complete equivalence between reducibility semantics and standard base semantics.

Conditional Equivalence

Theorem 4: If ∀Γ ∀A ∀C ⊇ₙ B (Γ |=ˢ_{C,n} A ⟹ Γ |=^α_{C,n} A), then ∀Γ ∀A ∀C ⊇ₙ B (Γ |=^α_{C,n} A ⟹ Γ |=ˢ_{C,n} A)

Base Incomparability

Theorem 10: When n = 2, both the antecedent and consequent of Corollary 3 fail.

This means the Prawitz method and Sandqvist method are incomparable over 2-level atomic bases.

Base-Completeness Inconsistency

Theorem 18: IL is base-complete with respect to ⊩ₙ ⟺ ⊩ₙ enjoys the compactness of derivation principle and IL is complete with respect to ⊩ₙ

Corollaries 11-13: IL is not base-complete under any proof-theoretic semantics.

Important Corollaries

1. Sufficient Conditions for Conversion: Theorem 13 provides sufficient conditions for equivalence of two semantics
2. Incompleteness Transitivity: Equivalence results allow incompleteness results to transfer between different frameworks
3. Compactness Restrictions: Base-completeness requires "local" compactness, which conflicts with properties of certain semantics

Related Work

Historical Development

1. Prawitz (1965-1973): Established proof-theoretic semantics based on argument structures
2. Schroeder-Heister (2006): Developed standard base semantics
3. Sandqvist (2015): Proposed a variant with elimination-rule treatment of disjunction
4. Piecha et al. (2015-2019): Proved incompleteness results for intuitionistic logic

Positioning of This Paper's Contribution

• Unification: First systematic comparison of three major approaches
• Deep Analysis: Not only establishing equivalence but also analyzing conditions and reasons for non-equivalence
• Theoretical Extension: Introducing the concept of base-completeness and revealing its contradictory nature

Conclusions and Discussion

Main Conclusions

1. Structural Equivalence: Reducibility semantics and standard base semantics are structurally identical under given restrictions; the presence or absence of "witnesses" does not affect the constructive spirit
2. Conditional Unification: The Prawitz method and Sandqvist method can be compared at the global level, but diverge at the model level
3. Base-Completeness Paradox: Base-completeness is an inconsistent concept for intuitionistic logic, revealing deep structural features of proof-theoretic semantics
4. Role of Compactness: The compactness of derivation principle plays a crucial role in proof-theoretic semantics; its failure leads to completeness problems

Limitations

1. Finiteness Assumptions: Results primarily apply to finite formula sets; extension to infinite cases requires additional work
2. Level Restrictions: Some results are limited to specific levels of atomic bases, though the author indicates these restrictions can be removed
3. Degree of Constructivity: While equivalence is proven, precise characterization of "degree of constructivity" remains to be explored

Future Directions

1. More General Base Orders: Investigating similar results under more general atomic base ordering structures
2. Non-monotonic Extensions: Extending analysis to non-monotonic proof-theoretic semantics
3. Applied Research: Exploring applications of these theoretical results in concrete logical system design

In-Depth Evaluation

Strengths

1. Theoretical Depth: Provides important theoretical unification in proof-theoretic semantics, filling a long-standing gap
2. Technical Rigor: Sophisticated proof techniques, particularly in handling conditional equivalence and base incomparability
3. Deep Insights: The discovery of base-completeness inconsistency reveals essential features of proof-theoretic semantics
4. Clear Exposition: Complex technical content is well-organized with clear concept explanations

Weaknesses

1. Limited Practical Applicability: Primarily theoretical results with limited direct guidance for actual logical system design
2. Insufficient Examples: While key counterexamples are provided, more analysis of concrete application scenarios would be beneficial
3. Limited Philosophical Discussion: Discussion of philosophical implications of constructive semantics could be deeper

Impact

1. Theoretical Contribution: Provides important unifying framework for proof-theoretic semantics, likely to influence subsequent research in the field
2. Methodological Value: The established comparative methodology has reference value for other branches of logical semantics
3. Foundational Research: The revealed base-completeness paradox may prompt reconsideration of foundational concepts in proof-theoretic semantics

Applicable Scenarios

1. Theoretical Logic: Provides theoretical foundation for studying different proof-theoretic semantic methods
2. Logical System Design: Provides judgment criteria for selecting appropriate semantic frameworks
3. Constructive Mathematics: Provides tools for understanding semantic foundations of constructive reasoning

References

The paper cites core literature in the field, including:

• Prawitz's pioneering work 18-21
• Schroeder-Heister's base semantics theory 24-26
• Sandqvist's completeness results 22
• Piecha et al.'s incompleteness research 15-17
• Martin-Löf's type theory 9

These citations fully demonstrate the author's deep understanding of the field's development and comprehensive grasp of related work.

Overall Assessment: This is a high-quality theoretical logic paper making important contributions to proof-theoretic semantics, a specialized field. While technically demanding, it has significant value for understanding the semantic foundations of constructive logic. Both the theoretical unification work and the discovery of the base-completeness paradox are likely to have lasting impact.