Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents

Tim S. Lyon

Abstract

This paper develops a novel nested sequent proof-search methodology for intuitionistic tense logics (ITLs), supporting finite counter-model extraction. We introduce a new loop-checking method that detects repeating nested sequents using homomorphisms, thereby bounding the height of derivations during proof-search. Due to the non-invertibility of some inference rules, the algorithm does not construct a single derivation, but a generalized structure we call a 'computation tree.' We show how proofs and counter-models can be extracted from computation trees when proof-search succeeds or fails, respectively. This establishes the finite model property for each ITL of the form IKt + A with A a subset of {T,B,D}.

Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents

Abstract

This paper develops a novel nested sequent proof-search methodology for intuitionistic tense logics (ITLs), supporting finite counter-model extraction. We introduce a new loop-checking method that detects repeating nested sequents using homomorphisms, thereby bounding the height of derivations during proof-search. Due to the non-invertibility of some inference rules, the algorithm does not construct a single derivation, but a generalized structure we call a 'computation tree.' We show how proofs and counter-models can be extracted from computation trees when proof-search succeeds or fails, respectively. This establishes the finite model property for each ITL of the form IKt + A with A a subset of {T,B,D}.

Paper Structure

This paper contains 14 sections, 12 theorems, 14 equations, 5 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Paper Organization.
  4. Preliminaries
  5. Nested Sequent Systems
  6. Proof-Search and Decidability
  7. Computation Trees and Proof Extraction
  8. Detecting Repeats and Termination
  9. Counter-Model Extraction
  10. Concluding Remarks
  11. Supplement for Section \ref{['sec:systems']}
  12. Modal Rules.
  13. Supplement for Section \ref{['subsec:comp-trees']}
  14. Computation Tree.

Key Result

Lemma 2.4

Let $M$ be a model with $w,u \in W$. If $w \leq u$ and $M, w \vDash A$, then $M, u \vDash A$.

Figures (5)

  • Figure 1: Nested Sequent Rules.
  • Figure 2: Disjunctive branching rule $\mathsf{db}$.
  • Figure 3: Computation tree and proof extraction example.
  • Figure 4: Repeat example.
  • Figure 5: Failed proof-search and extracted counter-model.

Theorems & Definitions (42)

  • Definition 2.1: Frame
  • Definition 2.2: Model
  • Definition 2.3: Semantic Clauses
  • Lemma 2.4: Ewa86
  • Remark 3.1
  • Definition 3.2: Seq-Tree
  • Definition 3.3: Extended Semantics
  • Definition 3.4
  • Example 3.5
  • Definition 3.6: Nested Sequent System
  • ...and 32 more