No Future without (a hint of) Past: A Finite Basis for ‘Almost Future‿Temporal Logic

详细信息    查看全文

• 作者：Dorit Pardo (Ordentlich) ; ^{dorit.pardo@gmail.com" class="auth_mail" title="E-mail the corresponding author} ; Alexander Rabinovich ; ^{rabinoa@post.tau.ac.il" class="auth_mail" title="E-mail the corresponding author}
• 刊名：Information and Computation
• 出版年：2016
• 出版时间：April 2016
• 年：2016
• 卷：247
• 期：Complete
• 页码：203-216
• 全文大小：427 K

文摘

Kamp's theorem established the expressive completeness of the temporal modalities Until and Since for the First-Order Monadic Logic of Order (FOMLO) over real and natural time flows. Over natural time, a single future modality (Until) is sufficient to express all future FOMLO formulas. These are formulas whose truth value at any moment is determined by what happens from that moment on. Yet this fails to extend to real time domains: here no finite basis of future modalities can express all future FOMLO formulas. In this paper we show that finiteness can be recovered if we slightly soften the requirement that future formulas must be totally past-independent: we allow formulas to depend just on the arbitrarily recent past, and maintain the requirement that they be independent of the rest – actually – of most of the past. We call them ‘almost future’ formulas, and show that there is a finite basis of almost future modalities which is expressively complete (over all Dedekind complete time flows) for the almost future fragment of FOMLO.