AN EMBEDDING-BASED COMPLETENESS PROOF FOR NELSON'S PARACONSISTENT LOGIC
Norihiro Kamide · 2010
It is known that a syntactical embedding theorem of Nelson’s paraconsistent logic N4 into the positive intuitionistic logic LJ is useful to show the cut-elimination and decidability theorems for N4. In this paper, a semantical embedding theorem of N4 into LJ is shown. An alternative proof of the Kripke-completeness theorem for N4 is obtained by combining both the syntactical and semantical embedding theorems. Thus, the completeness, cut-elimination and decidability theorems can uniformly be obtained from these embedding theorems. A singleconsequence Kripke semantics for N4 is also addressed based on a modication of the semantical embedding theorem.