Abstract

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 → , by adding the axiom of constant domain ∀x ∨ B) → ∀xA ∨ B, by adding ∨ , and by adding ¬¬; 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