, A nontrivial model of Weydert's $SF_3$ minus the Leibniz rules.

Abstract We consider the positive set theory "Strong Frege 3" (SF3) proposed by E. Weydert and discussed in [5]. SF3 is a "three valued" set theory where two binary predicates appear, is an element of and <(is an element of)over bar>, mutually exclusive, but none of whom is the negation of the other (so given the sets x and y there are three possibilities: either x is an element of y holds, or x<(is an element of)over bar>y holds, or both fail). SF3 gives the axiom of extensionality with respect to is an element of and <(is an element of)over bar>, and a comprehension scheme for those first order formulas which are built positively from x is an element of y, x<(is an element of)over bar>y, x = y and -(x = y) In this paper we build a model M, which we conjecture to satiefy SF3, and vie prove that M does satisfy SF3 but in the logic without Leibniz rules for equality; M is nontrivial in the sense that its equality relation is not the trivial relation which identifies everything. The construction uses an ad hoc calculus c Delta(3), which is a typed, three-valued variant of the Fitch combinatory logic C Delta (see [1]).