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.

Tense logic for discrete future time

1970 ◽  
Vol 35 (1) ◽  
pp. 105-118 ◽  
Author(s):  
Patrick Schindler
Keyword(s):  
Propositional Calculus ◽  
Tense Logic ◽  
Finite Model ◽  
Logical System ◽  
Model Property ◽  
Future Time ◽  
Finite Model Property ◽  
Complete Basis ◽  
Image Position ◽  
Classical Propositional Calculus

Prior has conjectured that the tense-logical system Gli obtained by adding to a complete basis for the classical propositional calculus the primitive symbol G, the definitionsDf. F: Fα = NGNαDf. L: Lα = KαGα,and the postulatesis complete for the logic of linear, infinite, transitive, discrete future time. In this paper it is demonstrated that that conjecture is correct and it is shown that Gli has the finite model property: see [4]. The techniques used are in part suggested by those used in Bull [2] and [3]:Gli can be shown to be complete for the logic of linear, infinite, transitive, discrete future time in the sense that every formula of Gli which is true of such time can be proved as a theorem of Gli. For this purpose the notion of truth needs to be formalized. This formalization is effected by the construction of a model for linear, infinite, transitive, discrete future time.

On simple, weak and strong models of propositional calculi

1973 ◽  
Vol 74 (1) ◽  
pp. 1-9 ◽  
Author(s):  
Ronald Harrop
Keyword(s):  
Simple Model ◽  
Propositional Calculus ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Finite Structure ◽  
Propositional Calculi ◽  
Simple Models

In this paper we will be concerned primarily with weak, strong and simple models of a propositional calculus, simple models being structures of a certain type in which all provable formulae of the calculus are valid. It is shown that the finite model property defined in terms of simple models holds for all calculi. This leads to a new proof of the fact that there is no general effective method for testing, given a finite structure and a calculus, whether or not the structure is a simple model of the calculus.

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.

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.

On the Finite Model Property of Weak Intuitionistic Tense Logic

2021 ◽  
pp. 174-182
Author(s):  
Yu Peng ◽  
Zhe Lin ◽  
Fei Liang
Keyword(s):  
Tense Logic ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property

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.

Logics containing K4. Part I

1974 ◽  
Vol 39 (1) ◽  
pp. 31-42 ◽  
Author(s):  
Kit Fine
Keyword(s):  
Modal Logic ◽  
Recent Work ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Fourth Section ◽  
Negative Results ◽  
Intermediate Logics ◽  
Completeness Result ◽  
Background Material

There are two main lacunae in recent work on modal logic: a lack of general results and a lack of negative results. This or that logic is shown to have such and such a desirable property, but very little is known about the scope or bounds of the property. Thus there are numerous particular results on completeness, decidability, finite model property, compactness, etc., but very few general or negative results.In these papers I hope to help fill these lacunae. This first part contains a very general completeness result. Let In be the axiom that says there are at most n incomparable points related to a given point. Then the result is that any logic containing K4 and In is complete.The first three sections provide background material for the rest of the papers. The fourth section shows that certain models contain no infinite ascending chains, and the fifth section shows how certain elements can be dropped from the canonical model. The sixth section brings the previous results together to establish completeness, and the seventh and last section establishes compactness, though of a weak kind. All of the results apply to the corresponding intermediate logics.

Canonical rules

2009 ◽  
Vol 74 (4) ◽  
pp. 1171-1205 ◽  
Author(s):  
Emil Jeřábek
Keyword(s):  
Alternative Proof ◽  
Finite Model ◽  
Consequence Relations ◽  
Model Property ◽  
Finite Model Property ◽  
Admissible Rules ◽  
Superintuitionistic Logics ◽  
Canonical Formulas ◽  
Global Consequence

AbstractWe develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia theorem and the theory of modal companions to systems of multiple-conclusion rules or (unitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property.

Sign in / Sign up

Export Citation Format

Share Document