The finite model property in tense logic

1995 ◽  
Vol 60 (3) ◽  
pp. 757-774 ◽  
Author(s):  
Frank Wolter
Keyword(s):  
Modal Logics ◽  
Tense Logic ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Negative Results ◽  
Propositional Language ◽  
Positive Results

AbstractTense logics in the bimodal propositional language are investigated with respect to the Finite Model Property. In order to prove positive results techniques from investigations of modal logics above K4 are extended to tense logic. General negative results show the limits of the transfer.

scholarly journals On the Decidability of Intuitionistic Tense Logic without Disjunction

2020 ◽  
Author(s):  
Fei Liang ◽  
Zhe Lin
Keyword(s):  
Proof Theory ◽  
Tense Logic ◽  
Heyting Algebras ◽  
Finite Model ◽  
Algebraic Proof ◽  
Model Property ◽  
Algebraic Models ◽  
Finite Axiomatizability ◽  
Finite Model Property ◽  
Modal Operators

Implicative semi-lattices (also known as Brouwerian semi-lattices) are a generalization of Heyting algebras, and have been already well studied both from a logical and an algebraic perspective. In this paper, we consider the variety ISt of the expansions of implicative semi-lattices with tense modal operators, which are algebraic models of the disjunction-free fragment of intuitionistic tense logic. Using methods from algebraic proof theory, we show that the logic of tense implicative semi-lattices has the finite model property. Combining with the finite axiomatizability of the logic, it follows that the logic is decidable.

Decidability of interpretability logics ILM0 and ILW*

2017 ◽  
Vol 25 (5) ◽  
pp. 758-772 ◽  
Author(s):  
Luka Mikec ◽  
Tin Perkov ◽  
Mladen Vuković
Keyword(s):  
Open Problem ◽  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Filtration Method ◽  
Finite Model Property ◽  
Missing Link ◽  
Interpretability Logic

Abstract The finite model property is a key step in proving decidability of modal logics. By adapting the filtration method to the generalized Veltman semantics for interpretability logics, we have been able to prove the finite model property of interpretability logic ILM0 w.r.t. generalized Veltman models. We use the same technique to prove the finite model property of interpretability logic ILW* w.r.t. generalized Veltman models. The missing link needed to prove the decidability of ILM0 was completeness w.r.t. generalized Veltman models, which we obtain in this article. Thus, we prove the decidability of ILM0, which was an open problem. Using the same technique, we prove that ILW* is also decidable.

Simulating polyadic modal logics by monadic ones

2003 ◽  
Vol 68 (2) ◽  
pp. 419-462 ◽  
Author(s):  
George Goguadze ◽  
Carla Piazza ◽  
Yde Venema
Keyword(s):  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
First Order Definability

AbstractWe define an interpretation of modal languages with polyadic operators in modal languages that use monadic operators (diamonds) only. We also define a simulation operator which associates a logic Λsim in the diamond language with each logic Λ in the language with polyadic modal connectives. We prove that this simulation operator transfers several useful properties of modal logics, such as finite/recursive axiomatizability, frame completeness and the finite model property, canonicity and first-order definability.

An algebraic study of tense logics with linear time

1968 ◽  
Vol 33 (1) ◽  
pp. 27-38 ◽  
Author(s):  
R. A. Bull
Keyword(s):  
Linear Time ◽  
Propositional Calculus ◽  
Tense Logic ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Fourth Section ◽  
Classical Propositional Calculus ◽  
Axiom Systems ◽  
Time Linear

In [2] Prior puts forward a tense logic, GH1, which is intended to axiomatise tense logic with time linear and rational; he also contemplates the tense logic with time linear and real. The purpose of this paper is to give completeness proofs for three axiom systems, GH1, GHlr, GHli, with respect to tense logic with time linear and rational, real, and integral, respectively.1 In a fourth section I show that GH1 and GHlr have the finite model property, but that GHli lacks it.GH1 has the operators of the classical propositional calculus, together with operators P, H, F, G for ‘It has been the case that’, ‘It has always been the case that’, ‘It will be the case that’, ‘It will always be the case that’, respectively.

Note on a paper in tense logic

1969 ◽  
Vol 34 (2) ◽  
pp. 215-218 ◽  
Author(s):  
R. A. Bull
Keyword(s):  
Tense Logic ◽  
Finite Model ◽  
Model Property ◽  
Ordered Sets ◽  
Finite Model Property ◽  
Finite Models ◽  
Correct Proof

In [1, §4], my ‘proof’ that GH1 has the finite model property is incorrect; there are considerable obscurities towards the end of §1, particularly on p. 33; and I should have exhibited the finite models for GH1. In §1 of this paper I expand the analysis of the sub-directly irreducible models for GH1 which I give in §1 of [1]. In §2 I give a correct proof that GH1 has the finite model property. In §3 I exhibit these finite models as models on certain ordered sets.

scholarly journals A Finite Model Property for Gödel Modal Logics

2013 ◽  
pp. 226-237 ◽  
Author(s):  
Xavier Caicedo ◽  
George Metcalfe ◽  
Ricardo Rodríguez ◽  
Jonas Rogger
Keyword(s):  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property

scholarly journals New New Modification of the Subformula Property for a Modal Logic

2020 ◽  
Author(s):  
Mitio Takano
Keyword(s):  
Modal Logic ◽  
Natural Extension ◽  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Additional Axiom ◽  
Subformula Property

A modified subformula property for the modal logic KD with the additional axiom $\Box\Diamond(A\vee B)\supset\Box\Diamond A\vee\Box\Diamond B$ is shown. A new modification of the notion of subformula is proposed for this purpose. This modification forms a natural extension of our former one on which modified subformula property for the modal logics K5, K5D and S4.2 has been shown (Bull Sect Logic 30:115--122, 2001 and 48:19--28, 2019). The finite model property as well as decidability for the logic follows from this.

Sign in / Sign up

Export Citation Format

Share Document