Proof Systems Combining Classical and Paraconsistent Negations |
| |
Authors: | Norihiro Kamide |
| |
Institution: | (1) Waseda Institute for Advanced Study, Waseda University, 1-6-1 Nishi Waseda, Shinjuku-ku, Tokyo 169-8050, Japan |
| |
Abstract: | New propositional and first-order paraconsistent logics (called L
ω
and FL
ω
, respectively) are introduced as Gentzen-type sequent calculi with classical and paraconsistent negations. The embedding
theorems of L
ω
and FL
ω
into propositional (first-order, respectively) classical logic are shown, and the completeness theorems with respect to simple
semantics for L
ω
and FL
ω
are proved. The cut-elimination theorems for L
ω
and FL
ω
are shown using both syntactical ways via the embedding theorems and semantical ways via the completeness theorems.
Presented by Yaroslav Shramko and Heinrich Wansing |
| |
Keywords: | Paraconsistent negation sequent calculus cut-elimination completeness |
本文献已被 SpringerLink 等数据库收录! |
|