

Symposium on logic and computability "Logic and Computation Day"
June 7, 2013 12:15–13:00, Moscow, Steklov Mathematical Institute of RAS






Circular proofs for provability logic
D. S. Shamkanov^{} ^{} Steklov Mathematical Institute of the Russian Academy of Sciences

Number of views: 
This page:  57 

Abstract:
We present a circular proof system for the GödelLöb provability logic GL. In contrast to the ordinary proofs, a circular proof can be formed from an ordinary derivation tree by identifying each open assumption with an identical interior sequent. We prove that the circular proofsystem is sound and complete with respect to the standard sequentstyle formulation of GL, that it is contractionfree and cutfree, and that its logical rules are invertible. As an application, we give a syntactic proof of Lyndon interpolation for GL.
Language: English

