Re: SUO: Set/Class Distinction (fwd)
I wrote:
> ...it is not provable in general [in the SUMO]
> that x is in the class of A's if and only x is an A, i.e., formally, one
> can't in general prove, for any given condition A of the language
> containing the variable ?x, (iff A (instance ?x (KappaFn A))).
This is garbled. Let me say it right. Let A be a sentence in the
language of the SUMO, and let A[V1/V2] be the result of substituting an
occurrence of the (substitutable) variable V2 for every free occurrence
of V1 in A. Then, in the SUMO, one cannot in general prove:
(forall (V2)
(<=> (instance V2 (KappFn V1 A))))
A[V1/V2]
Notably, even though it appears that the Russell Class (KappaFn ?y (not
instance ?y ?y)) can be shown to exist in the SUMO (at least it would
appear so from the documentation for KappaFn), one can't prove (at
least, not if SUMO is consistent):
(forall (?x)
(<=> (instance ?x (KappaFn ?y (not instance ?y ?y)))
(not (instance ?x ?x)))),
from which would follow the inconsistent instantiation:
(<=> (instance R R)
(not (instance R R)))
where R is (KappaFn ?y (not (instance ?y ?y))). (This, of course, is
just Russell's Paradox.)
-chris
--
/\ ASCII ribbon | Chris Menzel -- http://philebus.tamu.edu/~cmenzel
\/ campaign | Philosophy Dept, Texas A&M University
/\ against | College Station, TX 77843-4237
/ \ HTML email. | voice: 979.845-5660 fax: 979.845.0458