Towards an ill-founded proof system for intuitionistic linear temporal logic
Lide Grotenhuis, University of Amsterdam
Ill-founded and cyclic proof systems have proven to be fruitful alternatives to traditional, finitary proof systems when dealing with modal fixed point logics. The question arises whether ill-founded and cyclic systems can be also be designed for intuitionistic versions of these logics. In this talk, I will present ongoing research aimed at developing an ill-founded sequent calculus for intuitionistic linear temporal logic. In particular, I will focus on our attempt to show completeness of such a calculus using backwards proof search. This is joint work with Lukas Zenger, Bahareh Afshari and Graham Leigh.