Abstract

Nelson has presented a constructive arithmetic with a negation opera- tion () dierent from the ordinary intuitionistic one . In [5] he presents a variant of Kleene's realization semantics for intuitionistic arithmetic, and proves that relative to this interpretation the arithmetic language with { has the same expressive power as the usual intuitionistic one, and fact certain theories of arithmetic incorporating his negation are equivalent to corresponding systems of intuitionistic arithmetic. A Fitch style natural deduction formulation ) of the pure rst order logic that may be extracted, from Nelson's work may be obtained from that for intuitionistic rst order logic by rst dropping the intuitionistic rule of negation intro- duction and then adding rules guaranteeing the De Morgan equivalences, their quantier analogues, and the equivalence of anegated implication with the conjunction of its antecedent and the negation of its consequent. Given the De Morgan equivalences, conjunction and the existential quantier may he treated as dened operators