A Modal Proof Theory for Polynomial Coalgebras

The abstract mathematical structures known as coalgebras are of increas-ing interest in computer science for their use in modelling certain types of data structures and programs. Traditional algebraic methods describe objects in terms of their construction, whilst coalgebraic methods describe objects in terms of their decomposition, or observational behaviour. The latter techniques are particularly useful for modelling infinite data struc-tures and providing semantics for object-oriented programming languages, such as Java. There have been many different logics developed for reasoning about coalgebras of particular functors, most involving modal logic. We define a modal logic for coalgebras of polynomial functors, extending Rößiger’s logic [33], whose proof theory was limited to using finite constant sets, by adding an operator from Goldblatt [11]. From the semantics we de-fine a canonical coalgebra that provides a natural construction of a final coalgebra for the relevant functor. We then give an infinitary axiomatiza-tion and syntactic proof relation that is sound and complete for functors constructed from countable constant sets. Acknowledgments I am deeply indebted to my supervisor, Professor Robert Goldblatt, for pointing me in the right direction and keeping my wheels on the tracks. His mathematical advice is the best anyone could hope for. I would like to thank Ranald Clouston for many discussions on logic and life in general. This thesis (and my life in general) are the better for them. I would like to thank all the people at the Centre for Logic, Language and Computation at Victoria who have taught me through my undergrad-uate years for introducing me to the exciting world of logic. Financially, I have been supported by a scholarship from the Logic and Computation programme of the New Zealand Institute for Mathematics and its Applications. I am grateful for the hospitality of the Institute fo