A Modal Proof Theory for Final Polynomial Coalgebras
by David Friggens and Robert Goldblatt
An infinitary proof theory is developed for modal logics whose
models are coalgebras of polynomial functors on the category of
sets. The canonical model method from modal logic is adapted to
construct a final coalgebra for any polynomial functor. The states of
this final coalgebra are certain ``maximal'' sets of formulas that have
natural syntactic closure properties.
The syntax of these logics extends that of previously developed
modal languages for polynomial coalgebras by adding formulas that
express the ``termination'' of certain functions induced by transition
paths. A completeness theorem is proven for the logic of functors which
have the Lindenbaum
property that every consistent set of formulas has a maximal extension.
This property is shown to hold if if the deducibility relation is
generated by countably many inference rules.
A counter-example to completeness is also given. This is a
polynomial functor that is not Lindenbaum: it has an uncountable
set of formulas that is deductively consistent but has no maximal
extension and is unsatisfiable, even though all of its countable subsets
are satisfiable.