Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The proof theory and semantics of second-order (intuitionistic) tense logic

Justus Becker, Anupam Das, Sonia Marin, Paaras Padhiar

TL;DR

The paper develops a comprehensive framework for second-order tense logic over both intuitionistic and classical bases, combining syntax, two-sorted semantics, and labelled proof theory. It shows that axiomatisations, (bi)relational semantics, and proof-search based completeness all coincide, with cut-admissibility established for corresponding calculi. Diamonds are definable from boxes using tense modalities, enabling a coherent treatment of positive modalities within the second-order intuitionistic setting. Completeness results are achieved via a proof-search procedure that builds countermodels through Schütte-style semivaluations extended to impredicative comprehension, harmonizing semantic and syntactic perspectives. The work also connects to prior second-order modal logics and negative translations, and outlines future directions including fixed points, global modalities, and a Curry–Howard style interpretation.

Abstract

We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order logic is its capacity to define positive connectives from the negative fragment. Duly we are able to recover the diamond (and its associated theory) using only boxes, as long as we include both forward and backward modalities (`tense' modalities). We propose axiomatic, proof theoretic and model theoretic definitions of `second-order intuitionistic tense logic', and ultimately prove that they all coincide. In particular we establish completeness of a labelled sequent calculus via a proof search argument, yielding at the same time a cut-admissibility result. Our methodology also applies to the classical version of second-order tense logic, which we develop in tandem with the intuitionistic case.

The proof theory and semantics of second-order (intuitionistic) tense logic

TL;DR

The paper develops a comprehensive framework for second-order tense logic over both intuitionistic and classical bases, combining syntax, two-sorted semantics, and labelled proof theory. It shows that axiomatisations, (bi)relational semantics, and proof-search based completeness all coincide, with cut-admissibility established for corresponding calculi. Diamonds are definable from boxes using tense modalities, enabling a coherent treatment of positive modalities within the second-order intuitionistic setting. Completeness results are achieved via a proof-search procedure that builds countermodels through Schütte-style semivaluations extended to impredicative comprehension, harmonizing semantic and syntactic perspectives. The work also connects to prior second-order modal logics and negative translations, and outlines future directions including fixed points, global modalities, and a Curry–Howard style interpretation.

Abstract

We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order logic is its capacity to define positive connectives from the negative fragment. Duly we are able to recover the diamond (and its associated theory) using only boxes, as long as we include both forward and backward modalities (`tense' modalities). We propose axiomatic, proof theoretic and model theoretic definitions of `second-order intuitionistic tense logic', and ultimately prove that they all coincide. In particular we establish completeness of a labelled sequent calculus via a proof search argument, yielding at the same time a cut-admissibility result. Our methodology also applies to the classical version of second-order tense logic, which we develop in tandem with the intuitionistic case.
Paper Structure (46 sections, 57 theorems, 41 equations, 2 figures)

This paper contains 46 sections, 57 theorems, 41 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Background and motivation
  3. Contributions
  4. Related works
  5. Structure of the paper
  6. A second-order extension of tense logic
  7. Syntax of second-order tense logic
  8. A minimal axiomatisation
  9. On the underlying (first-order) modal and tense logics
  10. Classical theory
  11. Model theory: (bi)relational structures
  12. Two-sorted birelational semantics under full comprehension
  13. Two-sorted predicate semantics under full comprehension
  14. Two-sorted (uni)relational semantics under full comprehension
  15. Proof theory: labelled systems
  16. ...and 31 more sections

Key Result

Theorem 2.7

$\mathsf{IK} \mathsf{t} 2(\Diamond, \Diamondblack)$ (and so all its extensions) proves:

Figures (2)

  • Figure 1: The 'grand tours' of this work.
  • Figure 2: Rules of the labelled system $\ell \mathsf{K}\mathsf t 2$ (with cut). Here a symbol is fresh if it does not occur in the lower sequent.

Theorems & Definitions (136)

  • Remark 2.1: Propositional symbols vs variables
  • Definition 2.2: Axiomatisation with diamonds
  • Remark 2.3: Full comprehension
  • Remark 2.4: Other logical operators
  • Remark 2.5: Minimality
  • Example 2.6: $\Box$ distributes over $\forall$
  • Theorem 2.7
  • proof
  • Definition 2.8
  • Example 2.9: Redundancy
  • ...and 126 more