Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)

TL;DR

This paper introduces a linear nested sequent calculus for tense logic Kt, enabling backward proof-search, counter-model construction, and cut-elimination, and extends to symmetric modal logic KB.

Contribution

It presents the first linear nested sequent calculus for tense logic Kt with proof-theoretic properties and minimal nesting, also deriving a cut-free calculus for KB.

Findings

Enables backward proof-search and counter-model construction

Provides a syntactic cut-elimination procedure

Yields a cut-free calculus for symmetric modal logic KB

Abstract

We give a linear nested sequent calculus for the basic normal tense logic Kt. We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut-elimination. Linear nested sequents thus provide the minimal amount of nesting necessary to provide an adequate proof-theory for modal logics containing converse. As a bonus, this yields a cut-free calculus for symmetric modal logic KB.