Kripke Completeness of First-Order Constructive Logics with Strong Negation
Ichiro Hasuo · Logic Journal of IGPL · 2003
This paper considers Kripke completeness of Nelson's constructive predicate logic N3 and its several variants. N3 is an extension of intuitionistic predicate logic Int by an contructive negation operator ∼ called strong negation. The variants of N3 in consideration are by omitting the axiom A → (∼A → B), by adding the axiom of constant domain ∀x(A(x) ∨ B) → ∀xA(x) ∨ B, by adding (A → B) ∨ (B → A), and by adding ¬¬(A ∨ ∼A); the last one we would like to call the axiom of potential omniscience and can be interpreted that we can eventually verify or falsify a statement, with proper additional information. The proofs of completeness are by the widely-applicable tree-sequent method; however, for those logics with the axiom of potential omniscience we can hardly go through with a simple application of it. For them we present two different proofs: one is by an embedding of classical logic, and the other by the TSg method, which is an extension of the tree-sequent method.