# Strong Completeness and the Finite Model Property for Bi-Intuitionistic Stable Tense Logics

## TL;DR

This paper introduces a Hilbert-style axiomatisation for Bi-Intuitionistic Stable Tense Logics, proves their strong completeness, and establishes the finite model property and decidability for certain classes.

## Contribution

It provides the first Hilbert-style axiomatization and strong completeness proof for BIST logics, along with results on finite model property and decidability.

## Key findings

- First Hilbert-style axiomatization of BIST logics
- Strong completeness established for BIST logics
- Finite model property and decidability proven for certain classes

## Abstract

Bi-Intuitionistic Stable Tense Logics (BIST Logics) are tense logics with a Kripke semantics where worlds in a frame are equipped with a pre-order as well as with an accessibility relation which is 'stable' with respect to this pre-order. BIST logics are extensions of a logic, BiSKt, which arose in the semantic context of hypergraphs, since a special case of the pre-order can represent the incidence structure of a hypergraph. In this paper we provide, for the first time, a Hilbert-style axiomatisation of BISKt and prove the strong completeness of BiSKt. We go on to prove strong completeness of a class of BIST logics obtained by extending BiSKt by formulas of a certain form. Moreover we show that the finite model property and the decidability hold for a class of BIST logics.