For a given intuitionistic propositional formula A and a propositional variable x occurring in it, define the infinite sequence of formulae { A i }i≥1 by letting A 1 be A and A i+1 be A(A i /x). Ruitenburg’s Theorem [8] says that the sequence { A i }i≥1 (modulo logical equivalence) is ultimately periodic with period 2, i.e. there is N ≥ 0 such that A N+2 ↔ A N is provable in intuitionistic propositional calculus. We give a semantic proof of this theorem, using duality techniques and bounded bisimulations ranks.

Ruitenburg's Theorem via Duality and Bounded Bisimulations / S. Ghilardi, L. Santocanale - In: Advances in Modal Logic / [a cura di] G. Bezhanishviii, G. D'Agostino, G. Metcalfe, T. Studer. - [s.l] : College Publications, 2018. - ISBN 9781848902558. - pp. 277-290

Ruitenburg's Theorem via Duality and Bounded Bisimulations

S. Ghilardi
;
2018

Abstract

For a given intuitionistic propositional formula A and a propositional variable x occurring in it, define the infinite sequence of formulae { A i }i≥1 by letting A 1 be A and A i+1 be A(A i /x). Ruitenburg’s Theorem [8] says that the sequence { A i }i≥1 (modulo logical equivalence) is ultimately periodic with period 2, i.e. there is N ≥ 0 such that A N+2 ↔ A N is provable in intuitionistic propositional calculus. We give a semantic proof of this theorem, using duality techniques and bounded bisimulations ranks.
Ruitenburg’s Theorem; Sheaf Duality; Bounded Bisimulations
Settore MAT/01 - Logica Matematica
2018
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
aiml18.pdf

accesso riservato

Tipologia: Pre-print (manoscritto inviato all'editore)
Dimensione 403.03 kB
Formato Adobe PDF
403.03 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
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/587094
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact