One type of formal negationless systems (Q1080412)

A system of negationless predicate calculus (NPC) is formulated by a two- step procedure. First, a basis system (BS) is presented, then a criterion is given for identifying NPC-permissible deductions in BS. Intuitively, a deduction is NPC-permissible iff there are, in the intuitionistic sense, objects satisfying the conditions described by the premisses. This becomes the requirement that it be a theorem of BS that there are such objects. A Kripke semantics for NPC is given for which soundness and completeness is claimed, but not proved.