An extension of negationless logic.
J. Kent Minichiello · Notre Dame Journal of Formal Logic · 1969
MINICHIELLO §1. Nelson [l] has provided a formalization of part of Griss' negationless mathematics [2].The logic Nelson devised uses a quantified implication {A zSx B) and a quantified disjunction (Σlx(A h . . ., A n )) as well as &, V, and 3.These connectives do not exhaust the possibilities for rendering each provable sequent of Nelson's Pi system as a provable formula: when given a sequent A u . . ., A m -» B l9 . . ., B n , we lack a corresponding closed formula to be read negationlessly as "for all x l9 . . ., Xk if A λ and . . .and A m , then B x or ... or B n ."Further, in Nelson's two most restricted predicate calculi there is no obvious way of forming Griss negation in several variables.If Ψ is a distinguishability relation and P(t lf ...,£») is a formula in which x h . . ., x n do not occur, then the Griss negation of P{tχ, . . ., t n ) should be read (( for all x u . . .,x n if H^i, -. ,x n )thenx 1 Φt 1 or . . .or Xn*U."We have defined a general connective which provides the lacking notation [3].Using the notation of [l] we give the definition and introduction rules for this connective.Let ~x be a non-empty list of distinct variables, Ψ a (possible empty) list of formulas, and Φ a non-empty list of formulas: then (Ψ Ώ~X Φ) is a formula.Introduction rules suitable toin which Γ does not contain any of ~x free, each variable of ~x (term of t) is free for the corresponding variable of Ί (x) in each formula of Π(^), ^(Ί) (^i(*), . ., B n (x)), if ϊl(x) {AS), . . ., 4.(0) is empty then the premise(s) not involving Φ(~x) (B^), . . ., J5 w (f)) is (are) omitted, Π(#) is a list of m formulas, Ψ(x) is a non-empty list of n formulas, etc.An additional premise