Universal set theory and three-valued logic
Tim Sweeney
turn set-defining characteristic functions into partial functions from
sets to the three-valued logic {T,F,bot}. This three-valued logic
extends classical logic in the obvious way with
and(T,bot)=or(F,bot)=bot, and(F,x)=F, or(T,x)=T, not(bot)=bot, so that
every truth function has a fixed point.
Obviously the law of excluded middle does not hold: or(a,not(a)) only
implies that a is T or bot. This gives the logic a constructive
character.
In my formulation, I identify each set with its characteristic
function from sets to {T,F,bot}. Thus given s:set, the membership of
an element x can be tested with s(x). In the general case, this is a
partial function, returning bot for some values. I call such sets
"partial sets", and sets whose characteristic function is in {T,F}
"total sets". Every set of ZF and NF is a total set, with this theory
admitting a strictly larger class of sets than either.
Russell's set R={s:set|not(s(s))} is then a partial set. All ZF sets
are elements of R, while some elements of NF are not elements of R,
while some new sets such as R itself are of undecidable membership.
I've translated the ZF axioms to this set theory, rephrasing them in
terms of characteristic functions and new for-all and there-exists
logic operators performing logical conjunction and disjunctions across
all elements of a characteristic functions. Everything appears to be
sound and avoids known paradoxes.
With the new axioms, it is easy to construct a bijection from the
universal set to its power set. Cantor's proof that |P(x)|>|x| for
all non-empty sets x proceeds by constructing C={a:x|not(P(x)(a)} and
using the law of excluded middle to derive a contradiction on its
membership in P(x). This goes away for lack of excluded middle,
leaving C a partial set which appears not to be constructively
contradictory.
The one worrying aspect of this approach is that it identifies sets
with characteristic functions from sets to logic values:
Set=Set->{T,F,bot}. I have only been able to develop an intuition of
such sets in a purely constructive way, by writing down a finite list
of possibly self-referential equations defining sets, and convincing
myself that a unique solution exists. This is much in the style of
NF's axiom that every (possibly cyclic) graph corresponds to a set,
but I allow unlimited comprehension.
Are there any known problems with this approach to set theory? Any
pointers to research on the topic?
Tim Sweeney
Hans Aberg
t...@epicgames.com (Tim Sweeney) wrote:
>One apparent way of avoiding the paradoxes of naive set theory is to
>turn set-defining characteristic functions into partial functions from
>sets to the three-valued logic {T,F,bot}.
...
>Are there any known problems with this approach to set theory? Any
>pointers to research on the topic?
While implementing a proof verification system, the strong three valued
logic of Kleene (see his book "Introduction to Metamathematics") emerged
to me naturally in the form of metamathematical provability. I use right
now Kleenean K = {f, u, t}, f = false, u = undecidable, t = true. (Three
valued logic has studied by others before Kleene, by he seems to be the
first to study this strong three valued logic in connection of algorithmic
decidability, so I named the type after him.)
The object logic remains the same old Boolean B = {f, t}. In classical
metamathematics all closed wff's (well formed formulas) are thought to be
true or false. The type K is then just used in order to express the fact
that some closed wff's are not practically provable to be true or false.
This perhaps does not immediately apply to your picture, but you might
want to look for a connection.
Hans Aberg
Aatu Koskensilta
> One apparent way of avoiding the paradoxes of naive set theory is to
> turn set-defining characteristic functions into partial functions from
> sets to the three-valued logic {T,F,bot}. This three-valued logic
> extends classical logic in the obvious way with
> and(T,bot)=or(F,bot)=bot, and(F,x)=F, or(T,x)=T, not(bot)=bot, so that
> every truth function has a fixed point.
>
> Obviously the law of excluded middle does not hold: or(a,not(a)) only
> implies that a is T or bot. This gives the logic a constructive
> character.
Not necessarily. It gives you partiality, but whether or not that has
anything to do with constructivity is another matter.
> In my formulation, I identify each set with its characteristic
> function from sets to {T,F,bot}. Thus given s:set, the membership of
> an element x can be tested with s(x). In the general case, this is a
> partial function, returning bot for some values. I call such sets
> "partial sets", and sets whose characteristic function is in {T,F}
> "total sets". Every set of ZF and NF is a total set, with this theory
> admitting a strictly larger class of sets than either.
>
> Russell's set R={s:set|not(s(s))} is then a partial set. All ZF sets
> are elements of R, while some elements of NF are not elements of R,
> while some new sets such as R itself are of undecidable membership.
>
> I've translated the ZF axioms to this set theory, rephrasing them in
> terms of characteristic functions and new for-all and there-exists
> logic operators performing logical conjunction and disjunctions across
> all elements of a characteristic functions. Everything appears to be
> sound and avoids known paradoxes.
Not knowing the details of your approach I can't verify it's
correctness, but I can give you the reassurance that the general idea is
not inherently contradictory.
> With the new axioms, it is easy to construct a bijection from the
> universal set to its power set. Cantor's proof that |P(x)|>|x| for
> all non-empty sets x proceeds by constructing C={a:x|not(P(x)(a)} and
> using the law of excluded middle to derive a contradiction on its
> membership in P(x). This goes away for lack of excluded middle,
> leaving C a partial set which appears not to be constructively
> contradictory.
>
> The one worrying aspect of this approach is that it identifies sets
> with characteristic functions from sets to logic values:
> Set=Set->{T,F,bot}. I have only been able to develop an intuition of
> such sets in a purely constructive way, by writing down a finite list
> of possibly self-referential equations defining sets, and convincing
> myself that a unique solution exists. This is much in the style of
> NF's axiom that every (possibly cyclic) graph corresponds to a set,
> but I allow unlimited comprehension.
Is this really NF's axiom? It sounds more like Aczel's non-well-founded
set theory.
> Are there any known problems with this approach to set theory? Any
> pointers to research on the topic?
I'm not sure this corresponds to exactly what you're interested in, but
there have been various more or less succesful attempts to use
partiality in order to "overcome" the difficulties of Frege-style theory
of classes. For one example, see Penelope Maddy's article Proper Classes
in Journal of Symbolic Logic in 1983 in which Maddy uses a construction
remiscient of Kripke's inductively constructed partial truth predicate
to "construct" from the class V a model for class theory in which there
is a universal class V, the Russell class, and for any predicate P the
class of all x satisfying P. The problems of Kripke's theory carry over,
however, so that if we define equality between classes as A=B <=> Ax(x
\in A <=> x \in B) we get funni things like the Russell set not being
identical to itself (and of course not being not-identical to itself
either), in analogy to the fact that in the Kripke fixed point models M
we have for all liar sentence L, not M |= L<=>L.
The idea behind Maddy's construction and related constructions is that
we begin with all classes being totally undetermined, i.e. if we
represent a class with a pair (A+,A-) where A+ and A- are disjoint
subclasses of the universe (subsets of the domain of a model of set
theory, if you wish) then to every class symbol {x | P(x,a_1,...,a_n)}
we associate the pair (emptyset,emptyset), and proceed in stages as
follows: at stage n+1 we assign to the class symbol {x |
P(x,a_1,...,a_n)} the pair (the p such that the model M_n says p
satisfies P(a_1,...,a_n), the p such that the model M_n says p does not
satisfy P(a_1,...,a_n)), and at limit ordinals l take for every class
the pair (union of A_a+ for all a <l, union of A_a- for all a < l).
(Here we use some partial truth function scheme to evaluate whether a
sentence holds in a model or does not. x \in {x | P(x,a_1,...,a_n)} is
true in M if and only if x \in {x | P(x,a_1,...,a_n)}+ and is false if
and only if x \in {x | P(x,a_1,...,a_n)}- so that at the first stage
membership in all classes is undecided). Finally, to get the actual
interpretation of A = {x | P(x,a_1,...,a_n)} we take the pair {union
over all ordinals a of A_a+, union over all ordinals a of A_a-).
If you're interested in the details (and there are numerous messy
details), you can look up a summary I wrote of Maddy's article found in
the message <bm9odp$2pq$1...@phys-news1.kolumbus.fi>. Of course, you should
also look up the original article.
It's noteworthy also that any theory of classes in the Fegean vein
corresponds to a theory of truth, and vice versa. I don't know if these
connections have been studied systematically - something I'm playing
around with these days.
For a general survey (which might be a bit out of date, but very useful
nevertheless) of attempts to create "type-free" theories of this sort
you should consult Feferman's Towards Useful Type Theories found in
Journal of Symbolic Logic circa 1988 if I'm not altogether mistaken.
You could mail me if you wish, and I could try to go trough my notes and
gather a list of references (something I should do one day anyways) for
you to look at.
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
Robin Chapman
>
> With the new axioms, it is easy to construct a bijection from the
> universal set to its power set.
How?
--
Robin Chapman, www.maths.ex.ac.uk/~rjc/rjc.html
"Needless to say, I had the last laugh."
Alan Partridge, _Bouncing Back_ (14 times)
Toni Lassila
<r...@ivorynospamtower.freeserve.co.uk> wrote:
>Tim Sweeney wrote:
>
>> With the new axioms, it is easy to construct a bijection from the
>> universal set to its power set.
>
>How?
He has no idea, but it's easy.
Tim Sweeney
> > universal set to its power set.
>
> How?
In a set theory with a universal set U and sufficient power to reason
about it, P(U)=U. So, the identity function is a suitable bijection.
If P(U)=U is controversial (given a set theory with a universal set
and no urelements), I would be interested in hearing so. I realize
that some universal set theories preclude analysis of P(U)=U on the
grounds of stratification, but if a theory allows one to reason about
P(U)=U then surely it must either be true or undecidable.
Note that Cantor's construction showing that for non-empty x,
|P(x)|>|x|, fails on such "large sets" as U: the set one constructs to
refute the possibility of a bijection involves negation and the law of
excluded middle, so the set membership relation of the refutation set
may be partial, and that partiality precludes the contradiction.
galathaea
: One apparent way of avoiding the paradoxes of naive set theory is to
: turn set-defining characteristic functions into partial functions from
: sets to the three-valued logic {T,F,bot}. This three-valued logic
: extends classical logic in the obvious way with
: and(T,bot)=or(F,bot)=bot, and(F,x)=F, or(T,x)=T, not(bot)=bot, so that
: every truth function has a fixed point.
Very much Lukasiewicz' trivalent logic, then. That is good, and it allows
easy extension to polyvalent logics.
: Obviously the law of excluded middle does not hold: or(a,not(a)) only
: implies that a is T or bot. This gives the logic a constructive
: character.
Constructivism has been one of the driving reasons behind the introduction
of alternate logics. Removing the constraint of excluded "middle"
generalises one into the realm of Heyting algebras, where constructive
theories roam, while allowing the avoidance of the antinomies found in the
Boolean.
: In my formulation, I identify each set with its characteristic
: function from sets to {T,F,bot}. Thus given s:set, the membership of
: an element x can be tested with s(x). In the general case, this is a
: partial function, returning bot for some values. I call such sets
: "partial sets", and sets whose characteristic function is in {T,F}
: "total sets". Every set of ZF and NF is a total set, with this theory
: admitting a strictly larger class of sets than either.
In some ways, this is the structure of a topoi, or at least a functor from a
topoi category to something similar. Is the approach meant to be categorial
(which, by the way, is a good thing in my eyes -- I'm just curious)? Then,
your partial classification appears to mainly distinguish the topoi of sets
from some of the many other topoi.
: Russell's set R={s:set|not(s(s))} is then a partial set. All ZF sets
: are elements of R, while some elements of NF are not elements of R,
: while some new sets such as R itself are of undecidable membership.
:
: I've translated the ZF axioms to this set theory, rephrasing them in
: terms of characteristic functions and new for-all and there-exists
: logic operators performing logical conjunction and disjunctions across
: all elements of a characteristic functions. Everything appears to be
: sound and avoids known paradoxes.
The categorial study of paradox is becoming a large field these days, and it
appears you may be repeating some of the work already done (which can be
soooo frustrating sometimes!). I don't mean to assume any level of study,
but perhaps I might suggest that, if you haven't, you should check out some
of the resources available in this field. There are articles available
online I can suggest.
: With the new axioms, it is easy to construct a bijection from the
: universal set to its power set. Cantor's proof that |P(x)|>|x| for
: all non-empty sets x proceeds by constructing C={a:x|not(P(x)(a)} and
: using the law of excluded middle to derive a contradiction on its
: membership in P(x). This goes away for lack of excluded middle,
: leaving C a partial set which appears not to be constructively
: contradictory.
:
: The one worrying aspect of this approach is that it identifies sets
: with characteristic functions from sets to logic values:
: Set=Set->{T,F,bot}. I have only been able to develop an intuition of
: such sets in a purely constructive way, by writing down a finite list
: of possibly self-referential equations defining sets, and convincing
: myself that a unique solution exists. This is much in the style of
: NF's axiom that every (possibly cyclic) graph corresponds to a set,
: but I allow unlimited comprehension.
:
: Are there any known problems with this approach to set theory? Any
: pointers to research on the topic?
No known problems that I am aware of. In fact, it seems to me to be one of
the more successful modern approaches for classifying paradox. However, if
I could make one suggestion, it would be to not restrict yourself to your
trivalent logic. Any Heyting algebra is possible, and expands your research
into the much more fruitful world that all topoi present. In fact, because
of natural distinctions that present themselves between propositions that
take on the "middle" value, trivalent theories are often looked at only as
summarisations of a more natural infinitely valent theory. Good resources
for this can be found in intuitionist discussions, but it is more general.
Also, may I ask why you posted to comp.lang.functional? This intrigues me
because some of my own research has been around the evaluation of the lambda
calculus and proof / evaluation theory in the context of non standard
logics, but I do not see this approach explicitly stated in your message.
Good luck with your researche!
--
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
galathaea: prankster, fablist, magician, liar
galathaea
: One apparent way of avoiding the paradoxes of naive set theory is to
: turn set-defining characteristic functions into partial functions from
: sets to the three-valued logic {T,F,bot}. This three-valued logic
: extends classical logic in the obvious way with
: and(T,bot)=or(F,bot)=bot, and(F,x)=F, or(T,x)=T, not(bot)=bot, so that
: every truth function has a fixed point.
Very much Lukasiewicz' trivalent logic, then. That is good, and it allows
easy extension to polyvalent logics.
: Obviously the law of excluded middle does not hold: or(a,not(a)) only
: implies that a is T or bot. This gives the logic a constructive
: character.
Constructivism has been one of the driving reasons behind the introduction
of alternate logics. Removing the constraint of excluded "middle"
generalises one into the realm of Heyting algebras, where constructive
theories roam, while allowing the avoidance of the antinomies found in the
Boolean.
: In my formulation, I identify each set with its characteristic
: function from sets to {T,F,bot}. Thus given s:set, the membership of
: an element x can be tested with s(x). In the general case, this is a
: partial function, returning bot for some values. I call such sets
: "partial sets", and sets whose characteristic function is in {T,F}
: "total sets". Every set of ZF and NF is a total set, with this theory
: admitting a strictly larger class of sets than either.
In some ways, this is the structure of a topoi, or at least a functor from a
topoi category to something similar. Is the approach meant to be categorial
(which, by the way, is a good thing in my eyes -- I'm just curious)? Then,
your partial classification appears to mainly distinguish the topoi of sets
from some of the many other topoi.
: Russell's set R={s:set|not(s(s))} is then a partial set. All ZF sets
: are elements of R, while some elements of NF are not elements of R,
: while some new sets such as R itself are of undecidable membership.
:
: I've translated the ZF axioms to this set theory, rephrasing them in
: terms of characteristic functions and new for-all and there-exists
: logic operators performing logical conjunction and disjunctions across
: all elements of a characteristic functions. Everything appears to be
: sound and avoids known paradoxes.
The categorial study of paradox is becoming a large field these days, and it
appears you may be repeating some of the work already done (which can be
soooo frustrating sometimes!). I don't mean to assume any level of study,
but perhaps I might suggest that, if you haven't, you should check out some
of the resources available in this field. There are articles available
online I can suggest.
: With the new axioms, it is easy to construct a bijection from the
: universal set to its power set. Cantor's proof that |P(x)|>|x| for
: all non-empty sets x proceeds by constructing C={a:x|not(P(x)(a)} and
: using the law of excluded middle to derive a contradiction on its
: membership in P(x). This goes away for lack of excluded middle,
: leaving C a partial set which appears not to be constructively
: contradictory.
:
: The one worrying aspect of this approach is that it identifies sets
: with characteristic functions from sets to logic values:
: Set=Set->{T,F,bot}. I have only been able to develop an intuition of
: such sets in a purely constructive way, by writing down a finite list
: of possibly self-referential equations defining sets, and convincing
: myself that a unique solution exists. This is much in the style of
: NF's axiom that every (possibly cyclic) graph corresponds to a set,
: but I allow unlimited comprehension.
:
: Are there any known problems with this approach to set theory? Any
: pointers to research on the topic?
No known problems that I am aware of. In fact, it seems to me to be one of