I would like to discuss the following formalization of the Russel
paradox in my proof checking system VEDA (the main ideas of the VEDA
project were described in my paper "MSL - a Mathematical Specification
Language" published in Lecture Notes in Computer Science, vol.620 (1992),
pp. 303-313; the system VEDA just began to work in an experimental mode
on an IBM PC; this example was checked for a few seconds).
-- The Russel paradox ("--" means "comment")
[ -- typically an input to the VEDA system is a sequence of terms.
--in VEDA everything (a definition, a proof , ...) is a term.
-- Brackets "[", "]" are used in VEDA for building of sequences
-- and some other terms (including some definitions).
x : set; -- x is defined as a variable x
-- of the predefined type "set";
def[ R; set; -- R is defined as a constant of the type "set";
x in R == ~(x in x) ]; -- the defining axiom for R;
-- Checking this definition the system examines the defining axiom
-- and after discovering that the axiom is not of some simple form
-- which secures consistency of the axiom, the system looks in the
-- accessible part of the system data base for a true formula of the form
-- E[r:set, y in r == ~(y in y) ]; (y is a variable of the type "set")
-- and since there is no such a formula in the data base, the system
-- displays a warning message and marks this definition as "bad".
-- Note that bad definitions are forbidden inside proofs.
proof([ false; -- "false" is the formula to be proved; the system places
-- the formula into a local list Unproved;
P := R in R == ~(R in R); -- ":=" means "denotes";
-- checking the formula P, the system discovers that the name R is
-- defined in a bad definition and places R into the list Badnames.
!P; -- "!P" means that the formula P must be proved by the system using
-- accessible axioms and theorems (including formulas previously
-- proved in the proof) - in this case the system proves P by
-- discovering that P is unifiable with the defining axiom for R.
!(P == false); -- the system proves the formula "P == false" by simplifying
-- the formula (using the true formulas "(a == ~a) == false"
-- and "b == b" fron the system data base).
subst(false, P == false, P); -- subst(Q, E, H) is an inference rule used
-- when the formula E is a true formula of the form
--" m = n" or "m == n" and the formula Q is the result
-- of replacement in the formula H all subterms m on n.
-- If it is so then the formula Q will be true if H is true.
-- Here the system removes the formula "false" from the
-- list Unproved.
]) -- 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?