Avron`s (propositional) self-extensional four-valued paradefinite logic, referred to here as A4 in a Gentzen-type sequent calculus style, is re-investigated. The logic A4 is known to be the unique self-extensional extension of Dunn-Belnap logic (also referred to as Belnap-Dunn logic) by adding classical implication. It is observed that A4 is the classical-negation-free fragment of De and Omori's axiomatic extension BD+ of Dunn-Belnap logic by adding classical negation and classical implication. Theorems for embedding A4 into a Gentzen-type sequent calculus LK for propositional classical logic (with classical negation) are proved, and the completeness (with respect to a valuation semantics) and cut-elimination theorems for A4 are obtained using these embedding theorems. Similar theorems are also obtained for an extension A4c of A4 by adding conflation.
展开▼
