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 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.

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.

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.

A consistent prepositional logic without any finite models

1985 ◽  
Vol 50 (1) ◽  
pp. 38-41 ◽  
Author(s):  
C. G. McKay
Keyword(s):  
Propositional Logic ◽  
Classical System ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Finite Models ◽  
Positive Logic ◽  
Usual Manner ◽  
Constructive Criticism ◽  
Infinite Set

Some propositional logics (e.g. the classical system) can be characterized by a finite model, while others (e.g. Heyting's) which have the finite model property (FMP) can be characterized by an infinite set of finite models. Still others (e.g. certain extensions of Heyting's logic) which lack the FMP can only be characterized by a set of models, at least one of which is infinite. Yet all these logics admit finite models even though they may not be characterized by them. (For example, they all admit the 2-element Boolean algebra as a model in the sense that all their theorems are valid on that algebra when the propositional connectives are interpreted in the usual manner.) The object of the present paper is to give a (not too artificial) example of a propositional logic which is consistent and which admits only infinite models. It therefore lacks the FMP in a very strong sense. Such a propositional logic, I shall call hyperinfinite. The existence of hyperinfinite logics was already plausible from a result in abstract algebra which says that there are varieties of algebras of which the only finite element is the trivial algebra (see [3]).I wish to thank Professor A. S. Troelstra, Amsterdam, for comments on an early version of this paper. The constructive criticism of two anonymous referees has also been useful.The hyperinfinite propositional logic to be described is obtained from Positive Logic—the negative-free part of Heyting's logic—by adjoining certain axioms which govern the use of a unary modal connective.

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.

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.

On the Modal μ-Calculus Over Finite Symmetric Graphs

2015 ◽  
Vol 65 (4) ◽  
Author(s):  
Giovanna D’Agostino ◽  
Giacomo Lenzi
Keyword(s):  
Lower Bound ◽  
Upper Bound ◽  
Satisfiability Problem ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
Symmetric Graphs ◽  
Trivial Consequence

AbstractIn this paper we consider the alternation hierarchy of the modal μ-calculus over finite symmetric graphs and show that in this class the hierarchy is infinite. The μ-calculus over the symmetric class does not enjoy the finite model property, hence this result is not a trivial consequence of the strictness of the hierarchy over symmetric graphs. We also find a lower bound and an upper bound for the satisfiability problem of the μ-calculus over finite symmetric graphs.

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.

Sign in / Sign up

Export Citation Format

Share Document