Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
Re: Relational Mereology interpreting type theory: Correction!
Posted:
Aug 1, 2012 4:35 AM
|
|
On Tue, 31 Jul 2012, Zuhair wrote:
> Mereo-relational Theory: A theory in first order logic with identity
> "=", part-hood "p" and Ordered pair "()".
>
> Axioms: Identity theory axioms +
>
> (1) x p x
>
> (2) x p y & y p z -> x p z
>
> (3) x p y & y p x -> x=y
p is an order usually notated <=.
> Define (pp): x pp y <-> x p y & ~y p x
>
Why make it complicated?
x < y when x <= y and x /= y.
> Define (O): x O y <-> Exist z. z p x & z p y
>
x O y when { x,y } is bounded below.
> (4) x pp y -> Exist z. z p y & ~ z O x
>
x < y -> some z < y with { z,x } not bounded below.
> (5) (~ x p y) -> Exist z. z p x & ~ z O y
>
not x <= y implies some z < x with { z,y } not bounded below
> Define(atom): x is atom <-> ~Exist y. y pp x
>
for all y, not y < x
> (6) Exist z. phi ->
> (Exist x. for all y. y O x <-> Exist m. phi(m) & y O m)
Do you mean "Exist z, phi(z) ->"?
Do you also mean
"(Exist x. for all y. (y O x <-> Exist m. phi(m) & y O m))"?
> Define (whole of (phi)s): x is a whole of (phi)s iff whatever overlaps
> with x do overlap with an object satisfying phi
Makes no sense at all for all the undefined terms and in addition
seems irrevelant to the discussion.
> (7) Exist x. for all y. y p x -> Exist z. z pp y
Do you maan "Exist x. for all y. (y p x -> Exist z. z pp y)"?
some x with for all y, (y <= x -> some z < y
> Define(void): x is void <-> for y. y p x -> Exist z. z pp y
>
Do you mean "x is void <-> for all y, (y p x -> exist z, z pp y)"?
x void when for all y <= x, some z < y.
How is that void? From x <= x, some x1 < x and subsequently
... < xj < x_(j-1) <..< x1 < x
I stop here for that's enough of your not helpful pp notation.
> (8) Ordered pairs are identical iff they have the same projections
>
> (a,b)=(c,d) <-> a=c & b=d
>
> (9) Every ordered pair of wholes of atoms is void
>
> (10) for i=1,2,3,...
> Every ordered pair of wholes of i_th degree ordered pairs is a void
> disjoint of its projections
>
> Define:
> x is 1_st degree ordered pair <-> x is an ordered pair of wholes of
> atoms
> x is i+1_th degree ordered pair <-> x is an ordered pair of wholes of
> i_degree ordered pairs
>
> (11) for n=1,2,3,...
> For all x. (Exist z1,..,zn for all y. y p x & y is atom -> y=z1
> or ..or y=zn) -> Exist z. z is atom & ~ z p x.
>
> / Theory definition finished.
>
> I think this clearly interpret type theory + infinity + proper
> classes.
>
> Zuhair
>
|
|
|
|
