> The Russel Paradox and the VEDA system
>
> I would like to discuss the following formalization of the Russel
> paradox in my proof checking system VEDA (the main ideas of the VEDA
>
> ..............
> ]) -- end the proof; at this point the system checks the list Unproved
> -- and discovers that it is empty. So the proof is accepted as valid
> -- but because the list Badnames is not empty, a warning message will
> -- be displayed.
> ] -- end the Russel paradox.
>
> I would be grateful for any comments.
>
> Dr. Victor Makarov makv@delphi.com
>
> P.S.
> Maybe Frege was so shocked by the paradox because his Begriffsschrift
> did not include any language constructs for definitions?
>
>
>
But you use constraint for axiom of substitution, which
make the set theory not natural.