```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 quantifierAp[pEQp]be interpreted asAp[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))))=================
```