Effective Completeness for S4.3.1-Theories with Respect to Discrete Linear Models

TL;DR

This paper develops an effective construction method for S4.3.1 modal theories, enabling the realization of models with linear order accessibility relations, advancing the computable model theory of modal logic.

Contribution

It introduces a new effective construction that extends previous methods to produce models with linear order accessibility relations for S4.3.1 theories.

Findings

Successfully effectivizes the completeness theorem for S4.3.1 with linear models

Extends previous effective Henkin-type constructions to linear order models

Provides a new technique for computable model construction in modal logic

Abstract

The computable model theory of modal logic was initiated by Suman Ganguli and Anil Nerode in [4]. They use an effective Henkin-type construction to effectivize various completeness theorems from classical modal logic. This construction has the feature of only producing models whose frames can be obtained by adding edges to a tree digraph. Consequently, this construction cannot prove an effective version of a well-known completeness theorem which states that every $\mathsf{S4.3.1}$-theory has a model whose accessibility relation is a linear order of order type $\omega$. We prove an effectivization of that theorem by means of a new construction adapted from that of Ganguli and Nerode.