Constructive predicate logic with strong negation and model theory (Q1104309)

Strong negation differs from intuitionistic (Heyting) negation in that, by the former but not the latter, \(\sim (A\wedge B)\) is equivalent to the derivability of either \(\sim A\) or \(\sim B\), and \(\sim \forall xA(x)\) is equivalent to \(\sim A(t)\). Intuitionistic negation, \(\neg\), may, however, be defined in terms of strong negation, as \(\neg A\equiv A\supset \sim A\). In this paper a first-order constructive logic with strong negation is defined. It is presented first axiomatically, and then a Kripke-type many-worlds semantics is defined for it (the key feature of which is that formulas are evaluated in two ways, both positively and negatively). Using Henkin-style techniques, the axiomatic system is proved consistent and complete with respect to the semantics, likewise theorems for compactness and the Löwenheim property, that A is valid iff A is valid in all models with denumerable parameters. In addition, it is shown to embed intuitionistic logic, H, within the present system, S, with strong negation, and also how to embed the present system, S, within classical logic, C.