The logic of time is one of the most interesting modal logics, and its importance is widely acknowledged both for philosophical and formal reasons. In this thesis, we apply the method of internalisation of Kripke-style semantics into the syntax of sequent calculus to the proof-theoretical analysis of temporal logics. Sequent systems for different flows of time are obtained as modular extensions of a basic temporal calculus, through the addition of appropriate mathematical rules that correspond to the properties of temporal frames: a general and uniform treatment is thus achieved for a wide range of temporal logics. All the calculi enjoy remarkable structural properties, in particular are contraction and cut free. Linear discrete time is analysed by means of two infinitary calculi. The first is obtained by means of a rule with infinitely many premises, and the second through a new definition of provability which admits, under certain conditions, derivation trees with infinite branches. The first calculus enjoys the desired structural properties, but the presence of an infinitary rule is harmful for proof analysis. Two finitary systems are identified by replacing the infinitary rule with a weaker finitary rule, and by bounding the number of its premises, respectively. Corresponding, somehow complementary, conservativity results are proved with respect to adequate fragments of the original calculus. The second calculus stems from a closure algorithm which exploits the fixed-point equations for temporal operators and gives saturated sets of closure formulas from a given formula. Finitisation is obtained in the form of an upper bound to the proof-search procedure, and decidability follows as a major consequence.

Proof Analysis in Temporal Logic / B. Boretti ; M. Franchella. DIPARTIMENTO DI FILOSOFIA, 2009. 21. ciclo, Anno Accademico 2007/2008. [10.13130/boretti-bianca_phd2009].

Proof Analysis in Temporal Logic

B. Boretti
2009

Abstract

The logic of time is one of the most interesting modal logics, and its importance is widely acknowledged both for philosophical and formal reasons. In this thesis, we apply the method of internalisation of Kripke-style semantics into the syntax of sequent calculus to the proof-theoretical analysis of temporal logics. Sequent systems for different flows of time are obtained as modular extensions of a basic temporal calculus, through the addition of appropriate mathematical rules that correspond to the properties of temporal frames: a general and uniform treatment is thus achieved for a wide range of temporal logics. All the calculi enjoy remarkable structural properties, in particular are contraction and cut free. Linear discrete time is analysed by means of two infinitary calculi. The first is obtained by means of a rule with infinitely many premises, and the second through a new definition of provability which admits, under certain conditions, derivation trees with infinite branches. The first calculus enjoys the desired structural properties, but the presence of an infinitary rule is harmful for proof analysis. Two finitary systems are identified by replacing the infinitary rule with a weaker finitary rule, and by bounding the number of its premises, respectively. Corresponding, somehow complementary, conservativity results are proved with respect to adequate fragments of the original calculus. The second calculus stems from a closure algorithm which exploits the fixed-point equations for temporal operators and gives saturated sets of closure formulas from a given formula. Finitisation is obtained in the form of an upper bound to the proof-search procedure, and decidability follows as a major consequence.
2009
Proof theory ; labelled sequent calculus ; temporal logic
Settore M-FIL/02 - Logica e Filosofia della Scienza
FRANCHELLA, MIRIAM ANGELA GIOVANNA
Doctoral Thesis
Proof Analysis in Temporal Logic / B. Boretti ; M. Franchella. DIPARTIMENTO DI FILOSOFIA, 2009. 21. ciclo, Anno Accademico 2007/2008. [10.13130/boretti-bianca_phd2009].
File in questo prodotto:
File Dimensione Formato  
Tesi_B.Boretti.pdf

accesso aperto

Tipologia: Pre-print (manoscritto inviato all'editore)
Dimensione 800.89 kB
Formato Adobe PDF
800.89 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/64477
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact