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.