We present a semantics for strong negation systems on the basis of the subformula property of the sequent calculus. The new models, called subformula models, are constructed as a special class of canonical Kripke models for providing the way from the cut-elimination theorem to model-theoretic results. This semantics is more intuitive than the standard Kripke semantics for strong negation systems.

David Nelson’s constructive logics with strong negation may beviewed as alternative paraconsistent logic. These logics have been developedbefore da Costa’s works. We address some philosophical aspects of Nelson’slogics and give technical results concerning Kripke models and tableau calculi. We also suggest possible applications of paraconsistent constructivelogics.