Re: Triclass Theory

On Mar 19, 1:34 pm, "MoeBlee" <jazzm...@xxxxxxxxxxx> wrote:
On Mar 13, 8:21 pm, "zuhair" <zaljo...@xxxxxxxxx> wrote:

The following is a set theory

I studied your theory, getting as far as your argument for a purported
theorem schema of replacement. So I got through all the axioms. Just
about everything before the purported theorem schema of replacement
looks pretty good, though I have several suggestions. So, at least as
to everything before the purported theorem schema of replacement, I
think you did a pretty good job. I have no idea whether the theory is
consistent, but at least it is well formed.

At the argument for a purported theorem schema of replacement, it
seems to me that you make the mistake of universally generalizing on a
variable that was existentially instantiated. That is a common and
deadly mistake for someone who has not learned the predicate calculus.
However, perhaps I misunderstand your argument and that it really does
work; In that case, we'd have to go through, if you want me to
recognize its validity. Then, in a few key places after the purported
theorem schema of replacement, I just could not see your arguments as
being more than handwaving. If those purported theorems really do have
proofs, then for me to recognize the validity of those arguments, we'd
have to go over them. Maybe your arguments do work for someone with a
lot more insight than me; but at least for me, I couldn't see the
validity.

Below I show you how I would formalize what you've done. You don't
have to accept my formulation, but perhaps you will find it useful in
certain respects.

One thing I did not like were your definitions of 'subclass',
'subset', and 'proper subclass'. You added a clause to each of those;
which has the effect of making it difficult to compare with the usual
set theoretic definitions of those. It's your axioms, not your
definitions, that will give you a new theory. Definitions are just
abbreviations essentially. So it's better to keep your definitions
standard as much as possible so that we can compare your theory with
other theories more easily. Then, if you have a special concept you
want to define for your own theory, you can choose a new word for it.
But using a word already well used (such as 'subclass') for something
that has an added technical qualification in your theory just tends to
obscure comparisons between your theory and other theories.

Most of your ordering of the axioms, theorems, and definitions was
pretty good, but I changed a few things around. Also, even though the
ordering I provide is formally correct (in the sense that there is no
theorem or definition that depends on an axiom, theorem, or definition
that comes later), there could be improvement on the flow. But that is
not crucial at this time.

On minor detail: I don't like using the letter 'a' as a variable if
there is not another font to use to distinguish between metalanguage
and object language, since in a proof or discussion the variable 'a'
gets blurred next to the word, the indefinite article, 'a'. So I used
different letters other than 'a' and made some other changes in
variable letters as I thought suited a clearer notation. Also, since
you use 'P' for power, I used 'F' for formulas rather than 'P'.

Here's what I came up with (whatever typos and mistakes to be
corrected):

INTRODUCTION

Triclass theory is the set of sentences entailed (by classical first
order logic with identity) from the following non-logical axioms,
which are formulated in the exposition:

Extensionality
Universe
Regularity
Comprehension (schema)
Pairing
Empty Set
Union
Infinity
Power
Size Limitation

The following ontology is entailed by the axioms and definitions:

(1) We say that a class is any object that has a member or is 0 (as
'0' is defined in the exposition).
(2) All objects are classes.
(3) We say an urelement is an object that is not a class.
(4) There are no urelements.
(5) There is a unique class T of which all classes (even itself) are
members.
(6) We say a proper class is a class that is not T and is a member
only of T.
(7) There are proper classes.
(8) We say a set is a class that is a member of some class other than
T.
(9) There are sets.
(10) There is a unique class V whose members are all and only the
sets. And V is a proper class.
(11) There is a unique class 0 that has no members. And 0 is a set.
(12) For every class x, exactly one of three alternatives holds: x is
T, or x is a proper class, or x is a set.

So the main feature of triclass theory is that in addition to sets and
proper classes, there is a unique universal class T of which every
object (even itself) is a member. This may satisfy some people who
find any theory to be unintuitive if it is a theorem of the theory
that there does not exist a universe of all objects. However, there is
no partition of the universe T, so some people who pine for not just a
universe of all objects but one that can be partitioned will not be
satisfied. Perhpaps the lesson being that you can't have your pie and
partition it too.

We have not investigated whether the axioms are independent.

We are interested in comparisons between triclass theory and Morse
class theory.

There is no known proof of inconsistency of triclass theory. We
welcome all attempts at proof of inconsistency so that, if
inconsistency is found, we will know to revise the theory or abandon
it.

EXPOSITION

If a theorem or definition is stated as an open formula, then the open
formula is to be regarded as standing for any closure of the formula.

If 't' is a term that does not properly refer due to the antecedent of
a conditional definition failing, then we set t=0 (''0' is defined in
the exposition).

Theorem
~ExAy(yex <-> ~yey)
______

Axiom: Extensionality
AxAy(x=y <-> Az(zex <-> zey))
______

Axiom: Universe
E!xAy(yex & Az(xez -> x=z))
______

Definition
x =T <-> Ay(yex & Az(xez -> x=z))
______

Definition
x is a proper class <-> (~x=T & Az(xez -> z=T))
______

Definition
x is a set <-> Ez(~z=T & xez)
______

Theorem
Exactly one of three alternatives holds: x is a set, or x is a proper
class, or x=T.
______

Axiom: Regularity
Ax((~x=T & Ez zex) -> Eyex Acey ~cex)
______

Axiom Schema: Comprehension

If F is a formula in which the variable x is not free, then all
closures of
ExAy(yex <-> (y is a set & F))
are axioms.
______

Theorem Schema

If F is a formula in which the variable x is not free, then all
closures of
E!xAy(yex <-> (y is a set & F))
are theorems.

Proof
Follows from comprehesion and extensionality
______

Theorem
E!xAy(yex <-> y is a set)

Proof:>From comphrension we have ExAy(yex <-> (y is a set & y=y)).

So ExAy(yex <-> y is a set). And by extensionality, E!x(yex <-> y is a
set).
______

Definition
x=V <-> Ay(yex <-> y is a set)
______

Theorem
x is a set <-> xeV
______

Axiom: Pairing
AreV AseV ExeV Ay(yex <-> (yeV & (y=r v y=s)))
______

Definition
(reV & seV) -> ({r s}=x <-> Ay(yex <-> (yeV & (y=r v y=s))))
______

Definition
{r}={r r}
______

Theorem
~VeV

Proof:
Toward a contradiction, suppose VeV.
So, by pairing, {V}eV. So Ez(~z=T and {V}ez).
So, by the definition of T, we have ~{V}=T.
And Ve{V}.
So, by regularity, Eye{V} Acey ~ce{V}).
So ~Ve{V}, which is a contradiction.
______

Theorem
~V=T
______

Theorem
xeV -> ~x=T
______

Theorem
~b=T -> ~Veb

Proof
Toward a contradiction, suppose ~b=T and Veb.
Then VeV, which contradicts the theorem that ~VeV.
______

Theorem
Ex x is a proper class

Proof
V is a proper class.
______

Theorem
xeV -> ~xex

Proof
Toward a contradiction, suppose xeV and xex.
Then ~{x}=T and Ez ze{x}, but~Eye{x} Acey ~ce{x}, which contradicts
regularity.
______

Theorem
~x=T -> ~xex

Proof
Toward a contradiction, suppose ~x=T and xex. Then xeV, so ~xex, which
is a contradiction.
______

Theorem Schema

If F is a formula, then all closures of
Ab(~b=T -> ExAy(yex <-> (yeb & F))) ->
ExAy(yex <-> (yeV & F))
are theorems
______

Theorem Schema

If F is a formula, then all closures of
Ab(~b=T -> E!xAy(yex <-> (yeb & F))) ->
E!xAy(yex <-> (yeV & F))
are theorems
______

Axiom: Empty Set
ExeVAy ~yex
______

Definition
x=0 <-> Ay ~yex
______

Definition
x is a class <-> (Ey yex v x=0)
______

Theorem
x is a class
______

Definition
x is an urelement <-> ~x is a class)
______

Theorem
~ x is an urelement
______

Definition Schema

If F is a formula, then
E!xAy(yex <-> F) -> ({y | F}=x <-> Ay(yex <-> F)) &
~E!xAy(yex <-> F) -> ({y | F}=0)
______

Axiom: Union
AbExAy((yex <-> Ez(zeb & yez)) & (xeV <-> beV))
______

Theorem
E!xAy(yex <-> Ez(zeb & yez))
______

Definition
x=Ub <-> Ay(yex <-> Ez(zeb & yez))
______

Theorem
beV <-> Ub e V
______

Theorem
~ UV e V
______

Theorem
~ V e UV

Proof
Suppose toward a contradiction that VeYeV for some Y.
So ~Y=T. So VeV, which is a contradiction.
______

Theorem
~ UV = T

Proof
VeT but ~ V e UV.
______

Theorem
~ f = T -> ~Uf = T

Proof
Suppose ~f=T.
To show ~ UV e Uf, toward a contradiction suppose:
For some Y we have UV e Y e f.
So ~Y=T. So UV e V, which is a contradiction.
So ~ UV e Uf. But UV e T. So ~Uf=T.
______

Theorem
UT = T

Proof
If xeUT, then xeT, since Ax xeT.
If xeT, then xeTeT, so xeUT.
______

Theorem
Ars((~r=T & ~s=T) -> E!xAy(yex <-> (yer v yes))

Proof
Follows from comphrension, extensionality, and definition of T.
______

Definition
(~r=T & ~s=T) -> (x = rus <-> Ay(yex<->(yer v yes)))
______

Theorem
(reV & seV) -> rus e V

Proof
{r s}eV. So from union, we have U{r s} e V.
And Ay(yeU{r s} <-> (yer v yes)).
______

Axiom: Infinity
ENeV(0eN & Ax(xeN -> xu{x}eN))
______

Axiom: Power
Ab(~b=T -> ExAy(yex <-> (yeV & Az(zey -> zeb)) & (beV <-> xeV)))
______

Theorem
~b=T -> E!xAy(yex <-> (yeV & Az(zey -> zeb)))
______

Definition
~b=T -> (x=Pb <-> Ay(yex <-> (yeV & Az(zey -> zeb)))
______

Theorem
~b=T -> (beV <-> Pb e V)
______

Theorem
~b=T -> ~Pb=T

Proof
Toward a contradiction suppose Az(zeT -> z e Pb).
Then T e Pb. So TeV, which is a contradiction.
______

Definition
<r s>={{r} {r s}}
______

Theorem
(reV & seV & xeV & yeV) -> (<r s> = <x y> <-> (r=x & s=y))

Proof
Suppose {{r} {r s}}={{x} {x y}}.
Then there are four cases:
(1) {r}={x} and {r s}={x}.
(2) {r}={x} and {r s}={x y}.
(3) {r}={x y} and {r s}={x}.
(4) {r}={x y} and {r s}={x y}.
In case (1), r=x=s. So {x y}={s}, so y=s.
In case (2), r=x. And s=x or s=y. And if s=x, then s=r, so, since y=r
or y=s, we have y=s.
In case (3), r=x=s. And y=r, so y=s.
In case (4), r=x=y. And v=x or s=y. And if s=x, then s=y.
______

Definition
f is a relation <-> Apef Ers p=<r s>
______

Definition
f is many-one <-> Axyz(<x y>ef & <x z>ef) -> y=z)
______

Definition
f is a function <-> (f is a relation & f is many-one)
______

Definition
f is single rooted <-> Axyz(<x y>ef & <z y>ef) -> x=z)
______

Definition
f is 1-1 <-> (f is a function & f is single-rooted)
______

Definition
y subclass_of b <-> Az(zey -> zeb)
______

Theorem
y=b <-> (y subclass_of b & b subclass_of y)

Proof
Follows from extensionality.
______

Theorem
T subclass_of x <-> x=T
______

Definition
y proper subclass_of b <-> y subclass_of b & ~b=y)
______

Definition
y subset_of b <-> (y subclass_of b & yeV)
______

Theorem
~b=T -> (y subset_of b <-> yePb)
______

Definition
y proper subset_of b <-> (y subset_of b & ~b=y)
______

Theorem
yeV -> y proper subset_of V
______

Theorem
x is a proper class -> x subclass_of V
______

Theorem
x is a proper subclass_of T -> x subclass_of V
______

Theorem Schema

If F is a formula in which the variable x does is not free, then all
closures of
~b=T -> E!xAy(yex <-> (yeb & F))
are theorems.

Proof>From comprehension we have ExAy(yex <-> (yeV & yeb & F)).

But since ~b=T, we have that yeb entails yeV.
Uniqueness follows from extensionality.
______

Theorem
(~r=T & ~s=T) -> E!zAy(yez <-> Euw(y=<u w> & uer & wes))

Proof>From comprehension we have:

E!zAy(yez <-> (yeV & Euw(y=<u w> & uer & wes))).
~r=T and ~s=T and uer and wes, so by iteration of pairing, <u w>eV.
______

Definition
(~r=T & ~s=T) -> (z = rXs <-> Ay(yez <-> Euw(y=<u w> & uer & wes)))
______

Theorem Schema

If F is a formula in which the variable x is not free, then all
closures of
E!xAy(yex <-> (y e rXs & F))
are theorems.
______

Theorem
~f=T -> E!xAy(yex <-> Ez <y z>ef)

Proof
~f=T -> E!xAy(yex <-> (yeUUf & Ez <y z>ef)).
And if Ez <y z>ef, then yeUUf.
______

Definition
~f=T -> (dom(f) = x <-> Ez <y z>ef)
______

Theorem
~f=T -> E!xAy(yex <-> Ez <z y>ef)

Proof
~f=T -> E!xAy(yex <-> (yeUUf & Ez <z y>ef)).
And if Ez <z y>ef, then yeUUf.
______

Definition
~f=T -> (range(f) = x <-> Ez <z y>ef)
______

Definition
f:D->C <-> (f is a function & dom(f)=D & range(f) subclass_of C)
______

Definition
f:D->inj C <-> (f is 1-1 & dom(f)=D & range(f) subclass_of C)
______

Definition
f:D->sur C <-> (f is a function & dom(f)=D & range(f)=C)
______

Definition
f:D->bij C <-> (f is 1-1 & dom(f)=D & range(f)=C)
______

Theorem
0:0->bij 0
______

Definition
x supernumerous to b <-> (Ef f:b->inj x & ~Ef f:x->inj b)
______

Definition
b subnumerous to x <-> x supernumerous to b
______

Axiom: Size Limitation
xeV <-> x subnumerous to V
______

****That completes the axioms. Additional theorems and definitions
follow:

Definition
x equinumerous to b <-> Ef f:x->bij b
______

Theorem
~b=T -> E!xAy(yex <-> Ezeb y=<z z>)

Proof
E!xAy(yex <-> (y e bXb & Ezeb y=<z z>)).
And if Ezeb y=<z z> then y e bXb.
______

Definition
~b=T -> Ib=x <-> Ay(yex <-> Ezeb y=<z z>)
______

Theorem
Ib:b->bij b
______

Theorem
b subclass_of c -> ~b supernumerous to c

Proof
Suppose b=T. Then c=T. So b=c. And Ef f:b->inj b & ~Ef f:b->inj b is a
contradiction.
Suppose ~b=T. Then Ib:b->inj c.
______

Theorem
~f=T -> E!xAy(yex <-> Ers(y=<r s> & <s r>ef))

Proof
E!xAy(yex <-> (y e PPUUf & Ers(y=<r s> & <s r>ef))).
But if Ers(y=<r s> & <s r>ef)) then y e PPUUf.
______

Definition
~f=T -> (inv(f)=x <-> Ay(yex <-> Ers(y=<r s> & <s r>ef)))
______

MoeBlee

This rather splendid work can be completed with the following
theorums:

--------
Theorem of exclusive numerousity.
ArAs ( (~r=T & ~s=T) -> (r is equinumerous to s xor r is subnumerous
to s xor r is supernumerous to s) ).

Note the use of 'exlusive or' denoted as 'xor' , it means that between
any r and s
only ONE of the three numerousity types should exist.

-----------

Constellation of theorums:

Theorem: Ax( ~x=T -> x is equinumerous to x)

Theorem: AxAy( (~x=T & ~y=T) -> (x is equinumerous to y <-> y is
equinumerous to x ) ).

Theorem: AxAyAz( (~x=T & ~y=T &~z=T) -> ((x is equinumerous to y & y
is equinumerous to z) ->x is equinumerous to z) ).

Theorem: AxAyAz( (~x=T & ~y=T &~z=T) -> ((x is subnumerous to y & y is
subnumerous to z) ->x is subnumerous to z) ).

Theorem: AxAyAz( (~x=T & ~y=T &~z=T) -> ((x is subnumerous to y & y
is equinumerous to z) ->x is subnumerous to z) ).

------------

Theorem: Ax( x is a proper class <-> x is equinumerous to V ).

Proof: we already have Ax(x is a proper class -> x is subclass_of V)
as a theorem.
Then it follows that ~ (x is supernumerous to V) ( non
supernumerousity of a subclass over its class).
From limitation of size we have ~( x is subnumerous to V)
Thus x is equinumerous to V (theorm of exclusive numerousity).
Theorem proved.

--------------------

Theorem schema of small separation: if F is a formula in which x
doesn't occure free then all closures of

AseVExeVAy(yex<-> (yes & F) )

are theorums.

Proof:

From theorum of large separation we have x as a class.
Since seV then s is subnumerous to V
we have x is subclass_of s
then ~( x is supernumerous to s)
then either x is equinumerous to s, in which case it follows
that x is subnumerous to V
or x is subnumerous to s, in which case it follows that
x is subnumerous to V.
then in both cases x is subnumerous to V
since there is no other case of numerousity ( thoerem of exclusive
numerousity), then x is subnumerous to V thus xeV ( limitation of
size).
Theorem Proved.

-------------------------------

Theorem schema of Large separation ( note the place of this theorem
should be
among one of the theorems that follows global comprehension ).

If F is a formula in two variables, in which c is not free, then all
closures of:

[AxeV Ay(F -> yeV)] -> Ab(~b=T -> EcAy(yec <-> Exeb F)).

are theorums.

Proof: presented upthread.

-------------------------------
Theorem schema of small replacement:

If F is a formula in two variables, in which c is not free, then all
closures of:

[AxeV Ey(yeV & F) E!yF ] -> Ab(beV -> EceVAy(yec <-> Exeb F)).

are theorums.


Proofs: see upthread.

--------------------------------

Theorem of proper union:

AxAy(( x is a proper class & ~y=T) -> xuy is a proper class ).

Proof, from large union we have xuy.
since AxAy( (~x=T & ~y=T) -> x is a subclass_of xuy ).
then ~( x is supernumerous to xuy)
since x is equinumerous to V,
then V is not supernumerous to xuy
since xuy subclass_of V
then xuy is not supernumerous to V.
which is equivalent to saying that V is not subnumerous to xuy
Thus V is equinumerous to xuy
thus xuy is a proper class.
Theorem proved.
----------------------------------------

Definition of ordinals.

x is an ordinal <-> AyAz(zey&yex ->(zex&Au(uez->uey))).

To simplify this definition lets define transitive class.

x is transitive <-> AmAn((nem&mex) -> nex).

Now:

x is an ordinal <-> (x is transitive & Ay(yex->y is transitive)).

So an ordinal is a transitive class of transitive classes.

------------------------

Theorem: AxAy( (x is an ordinal & yex) -> y is an ordinal ).

Proof: From the definition of ordinals if x is an ordinal then Ay(yex-
y is transitive).
And Au(uey->uex-> u is transitive).
Thus every member y of an ordinal x is transitive and every member of
y is transtive
Then y is an ordinal.
Theorem proved.

--------------------

Theorem: AxAy( (x is a set & x is an ordinal & yex) -> (y is an
ordinal & y is a set) ).

Since every member of an ordinal is an ordinal, and every member of a
set is a set
then every member of an ordinal that is a set, IS an ordinal that is a
set.

Theorem proved.

------------------

Theorem: ExAy(yex<-> (y is an ordinal & y is a set)).

Proof: global comprehension

------------------

Theorem: E!xAy(yex<-> (y is an ordinal & y is a set)).

Proof: Extensionality

--------------------

Definition:

x=D <-> Ay(yex<-> (y is an ordinal & y is a set)).

-----------------------

Theorem: D is an ordinal.

Proof: Am(meD -> (m is an ordinal & m is a set)).
AmAn( (m is an ordinal & m is a set) -> (n is an ordinal and n is a
set))
An( n is an ordinal and n is a set -> neD) definition of D.
Thus AnemeD -> neD, Thus D is transitive.
Since AmeD -> m is an ordinal -> m is transitive.
Thus D is a transitive and AmeD-> m is transitive, Thus D is an
ordinal
Theorem proved.

-------------------------

Theorem: D is a proper class.

Suppose that D is a set, then D is an ordinal and D is a set -> DeD
since ~D=T ( extensionality) and ~D=0, then D violates regularity
Thus ~D is a set.
Since ~D=T
Then D is a proper class.

----------------------

Theorem of global choice: Ex( x is an ordinal & x is equinumerous to
V ).

Proof: D is a proper class <-> D is equinumerous to V.
D is an ordinal
Theorem proved.

******************************

Major Result of this theory:

1) ZFC in Triclass & ~ Triclass in ZFC.

Proof: Infinity, Pairing, Empty , are axioms in this theory.
Extensionlity, Regularity, Union, Power, Separation , Replacement
and Choice, in ZFC, are all theorems in this theory.

Thus ZFC in Triclass

Universe and global comprehension do not exist in ZFC
Thus ~ Triclass in ZFC.

2) Triclass is equi-interpretable with Morse-Kelley.

Not tested.


*********************************

What I like most in this theory, is that it provide us with the
apportunity
to look at ZFC from without, like looking to a city from an airplane.
ZFC appears so small, it would be the part of triclass theory that
is concerned with Small classes ( small class <-> set ).
Triclass has another section of it that deals with Large classes
(large class <-> proper class).
T affords us with the intuitive aspect of existence of a universe,
though
it is detached from the other classes, which hamper any further
processing
of T, but yet even this detachemant is in a way intuitive, you don't
expect
what contains every class to be an ordinary class!

Zuhair

.

Relevant Pages

  • Re: Triclass Theory
    ... about everything before the purported theorem schema of replacement ... We say a proper class is a class that is not T and is a member ... Axiom: Extensionality ... Toward a contradiction, suppose VeV. ...
    (sci.logic)
  • Re: Triclass Theory
    ... about everything before the purported theorem schema of replacement ... We say a proper class is a class that is not T and is a member ... Axiom: Extensionality ... Toward a contradiction, suppose VeV. ...
    (sci.logic)
  • Re: What is the Size of V in this theory?
    ... ordinals, that is of course an uncountable ordinal. ... In the above theory we have the following theorem schema: ... Now if we add the following ad hoc axiom to the list of axiom schemes ... So the class of all countable ordinals is a SET. ...
    (sci.logic)
  • Re: What is the Size of V in this theory?
    ... Do the set of all countable ordinals exist in ZF? ... Does ZF prove the existence of the SET of all countable ordinals? ... In the above theory we have the following theorem schema: ... Now if we add the following ad hoc axiom to the list of axiom schemes ...
    (sci.logic)
  • Re: What is the Size of V in this theory?
    ... ordinals, that is of course an uncountable ordinal. ... In the above theory we have the following theorem schema: ... Now if we add the following ad hoc axiom to the list of axiom schemes ... Now this class is either proper class, ...
    (sci.logic)