Discrete Tense Logic with Infinitary Inference Rules and Systematic Frame Constants: A Hilbert-Style Axiomatization
1996 (English)In: Journal of Philosophical Logic, ISSN 0022-3611, E-ISSN 1573-0433, Vol. 25, no 1, 45-100 p.Article in journal (Refereed) Published
The paper deals with the problem of axiomatizing a system τ1 of discrete tense logic, where one thinks of time as the set Z of all the integers together with the operations +1 (“immediate successor”) and -1 (“immediate predecessor”). τ1 is like the Segerberg-Sundholm system W1 in working with so-called infinitary inference rules; on the other hand, it differs from W1 with respect to (i) proof-theoretical setting, (ii) presence of past tense operators and a “now” operator, and, most importantly, with respect to (iii) the presence in τ of so-called systematic frame constants, which are meant to hold at exactly one point in a temporal structure and to enable us to express the irreflexivity of such structures. Those frame constants will be seen to play a paramount role in our axiomatization of τ1.
Place, publisher, year, edition, pages
1996. Vol. 25, no 1, 45-100 p.
IdentifiersURN: urn:nbn:se:uu:diva-31572DOI: 10.1007/BF00357842OAI: oai:DiVA.org:uu-31572DiVA: diva2:59469