polemotheos
User
Platinum Boarder
| Posts: 530 |  |
|
God's geometry - 2006/03/05 10:58
http://www.wischik.com/lu/philosophy/spinoza-deduction.html
The predicates used are
Ax x is an attribute
Bx x is free
Dx x is (an instance of) desire
Ex x is eternal
Fx x is finite
Gx x is a god
Jx x is (an instance of) love
Kx x is an idea
Mx x is a mode
Nx x is necessary
Sx x is a substance
Tx x is true
Ux x is an intellect
Wx x is a will
Axy x is an attribute of y
Cxy x is conceived through y
Ixy x is in y
Kxy x is a cause of y
Lxy x limits y
Mxy x is a mode of y
Oxy x is an object of y
Pxy x is the power of y
Rxy x has more reality than y
Vxy x has more attributes than y
Cxyz x is common to y and z
Dxyz x is divisible into y and z
*A for-all
*E there-exists
Following are just a normal way for logic to work.
US: If *Ax.X appears on an earlier line, *Eg.(g=b)=>X[g/b] may
be entered on a new line, with same premise-numbers as on earlier
UG: If *Eg.g=b=>X[a/b] appears on a line, then *Aa.X may be
entered on a line, if b occurs neither in X nor in any premise
on the earlier line. The premise-numbers of the new line are
those of the earlier line.
Ia: *Aa.a=a may be entered on a line, with premises 0
PA: If X[a/b] appears on an earlier line, *Eg.g=b may be entered
on a new line, if X is atomic and undefined. Premise numbers are
same.
EX: If *Aa.X appears on an earlier line, *Ea.X may be entered on new
line, sharing premise numbers.
Two modal operators L and N, with meaning as follows:
R1: LX => NX
R2: NX => X
R3: L(X=>Y) => LX => LY
R4: MX => LMX
R5: X => LX only when premises of X are 0
R6: N(X=>Y)=>NX=>NY
Here are the definitions of the terms. (== is a definition)
D1 *Ax. Kxx &-(*Ey.y<>x & Kyx) == L(*Ey.y=x)
D2 *Ax. Fx == *Ey. ((y<>x & Lyx) & *Az.Azx==Azy)
D3 *Ax. Sx == Ixx & Cxx
D4a *Ax. Ax == *Ey. (((Sy & Ixy) & Cxy) & Iyx ) & Cyx
D4b *Ax,y. Axy == Ax & CYx
D5a *Ax,y. Mxy == (x<>y & Ixy) & Cxy)
D5b *Ax. Mx == *Ey.(Sy & Mxy)
D6 *Ax. Gx == (Sx & *Ay.Ay=>Ayx) <--- defn. of God!
D7a *Ax. Bx == (Kxx & -*Ey.(y<>x & Kyx))
D7b *Ax. Nx == *Ey.y<>x & Kyx
D8 *Ax. Ex == L(*Ey.y=x)
These are Spinoza's axioms
A1 *Ax. Ixx v *Ey.(y<>x & Ixy)
A2 *Ax. -(*Ey.(y<>x & Cxy)) == Cxx
A3 *Ax,y. Kyx => N( *Eu.u=y == *Eu.u=x )
A4 *Ax,y. Kxy == Cyx
A5 *Ax,y. -(*Ez.Czxy) == -Cxy & -Cyx
A6 *Ax. Kx => (Tx == *Ey.Oyx & Hxy)
A7 *Ax. M - (*Ey.y=x) == - L(*Ey.y=x)
Some extra necessary axioms, ommitted by Spinoza
A8 *Ax,y. Ixy -> Cxy
A9 *Ax. *Ey.Ayx
A10 *Axyz. Dxyz -> M -(*Ew.w=x)
A11 *Ax,y. (Sx & Lyx) -> Sy
A12 *Ax. (*Ey. Mxy->Mx)
A13 M(*Ex.Gx)
A14 *Ax. N(*Ey.y=x) == -Fx)
A15 *Ax. ( -Fx -> [(-L(*Ey.y=x) & N(*Ey.y=x)) == *At.(*Ey.y.y=x at t)]
A16 *Ax,y. (*Ez.Azx & Azy) -> *Ez.Czxy
A17a *Ax. Ux -> -Ax
A17b *Ax. Wx -> -Ax
A17c *Ax. Dx -> -Ax
A17d *Ax. Jx -> -Ax
A18 *Ax,y. (Sx & Sy) -> (Rxy -> Vxy)
A19 *Ax,y. ((Ixy & Cxy)&Iyx)&Cyx == Pxy
Here are a few derivations
DP1 *Ax.Sx==Ixx from D3,A8
DP2 *Ax.Cxx->Ixx from A1,A2,A8
DP3 *Ax.Sx->Ax from D3,D4a
DP4 *Ax.Sx=Cxx from D3,DP2
DP5 *Ax.Sx v Mx from A1,A8,A12,D5a,DP1
DP6 *Ax.-(Sx & Mx) from D3,D5a,D5b,A2
DP7 *Ax,y. (Axy & Sy) -> x=y) from D3,D4b,A2
These are the first 11 propositions in Spinoza's Ethics
P1 *Ax,y. Mxy & Sy -> Ixy & Iyy from D5a,D3
P2 *Ax,y. (Sx & Sy) & x<>y -> -(*Ez.Czxy) from D3,A2,A5
P3 *Ax,y. -(*Ez.Czxy) -> -Kxy & -Kyx from A4,A5
P4 *Ax,y. x<>y -> *Ez,z'. [((((Azx&Az'x)&z<>z') v ((Azx & z=x)&My))
v ((Az'y & z'=y)&Mx)) v (Mx & My) from A9,Dp5,DP6,DP7
P5 *Ax,y. (Sx & Sy) & x<>y -> -(*Ew.Awx & Awy) from DP7
P6 *Ax,y. (Sx & Sy) & x<>y -> -(Kxy & -Kyx) from P2,P3
P6c *Ax. Sx -> -(*Ey. y<>x & Kyx) from D3,A2,A4
P7 *Ax. Sx -> L(*Ey.y=x) from D3,P6c,A4,D1
P8 *Ax. Sx -> -Fx from D2,A9,A11,P5
P9 *Ax,y. (Sx & Sy) -> (Rxy -> Vxy) from A18
P10 *Ax. Ax -> Cxx from D3,D4a and A2
P11 L (*Ex.Gx) <------ that God exists!
from D1,D3,D4a,D4b,D6,A1,A2,A4,A8,D9
And there we have it!
Your Peace, Surrender, In You,
YHVH Re-connect Co-operative |
Forum 