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      =     (
| s y     y S:1) + (
| s \not y     y S:1)  .

#PS
=

(11.12)

(
| y PS : 1)
=

(11.23)

(
| y S : 1)
=

(3.28), (3.39)

(
| (s y     s y)      (y S) : 1)
=

(3.46)

(
| (s y     y S)    (s y      y S) : 1)
=

(8.16), |- (s y     y S) (s y      y S)     false

(
| s y     y S:1) + (
| s \not y     y S:1)  .
The theorem is proved once we show
|-  (
| s \not y     y S:1)      =     #(P(S - {s}))
and
|-  s S        (
| s y     y S:1)      =     (
| s \not y     y S:1)  .
Lemma:
|-  (
| 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 y : s = x)     ("| x y: x S)
=

(9.18)(b)

("| x y : s x)     ("| x y: x S)
=

(8.15)

("| x y : s x     x S)
=

Notation, (1.3)

("| x y : (x = s)     x S)
=

|- x = s     x {s}

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

(11.22)

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

(11.13)

y S - {s}
To prove
|-  s S        (
| s y     y S:1)      =     (
| 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 = s:x z)     ("| :x y      x z     x {s})
=

|-  x = s     x {s}

("| x {s}:x z)     ("| :x y      x z     x {s})
=

(3.11), (3.47)(a)

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

(3.80), (8.15), (9.2)

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

(8.18)

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

(3.36)

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

(9.2), (3.61), (9.2)

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

(9.2), |- P Q R      Q PR, (9.2)

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

(3.36)

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

(8.18)

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

(9.2), (8.15), (3.80)

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

|-  x = s     x {s}

("| x = s : x\not y )     ("| :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 = 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 = 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        (
| s y     y S:1)      =     (
| s \not y     y S:1)
as required.


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