On #(PS) = 2#S
Theorem (11.73) states that for Theorem (11.73) states that for S finite, PS is finite and #(PS) = 2#S. A proof would require mathematical induction. The idea is to show that each time one adds a new element to a finite set, the power set doubles in size.


For s Î S, S = (S-{s}) È{s}, and the induction would follow from the following


Theorem: For S finite,
|-  s Î S     Þ    #(PS)    =    2·#(P(S - {s})) .
Let y be a fresh variable. We have


Lemma:
|-  #PS      =     ( å
 		y | s Î y   Ù  y Í S:1) + ( å
 		y | s \not Î y   Ù  y Í S:1)  .
#PS
=

(11.12)

( å
 		y | y Î PS : 1)
=

(11.23)

( å
 		y | y Í S : 1)
=

(3.28), (3.39)

( å
 		y | (s Î y   Ú  s Ï y)   Ù   (y Í S) : 1)
=

(3.46)

( å
 		y | (s Î y   Ù  y Í S)  Ú  (s Ï y   Ù   y Í S) : 1)
=

(8.16), |- (s Î y   Ù  y Í S) Ù(s Ï y   Ù   y Í S)   º   false

( å
 		y | s Î y   Ù  y Í S:1) + ( å
 		y | s \not Î y   Ù  y Í S:1)  .
The theorem is proved once we show
|-  ( å
 		y | s \not Î y   Ù  y Í S:1)      =     #(P(S - {s}))
and
|-  s Î S    Þ    ( å
 		y | s Î y   Ù  y Í S:1)      =     ( å
 		y | s \not Î y   Ù  y Í S:1)  .
Lemma:
|-  ( å
 		y | s \not Î y   Ù  y Í S:1)      =     #(P(S - {s})) .
This follows from Leibniz on ranges once we prove
|- s \not Î y   Ù  y Í S      º     y Í S - {s} .
Let x be a fresh variable.
s \not Î y   Ù  y Í S
=

(11.3), x d.n.o.f. in s, (11.13)

Ø($x | x Î y : s = x)   Ù  ("x | x Î y: x Î S)
=

(9.18)(b)

("x | x Î y : s ¹ x)   Ù  ("x | x Î y: x Î S)
=

(8.15)

("x | x Î y : s ¹ x   Ù  x Î S)
=

Notation, (1.3)

("x | x Î y : Ø(x = s)   Ù  x Î S)
=

|- x = s   º   x Î {s}

("x | x Î y : Ø(x Î {s})   Ù  x Î S)
=

(11.22)

("x | x Î y : x Î S -{s})
=

(11.13)

y Í S - {s}
To prove
|-  s Î S    Þ    ( å
 		y | s Î y   Ù  y Í S:1)      =     ( å
 		y | s \not Î y   Ù  y Í S:1)  .
consider the following


Lemma (Dow):
|- s Î z  Ù  y = z-{s}      º     s Ï y   Ù  z = yÈ{s}  .
Let x be a fresh variable.
s Î z  Ù  y = z-{s}
=

(8.14), x d.n.o.f. in s, (11.4), (11.22)

("x | x = s:x Î z)   Ù  ("x | :x Î y    º   x Î z   Ù  x Ï {s})
=

|-  x = s   º   x Î {s}

("x | x Î {s}:x Î z)   Ù  ("x | :x Î y    º   x Î z   Ù  x Ï {s})
=

(3.11), (3.47)(a)

("x | x Î {s}:x Î z)   Ù  ("x | :x\not Î y    º   x\not Î z   Ú  x Î {s})
=

(3.80), (8.15), (9.2)

("x | x Î {s}:x Î z)   Ù  ("x | x\not Î y :x\not Î z   Ú  x Î {s})   Ù  ("x | x\not Î z   Ú  x Î {s} : x\not Î y )
=

(8.18)

("x | x Î {s}:x Î z)   Ù  ("x | x\not Î y :x\not Î z   Ú  x Î {s})   Ù  ("x | x\not Î z: x\not Î y )   Ù  ("x | x Î {s} : x\not Î y )
=

(3.36)

("x | x Î {s} : x\not Î y )   Ù  (" x | x Î {s}:x Î z)   Ù  ("x | x\not Î y :x\not Î z   Ú  x Î {s})   Ù  ("x | x\not Î z: x\not Î y )
=

(9.2), (3.61), (9.2)

("x | x Î {s} : x\not Î y )   Ù  (" x | x Î {s}:x Î z)   Ù  ("x | x\not Î y :x\not Î z   Ú  x Î {s})   Ù  ("x | x Î y: x Î z )
=

(9.2), |- ØPÞ Ø Q ÚR    º   Q Þ PÚR, (9.2)

("x | x Î {s} : x\not Î y )   Ù  (" x | x Î {s}:x Î z)   Ù  ("x | x Î z : x Î y   Ú  x Î {s})   Ù  ("x | x Î y: x Î z )
=

(3.36)

("x | x Î {s} : x\not Î y )   Ù  (" x | x Î z : x Î y   Ú  x Î {s})   Ù  ("x | x Î y: x Î z )   Ù  (" x | x Î {s}:x Î z)
=

(8.18)

("x | x Î {s} : x\not Î y )   Ù  (" x | x Î z : x Î y   Ú  x Î {s})   Ù  ("x | x Î y   Ú  x Î {s}: x Î z)
=

(9.2), (8.15), (3.80)

("x | x Î {s} : x\not Î y )   Ù  (" x | :x Î z    º   x Î y   Ú  x Î {s})
=

|-  x = s   º   x Î {s}

("x | x = s : x\not Î y )   Ù  (" x | :x Î z    º   x Î y   Ú  x Î {s})
=

(8.14), x d.n.o.f. in s, (11.20), (11.4)

s Ï y   Ù  z = yÈ{s}  .
Assume s Î S. Recall that y d.n.o.f. s, S. Let z be a fresh variable.
( å
 		y  | s Î y  Ù  y Í S :1)
=

(8.21), z d.n.o.f. s Î y  Ù  y Í S , 1

( å
 		z  | s Î z  Ù  z Í S :1)
=

(8.,14), y d.n.o.f. z-{s}

( å
 		z  | s Î z  Ù  z Í S : ( å
 		y | y = z-{s} : 1))
=

(8.20), y d.n.o.f. s Î z  Ù  z Í S

( å
 		z, y  | s Î z  Ù  z Í S   Ù   y = z-{s}: 1)
=

Lemma (Dow)

( å
 		z, y  | s\not Î y   Ù   z = y È{s}   Ù  z Í S : 1)
=

á
|- ( å
 		z,y | R:P) = ( å
 		y,z | R:P)

ñ
( å
 		y, z  | s\not Î y   Ù   z = y È{s}   Ù  z Í S : 1)
=

(3.84)(a)

( å
 		y, z  | s\not Î y   Ù   z = y È{s}   Ù  y È{s} Í S : 1)
=

(8.20), z d.n.o.f. s\not Î y   Ù   z = y È{s}

( å
 		y  | s\not Î y   Ù  y È{s} Í S : ( å
 		z | z = y È{s}:1))
=

(8.14), z d.n.o.f. y È {s}

( å
 		y  | s\not Î y   Ù  y È{s} Í S : 1)
=

|- s Î S    Þ     y È{s} Í S º y Í S, Assumption

( å
 		y  | s\not Î y   Ù  y Í S : 1)
from which
|-  s Î S    Þ    ( å
 		y | s Î y   Ù  y Í S:1)      =     ( å
 		y | s \not Î y   Ù  y Í S:1)
as required.

File translated from TEX by TTH, version 2.60.
On 4 Feb 2001, 13:50.