Back from the future

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A∪B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and ẃ. This “ambivalent” nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in contrast, we make explicit this duality of until by introducing a new temporal operator ∇ that allows us to formalize the “history” of until, i.e., the “internal” universal quantification over the time instants between the current one and ẃ. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system N for a linear-time logic LTL∇ endowed with the new history operator. We show that LTL∇ is equivalent to the linear temporal logic LTL with until, which follows by formalizing back and forth translations between the two logics. We also define an indirect translation from LTL∇ into LTL via temporal logics with past operators; such a result provides an upper bound to the problem of satisfiability for LTL∇ formulas.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.3166/jancl.20.241-277
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 46,483
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Past, present and future.Arthur Prior - 1967 - Revue Philosophique de la France Et de l'Etranger 157:476-476.
Basic Proof Theory.Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280-280.
Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.
Labelled Deductive Systems.Dov M. Gabbay - 1996 - Oxford University Press.
Logics of Time and Computation.Robert Goldblatt - 1990 - Studia Logica 49 (2):284-286.

View all 13 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Back From the Future.Andrea Masini, Lucio Vigano & Marco Volpe - 2010 - Journal of Applied Non-Classical Logics 20 (3):241-277.
Normative Ethics: Back to the Future.Thomas Hurka - 2004 - In Brian Leiter (ed.), The Future for Philosophy. Oxford University Press.
Future Contradictions.Jc Beall - 2012 - Australasian Journal of Philosophy 90 (3):547-557.
Continental Philosophy: Back to the Future.David Wood - 2012 - Southern Journal of Philosophy 50 (2):206-219.
Back to The Future.F. Siegel - 1987 - Télos 1987 (74):164-167.
Back to the Future: Art and its History.M. G. Bal - 1998 - Semiotica 3 (119):287-308.
Back to the Future.Harold Morowitz - 1996 - Complexity 1 (6):37-38.
Back to the Open Future1.Elizabeth Barnes & Ross P. Cameron - 2011 - Philosophical Perspectives 25 (1):1-26.
Back to the Future.Joan W. Scott - 2008 - History and Theory 47 (2):279–284.
Those Were the Days: Looking Back at the Future.I. de Beaufort - 1996 - Journal of Medical Ethics 22 (6):356-359.
Back to “The Self and the Future”.Jennifer E. Whiting - 1999 - Philosophical Topics 26 (1/2):441-477.


Added to PP index

Total views
10 ( #776,919 of 2,286,524 )

Recent downloads (6 months)
2 ( #595,991 of 2,286,524 )

How can I increase my downloads?


My notes

Sign in to use this feature