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
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