Date: Apr 25, 2013 10:08 PM
Author: fom
Subject: Re: Matheology § 258

On 4/25/2013 6:02 AM, WM wrote:
>
> the domain of anonymous cowards.
>



Definition:
AxAy(xcy <-> (Az(ycz -> xcz) /\ Ez(xcz /\ -ycz)))

Theorem:
AxAy(xcy -> -ycx)

Theorem:
AxAyAz((xcy /\ ycz) -> xcz)

Theorem:
Ax(-xcx)

Definition:
AxAy(xey <-> (Az(ycz -> xez) /\ Ez(xez /\ -ycz)))

Definition:
AxAy(xEQy <-> (Az(xcz <-> ycz) /\ Az(zcx <-> zcy) /\ Az(xez <-> yez) /\
Az(zex <-> zey)))

Definition:
AxAy(x=y <-> Az(xez <-> yez))

Assumption:
AxAy(Az(xcz <-> ycz) -> Az(xez <-> yez))

Assumption:
AxAy(Az(zex -> zey) -> Az(ycz -> xcz))

Assumption:
AxEyAz(zey <-> zcx)

Theorem:
AxAy(xcy -> Az(zex -> zey))

Theorem:
AxAy(Az(ycz -> xcz) -> Az(zex -> zey))

Theorem:
AxAy(xcy <-> (Az(zex -> zey) /\ Ez(zey /\ -zex)))

Theorem:
AxAy(Az(zex -> zey) -> Az(zcx -> zcy))

Theorem:
AxAy(Az(xez -> yez) -> Az(xcz -> ycz))

Theorem:
AxAy(xEQy <-> Az(xcz <-> ycz)

Theorem:
AxAy(xEQy <-> Az(zex <-> zey))

That grammatical equivalence is expressible in terms of neighborhood
filters is provable:
AxAy(xEQy <-> Az(xez <-> yez))

Theorem:
AxAy(xEQy <-> x=y)

Assumption:
AxAy((Az(ycz -> xez) /\ Ez(xez /\ -ycz)) -> Az((xez /\ -ycz) -> (Ew(xew
/\ wcy) \/ Aw(zcw -> ycw))))

Assumption:
AxAy((Ez(xcz) /\ Ez(ycz)) -> EwAz(zew -> (z=x \/ z=y)))

Definition:
Ax(x=V() <-> Ay(-(ycx <-> y=x)))

Assumption:
ExAy(-(ycx <-> y=x))

Assumption:
Ax(Ey(xcy) -> Ey(xey))

Definition:
Ax(set(x) <-> Ey(xcy))

Definition:
Ax(x=null() <-> Ay(-(xcy <-> x=y)))

Assumption:
ExAy(-(xcy <-> x=y))

Assumption:
Ax(Ey(ycx) -> Ey(yex /\ -Ez(zex /\ zey)))

Assumption:
AxEy(Az(zey <-> Ew(wex /\ zew)) /\ (Ez(xcz) -> Ez(ycz)))

Assumption:
AxEy(Az(zey <-> Aw(wex -> zew)) /\ (Ez(zcx) -> Ez(ycz)))

Definition:
AxAy(x=P(y) <-> (Ez(ycz) /\ Az(zex <-> (zcy \/ z=y))))

Assumption:
Ax(Ey(xcy) -> Ey(Az(zey <-> (zcx \/ z=x)) /\ Ez(ycz)))

Definition:
AxAy(x=S(y) <-> (Ez(ycz) /\ Az(zex <-> (zey \/ z=y))))

Assumption:
Ax(Ey(xcy) -> Ey(Az(zey <-> (zex \/ z=x)) /\ Ez(ycz)))

Assumption:
Ex(Ey(xcy) /\ null()cx /\ Ay(ycx -> Ez(zcx /\ ycz)))


Let the restricted quantifier

Ap[pEQp]

be interpreted as

Ap[pEQp](phi(p)) <-> Ap(pEQp /\ phi(p))

Then for each n and each well-formed formula phi(y, p_0, ..., p_n),

assume


=================
Ap_n[p_nEQp_n]...Ap_0[p_0EQp_0]
AxAy(
Ew(ycw) ->
(Ez((Ew(zcw) /\ (yez <-> (yex /\ phi(y, p_0, ..., p_n))))) <-> Ew(xcw))
)
=================


and assume

=================
Ap_n[p_nEQp_n]...Ap_0[p_0EQp_0]
(
AxAyAz(
(
((Ew(xcw) /\ Ew(ycw)) /\ (phi(x,y, p_0, ..., p_n)) /\
((Ew(xcw) /\ Ew(zcw)) /\ (phi(x,z, p_0, ..., p_n))
) -> (y=z)
)
->
AxAy(
Ew(ycw) ->
(Ez((Ew(zcw) /\ (yez <-> Ew(wex /\ phi(z,w, p_0, ..., p_n))))) <-> Ew(xcw))
)
)
=================