Completeness over Kripke models of a cyclic proof system for game logic

Hoexum, Eline (2022) Completeness over Kripke models of a cyclic proof system for game logic. Master's Thesis / Essay, Mathematics.

Preview	Text mMATH_2022_HoexumES.pdf.pdf Download (425kB) | Preview
	Text toestemming.pdf Restricted to Registered users only Download (128kB)

Abstract

Game logic is a modal logic introduced by Rohit Parikh for reasoning about the outcomes that players can achieve in 2-player games. The language of game logic is usually interpreted over monotone neighbourhood models, but it can also be interpreted through Kripke semantics, which means the atomic games are interpreted as 1-player games. Parikh also gave a Hilbert-style proof system Par for game logic and it was shown by Enqvist et al. that this system is complete over monotone neighbourhood models. For their proof, they defined the proof systems CloM, CloG and G, which are used as intermediate systems to connect Par to a cyclic sequent system Clo, which is known to be complete. In the process, all of these systems are shown to be complete over monotone neighbourhood models. As game logic can also be interpreted over Kripke models, it is natural to wonder whether the proof systems defined by Enqvist et al. can be adapted to be complete over Kripke models. In this thesis, we adapt CloG into a new cyclic sequent system for game logic and we show that this system is complete over Kripke models. We do this by giving a validity-preserving translation from game logic to the modal μ-calculus and then defining a transformation from Clo to our new system.

Item Type:	Thesis (Master's Thesis / Essay)
Supervisor name:	Hansen, H.H. and Sterk, A.E.
Degree programme:	Mathematics
Thesis type:	Master's Thesis / Essay
Language:	English
Date Deposited:	15 Jul 2022 12:33
Last Modified:	15 Jul 2022 12:33
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/27849

Actions (login required)

View Item