On the Decidability of Intuitionistic Tense Logic without Disjunction
Keyword(s):
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.
2015 ◽
Vol 25
(03)
◽
pp. 349-379
◽
Keyword(s):
Keyword(s):
1970 ◽
Vol 35
(1)
◽
pp. 105-118
◽
2009 ◽
Vol 74
(4)
◽
pp. 1171-1205
◽
Keyword(s):
1971 ◽
Vol 12
(1)
◽
pp. 69-74
◽