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
Tim Sweeney
> : 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.
My goal is to show evidence that a particular type theory is
reasonable, by equating it to some existing system. An axiomatic set
theory was my first hope due to the relative simplicity, but a topos
will do.
> 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.
Do you have any pointers to research on topoi coinciding to a set
theory with a universal set, or more generally to any topos-centric
analysis of paradoxes due to nonwellfoundedness?
> 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.
In my setting, I am mainly interested in mechanically analyzing sets
to determine whether they are inhabited and, if so, whether they are
singletons. A trivalent logic seems sufficient for this: any finer
structure can be projected down for my purposes.
> 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.
I'm developing a programming language with enough expressive power
that one may easily express the major paradoxes from set theory, both
those due to recursion (the liar paradox) and those due to
nonwellfoundedness or reflection (Russell's paradox). I have a
compiler that analyzes programs and assigns to each term a set
cardinality approximations classifying its potential inhabitance, as
well as an indicator of the decidability of this classification.
The general idea is that single-valued terms correspond to
runtime-executable parts of programs, while more general (potentially
uninhabited or multivalued terms) may be bundled up into extensional
types and reasoned about within the limits of the compiler's
resolution rules. This all works to the extent of being able to
express the paradoxes, recognize their undecidability, and
mechanically determine that, for example, certain concrete terms do or
don't belong to Russell's set. But though it tends to work well in
mechanical terms, it lacks a theoretical basis.
Thank you very much for the pointers!
Tim Sweeney