Penn Arts & Sciences Logo

Logic and Computation Seminar

Tuesday, May 15, 2018 - 3:00pm

Stepan L. Kuznetsov

Steklov Mathematical Institute of RAS, Moscow

Location

University of Pennsylvania

DRL 4C8

We consider action logic, i.e., the logic of residuated Kleene lattices (RKLs). An RKL is a lattice (preorder with meet and join) equipped with a multiplicative operation having left and right residuals and with the iteration operation (Kleene star). The Kleene star can be axiomatised in various ways. The strongest way is the *-continuous one, where it is axiomatised by an omega-rule or, equivalently, by a calculus with non-well-founded derivations. There is also a weaker definition of Kleene star, as the least fixpoint of an operator, usually multiplication by the element being iterated, in join with the unit, which corresponds to the induction base. We show that, however, this definition is in a sense not canonical: this fixpoint can be not a fixpoint for another natural operator, which multiplies its operand by the element being iterated on the left and on the right simultaenously (in join with the unit and the element being iterated, as induction base cases for the even and odd number of iterations, respectively). As a side-effect, this gives a concrete example of a formula that can be derived using the omega-rule, but not with the weak induction rule (before that, only a non-constructive proof of this was known). It also happens that these different fixpoint definitions (induction principles) naturally arise from considering circular fragments of the calculus with non-well-founded derivations.