A type theory with a universal set in it.
- From: Zaljohar@xxxxxxxxx
- Date: Fri, 7 Dec 2007 14:20:13 -0800 (PST)
Hi
Let X be a theory in FOL with identity with the additional following
primitives: N,S,k,<,e,F.
N is a primitive one place predicate symbole that stands for 'natural
number'.
So N(x) stands for ' x is a natural number '.
S is primitive one place function symbole that stands for
'successor'.
So S(x) stands for the 'successor of x'.
k is a primitive constant.
< is a primitive two place relation symbole that stands for 'lesser
than'.
e is epsilon membership.
F is the stratification function, and it is a one place function
symbole.
Axioms:
1) Axiom:E!x( N(x) & ~Ey( x=S(y)) ).
Define x=0 <-> (N(x) & ~Ey( x=S(y))).
2) Axiom: Ax ( N(x) -> N(S(x)) ).
3) Axiom:Ax ( N(x) <-> ~x=S(x) ).
4) Axiom:Axyz( ( N(x) & N(y) & z=S(x) & z=S(y) ) -> x=y )
5) Axiom schema of Induction:For every formula Q, any closure of
(Q(0) &Ax((N(x) & Q(x)) -> Q(S(x)))) -> Ax ( N(x) ->Q(x) )
is an axiom.
6) Axiom:Ax( x < S(x) ).
7) Axiom:Axyz( (x<y & y<z) -> x<z )
8) Axiom:~ N(k)
9) Axiom:Ax ( N(x) -> x < k )
10) Axiom:Ax ( (N(x) v x=k) <-> F(x)=0 ).
11) Axiom of Extensionality:
Axy ( (~F(x)=0 & ~F(y)=0) -> (Az( zex<->zey) -> x=y) ).
12) Axiom:Ax Ay ( y e x -> F(y) < F(x) ).
13) Axiom:Ex Ay ( y e x <-> F(x)=0 ) .
This set is unique (Extensionality) and it is the set of Types ' T
' .
Definition: x=T <-> Ay( yex <-> F(y)=0 )
14) Axiom:Ax Ay( F(x)=y -> T(y) ).
15) Axiom:Ex Ay ( ~yex )
Definition x={} <-> Ay( ~yex)
16) Axiom: F({}) = S(0)
17) Axiom schema of Comprehension: for every formula Q in which x is
not free, then
all closures of
Aij((i e T & j e T & j < i & Ex(Q(x) & ~Eh( F(x)<h &~h=F(x) &h<i))
->
Ex( F(x)=i & Ay( yex<-> ( F(y)=j & Q ) ) ) )
are axioms.
/ Theory definition finished.
Zuhair
Sincerely speaking I don't know even if this theory is consistent or
not, but definitly it is too counter-intuitive.
This theory avoids the three major known paradoxes: Russell's, Burali-
Forti and Cantor's, in a rather strange manner.
This theory also proves the existence of a set of all sets.
Also Frege's definition of cardinality as an equivalence class of all
sets under equivalence relation 'bijection', works here, and this
equivalence class is a set.
The set of all ordinals doesn't exist in this theory, so is the set of
all sets that are not members of themself, it also doesn't exist in
this theory, so is the set of all non empty ordinals, this also
doesn't exist.
Cantor's paradox is prevented simply because the power set of the set
of all sets doesn't exist.
However, I do think that there is a great possibility that this theory
is inconsistent.
Even if this theory is shown not to have obviouse inconsistency, still
it would be TOO COUNTER-INTUITIVE and Complex.
But it might assist in understanding the complex nature of universal
set.
In this theory a universal set is defined as a set of type k.
x is a universal set <-> F(x)=k.
All such sets are in themselfs, and even the set of all these sets is
in itself.
Very complex theory!
Zuhair
.
- Follow-Ups:
- Re: A type theory with a universal set in it.
- From: LauLuna
- Re: A type theory with a universal set in it.
- From: Zaljohar
- Re: A type theory with a universal set in it.
- From: MoeBlee
- Re: A type theory with a universal set in it.
- From: Zaljohar
- Re: A type theory with a universal set in it.
- Prev by Date: Re: Torkel Franzen on truth
- Next by Date: Re: Torkel Franzen on truth
- Previous by thread: 'Two' incommensurables?
- Next by thread: Re: A type theory with a universal set in it.
- Index(es):
Relevant Pages
|
