A nontrivial model of Weydert's SF3 minus the Leibniz rules

We consider the positive set theory "Strong Frege 3" (SF3) proposed by E. W eydert and discussed in [5]. SF3 is a "three valued" set theory where two b inary 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 give n 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 e lement of)over bar>, and a comprehension scheme for those first order formu las 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 v ie 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 t he trivial relation which identifies everything. The construction uses an a d hoc calculus c Delta(3), which is a typed, three-valued variant of the Fi tch combinatory logic C Delta (see [1]).