Thomas,

Thanks for bringing this to my attention! The proof in question (at
the DC Proof website) was written with an old version of DC Proof.
Currently, selection criteria for a subset s may not refer to s
itself. I discovered that if you allow such selections, as older
versions did, you would be able to "prove" that all sets are empty!
So it was back to the drawing board, as they say.

I will try to rewrite this important proof using the revised Subset
Rule.

Regards,
Dan


--- In dcproof@yahoogroups.com, Thomas Heye <1910-131@...> wrote:
>
> Hi list,
> looking at the proof regarding addition of natural numbers, it was
> stated that the subset rule had been used-- in particular the set s
> being constructed was referenced in the selection criteria.
>
> Maybe somebody can help me; what follows is the fragment of a
prrof I
> started. It's strange that the premise rule dialog accepted the
> selection criteria for the set s; nevertheless, when I entered the
> part after ")a,b= in n2" in the subset dialog, DCProof complained
> about an "invalid reference to s".
>
> Of course, I can work on the proof with that new premise, but I'm
not
> very fond of too many "nested blocks".
>
> Best regards,
>
> Thomas