A Gabbay-Rule Free Axiomatization of T×W Validity

Authors: Di Maio M.C.¹; Zanardo A.²

Source: Journal of Philosophical Logic, Volume 27, Number 5, October 1998 , pp. 435-487(53)

Publisher: Springer

Buy & download fulltext article:

Price: $47.00 plus tax (Refund Policy)

Abstract:

The semantical structures called T×W frames were introduced in (Thomason, 1984) for the Ockhamist temporal-modal language, lagran _O, which consists of the usual propositional language augmented with the Priorean operators P and F and with a possibility operator diam . However, these structures are also suitable for interpreting an extended language, lagran _SO, containing a further possibility operator diam ^s which expresses synchronism among possibly incompatible histories and which can thus be thought of as a cross-history ‘simultaneity’ operator. In the present paper we provide an infinite set of axioms in lagran _SO, which is shown to be strongly complete forT×W-validity. Von Kutschera (1997) contains a finite axiomatization of T×W-validity which however makes use of the Gabbay Irreflexivity Rule (Gabbay, 1981). In order to avoid using this rule, the proof presented here develops a new technique to deal with reflexive maximal consistent sets in Henkin-style constructions.

Keywords: temporal logic; branching-time; synchronism; axiomatization

Language: English

Document Type: Regular paper

Affiliations: 1: Centro Studi San Salvador, Telecom Italia, San Marco 4826, I-30124 Venezia, Italy. E-mail: dimaio@cstudi.telecomitalia.it 2: Dipartimento di Matematica P. ed A., Via Belzoni 7, I-35131 Padova, Italy. E-mail: azanardo@euler.math.unipd.it

Publication date: 1998-10-01