A modal sequent calculus for a fragment of arithmetic

✍ Scribed by G. Sambin; S. Valentini

• Publisher: Springer Netherlands
• Year: 1980
• Tongue: English
• Weight: 657 KB
• Volume: 39
• Category: Article
• ISSN: 0039-3215
• DOI: 10.1007/bf00370323

✦ Synopsis

Global properties of canonical derivability predicates (the standard example is Pr( ) in Peano Arithmetic) are studied here by means of a suitable propositional modal logic GL. i whole book [1] has appeared on GIL and we refer to it for more information and a bibliography on GL. Here we propose a sequent calculus for GL and, by exhibiting a good proof procedure, prove that such calculus admits the eliminar of cuts. Most of standard results on GL are then easy consequences: completeness, decidability, ~initc model property, interpolation and thB fixed point theorem. * The second author holds a grant from the Consiglio Nazionale delle Ricerche, gruppo G.I~.S.A.G.A.