Cut-free proof systems for logics of weak excluded middle |
| |
Authors: | A Ciabattoni D M Gabbay N Olivetti |
| |
Affiliation: | (1) Dipartimento di Informatica, Università di Milano, Via Comelico, 39, Milano, Italy e-mail: ciabatto@dsi.unimi.it, IT;(2) Department of Computer Science, King’s College, Strand, London WC2R 2LS, UK e-mail: dg@dcs.kcl.ac.uk, GB;(3) Departimento di Informatica, Università di Torino, Corso Svizzera, 185, Torino, Italy e-mail: olivetti@di.unito.it, IT |
| |
Abstract: | In this work we perform a proof-theoretical investigation of some logical systems in the neighborhood of substructural, intermediate
and many-valued logics. The common feature of the logics we consider is that they satisfy some weak forms of the excluded-middle
principle. We first propose a cut-free hypersequent calculus for the intermediate logic LQ, obtained by adding the axiom *A∨**A to intuitionistic logic. We then propose cut-free calculi for systems W
n
, obtained by adding the axioms *A∨(A ⊕ ⋯ ⊕ A) (n−1 times) to affine linear logic (without exponential connectives). For n=3, the system W
n
coincides with 3-valued Łukasiewicz logic. For n>3, W
n
is a proper subsystem of n-valued Łukasiewicz logic. Our calculi can be seen as a first step towards the development of uniform cut-free Gentzen calculi
for finite-valued Łukasiewicz logics. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|