Proof that setof x is a characteristic function

Proof that `setof x` is a characteristic function

In order to prove that setof is one-to-one, we use Art Quaife's technique of weighting variables so that clauses containing variables will be discarded immediately. Quaife used this method [4] in his development of Goedel-Bernays set theory. He used it, as we do here, to prove universally quantified sentences, i. e. to refute existentially quantified sentences, i. e. to show that some "bad" constant does not exist. In TRC, this technique is even more widely applicable, since any stratified sentence can be rewritten as an equivalent equation or inequation between constant terms. ***JUSTIFY

weight_list(pick_and_purge).
weight(x,1000).
end_of_list.


----> UNIT CONFLICT at   0.35 sec ----> 166 [binary,165.1,108.1] $F.

Length of proof is 4.  Level of proof is 2.

Proof



30 [reference] charq xf=p1|xf noteq(isp1 xf,xf) !=p1.
31 [reference] charq xf=p1|xf noteq(isp1 xf,xf) !=p2.
34 [reference] p2 xy!=xf (p1 xy) |setof xf xy =p1.
35 [reference] p2 xy=xf (p1 xy) |setof xf xy =p2.
36 [assumption to refute] charq (setof bad)!=p1.
39 [ur,36,31] setof bad noteq(isp1 (setof bad),setof bad)!=p2.
40 [ur,36,30] setof bad noteq(isp1 (setof bad),setof bad)!=p1.
108 [ur,39,35,flip.1] bad (p1 noteq(isp1 (setof bad),setof bad))=p2 noteq(isp1 (setof bad),setof bad).
165 [ur,40,34,flip.1] bad (p1 noteq(isp1 (setof bad),setof bad))!=p2 noteq(isp1 (setof bad),setof bad).
166 [binary,165.1,108.1] $F.

up show outline