Key points are not available for this paper at this time.
In 1949 Nelson 5 proposed a constructive logic in which falsity is conceived in a fashion analogous to that for intuitionistic truth. The predicate calculus N (for strong negation) was characterized by the usual axioms and rules for positive intuitionistic connectives (see Kleene 4, p. 82, la–7 and 9–12), with the additional axiom schemata for strong negation: A ⊃ (¬A ⊃ B), Nelson's paper showed that N may be interpreted with concepts for constructive truth ( P -realizability) and falsity ( N -realizability). The paper also gave mappings between the intuitionistic and strong negation systems of arithmetic. These mappings are easily adapted to pure predicate calculus. One shows that intuitionistic predicate calculus I is a subsystem of N by reading the intuitionistic negation of A as A ⊃ B & ¬B in N . It is possible to map N into a subsystem of I using the definition of A′ in 5, p. 19 changing only the definition of (¬A)′ for atomic A to A ⊃ B & ¬B.
Almukdad et al. (Thu,) studied this question.