An Infinitary Sequent System for the Equational Theory of *-continuous Action Lattices

We present an infinitary logic ACT _ω in the form of a Gentzen-style sequent system, which is equivalent to the equational theory of *-continuous action lattices [9]. We prove the cut-elimination theorem for ACT _ω and, as a consequence, a theorem on the elimination of negative occurrences of *. This shows that ACT _ω is Π^0_1 , whence, by a result of Buszkowski [1], it is Π^0_1 complete.