Penn Arts & Sciences Logo

Logic and Computation Seminar

Tuesday, May 22, 2018 - 3:00pm

Daniyar Shamkanov

Steklov Mathematical Institute of RAS and HSE Faculty of Mathematics, Moscow


University of Pennsylvania

DRL 4E19

Cyclic and, more generally, non-well-founded proofs turn out to be an interesting alternative to traditional proofs for logics with fixed-point operators. Proof systems allowing such kind of proofs can be defined for the modal mu-calculus, the Lambek calculus with iteration, Peano arithmetic, and for other systems. In this talk, we consider a sequent calculus allowing non-well-founded proofs for the modal logic of transitive closure K+ and discuss a syntactic cut-elimination theorem for the given system.