Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Matheology § 258
Replies: 29   Last Post: Apr 27, 2013 7:43 PM

 Messages: [ Previous | Next ]
 fom Posts: 1,968 Registered: 12/4/12
Re: Matheology § 258
Posted: Apr 25, 2013 10:08 PM

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))
)
)
=================

Date Subject Author
4/23/13 mueckenh@rz.fh-augsburg.de
4/23/13 Virgil
4/24/13 Scott Berg
4/24/13 Virgil
4/25/13 mueckenh@rz.fh-augsburg.de
4/25/13 fom
4/25/13 mueckenh@rz.fh-augsburg.de
4/25/13 YBM
4/25/13 mueckenh@rz.fh-augsburg.de
4/25/13 Virgil
4/25/13 Virgil
4/25/13 fom
4/25/13 fom
4/26/13 Virgil
4/25/13 Virgil
4/25/13 Virgil
4/25/13 Virgil
4/25/13 fom
4/26/13 Virgil
4/26/13 Scott Berg
4/27/13 mueckenh@rz.fh-augsburg.de
4/27/13 Virgil
4/27/13 mueckenh@rz.fh-augsburg.de
4/27/13 Scott Berg
4/27/13 Virgil
4/27/13 mueckenh@rz.fh-augsburg.de
4/27/13 Virgil
4/27/13 ross.finlayson@gmail.com
4/27/13 Virgil
4/24/13 FredJeffries@gmail.com