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

TL;DR

This paper introduces a novel nested sequent proof-search method with loop-checking for intuitionistic tense logics, enabling finite counter-model extraction and establishing the finite model property for certain ITLs.

Contribution

It presents a new loop-checking technique using homomorphisms and a generalized 'computation tree' structure to handle non-invertible rules in proof-search for ITLs.

Findings

Supports finite counter-model extraction for ITLs.

Establishes the finite model property for ITLs of the form IKt + A.

Introduces a loop-checking method based on homomorphisms.

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}.