Ruitenburg's Theorem via Duality and Bounded Bisimulations

04/17/2018

∙

by   Luigi Santocanale, et al.

∙

0

∙

share

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 (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.