Proof Systems Combining Classical and Paraconsistent Negations |
| |
| Authors: | Norihiro Kamide |
| |
| Affiliation: | (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 等数据库收录！ |
|
