Event: Start with the initial nqthm theory.

;;; The proof in here is based on the hint to exercise (8) on
;;; page 43 of Kunen's Set Theory book.
;; Imagine sets a and b and corresponding functions fa and fb which
;; map a to b and vice-versa, where both are one-one.

Definition: id (x) = x

Conservative Axiom: fa-and-fb-are-one-one ((a (x) ∧ a (y) ∧ (x ≠ y)) → (fa (x) ≠ fa (y))) ∧ ((b (x) ∧ b (y) ∧ (x ≠ y)) → (fb (x) ≠ fb (y))) ∧ (a (x) → b (fa (x))) ∧ (b (x) → a (fb (x))) ∧ (truep (a (x)) ∨ falsep (a (x))) ∧ (truep (b (x)) ∨ falsep (b (x)))

Simultaneously, we introduce the new function symbols fa, fb, a, and b.

Definition: in-fa-range (x) ↔ ∃ fa-1 (a (fa-1 ) ∧ (fa (fa-1 ) = x))

;; The following 3 events were generated automatically to help with
;; the proof-checker's application of the macro command SK*.

Event: Disable in-fa-range.

Theorem: in-fa-range-suff (a (fa-1 ) ∧ (fa (fa-1 ) = x)) → in-fa-range (x)

Theorem: in-fa-range-necc (¬ (a (fa-1 (x)) ∧ (fa (fa-1 (x)) = x))) → (¬ in-fa-range (x))

Definition: in-fb-range (x) ↔ ∃ fb-1 (b (fb-1 ) ∧ (fb (fb-1 ) = x))

;; The following 3 events were generated automatically to help with
;; the proof-checker's application of the macro command sk*.

Event: Disable in-fb-range.

Theorem: in-fb-range-suff (b (fb-1 ) ∧ (fb (fb-1 ) = x)) → in-fb-range (x)

Theorem: in-fb-range-necc (¬ (b (fb-1 (x)) ∧ (fb (fb-1 (x)) = x))) → (¬ in-fb-range (x))

Definition: circled (flg, x, n) = if flg = 'a

then if n ≃ 0 then a (x)

else in-fb-range (x) ∧ circled ('b, fb-1 (x), n − 1) endif elseif n ≃ 0 then b (x) else in-fa-range (x) ∧ circled ('a, fa-1 (x), n − 1) endif

Definition: a-core (x) ↔ (a (x)

∧ ∀ a-level (((a-level ∈ N) ∧ circled ('a, x, a-level)) → circled ('a, x, 1 + a-level)))

Event: Disable a-core.

Theorem: a-core-necc-base ((n ≃ 0) ∧ a-core (x)) → circled ('a, x, n)

Theorem: a-core-necc-induction ((n ≄ 0) ∧ a-core (x) ∧ circled ('a, x, n − 1)) → circled ('a, x, n)

Theorem: a-core-necc (¬ circled ('a, x, n)) → (¬ a-core (x))

Event: Disable a-core-necc-base.

Event: Disable a-core-necc-induction.

Theorem: a-core-suff (a (x) ∧ (((a-level (x) ∈ N) ∧ circled ('a, x, a-level (x)))

→ circled ('a, x, 1 + a-level (x)))) → a-core (x)

Definition: b-core (x) ↔ (b (x)

∧ ∀ b-level (((b-level ∈ N) ∧ circled ('b, x, b-level)) → circled ('b, x, 1 + b-level)))

Event: Disable b-core.

Theorem: b-core-necc-base ((n ≃ 0) ∧ b-core (x)) → circled ('b, x, n)

Theorem: b-core-necc-induction ((n ≄ 0) ∧ b-core (x) ∧ circled ('b, x, n − 1)) → circled ('b, x, n)

Theorem: b-core-necc (¬ circled ('b, x, n)) → (¬ b-core (x))

Event: Disable b-core-necc-base.

Event: Disable b-core-necc-induction.

Theorem: b-core-suff (b (x) ∧ (((b-level (x) ∈ N) ∧ circled ('b, x, b-level (x)))

→ circled ('b, x, 1 + b-level (x)))) → b-core (x)

Definition: parity (n) = if n ≃ 0 then t

else ¬ parity (n − 1) endif

Definition: j (x) = if a-core (x) ∨ parity (a-level (x)) then fa (x)

else fb-1 (x) endif

Definition: j-1 (y) = if b-core (y) ∨ (¬ parity (b-level (y))) then fa-1 (y)

else fb (y) endif

; Our goals:
;(prove-lemma j-1-j (rewrite)
;  (implies (a x)
;           (equal (j-1 (j x)) x)))
;(prove-lemma j-j-1 (rewrite)
;  (implies (b y)
;           (equal (j (j-1 y)) y)))

;; We'll start on the first of these.  The theorem-prover output
;; suggests the following lemma:
;(prove-lemma b-core-fa (rewrite)
;  (implies (a x)
;           (iff (b-core (fa x))
;                (a-core x))))
;; A main lemma is that (a-core x) => (b-core (fa x)) for x in a.

Theorem: fa-1-inverts-fa a (x) → (fa-1 (fa (x)) = x)

;; The following is useful for proof-checker rewriting:

Theorem: in-fa-range-fa a (x) → in-fa-range (fa (x))

Theorem: b-core-fa a (x) → (b-core (fa (x)) ↔ a-core (x))

;; On to Case 2 of j-1-j.  We find there the following contradictory hyps:
;(AND (A X)
;     (PARITY (A-LEVEL X))
;     (NOT (A-CORE X))
;     (PARITY (B-LEVEL (FA X))))
;; We want to prove:
;; B-LEVEL-FA
;(IMPLIES (AND (A X) (NOT (A-CORE X)))
;         (EQUAL (B-LEVEL (FA X))
;                (ADD1 (A-LEVEL X))))

Theorem: b-fa-equality-rewrite (a (x) ∧ (¬ b (y))) → (fa (x) ≠ y)

Theorem: fa-range-contained-in-b (¬ b (y)) → (¬ in-fa-range (y))

Theorem: circled-implies-b circled ('b, y, n) → b (y)

Theorem: a-fb-equality-rewrite (b (y) ∧ (¬ a (x))) → (fb (y) ≠ x)

Theorem: fb-range-contained-in-a (¬ a (x)) → (¬ in-fb-range (x))

Theorem: circled-implies-a circled ('a, y, n) → a (y)

Theorem: circled-monotone (circled (flg, x, j ) ∧ (j ≮ i)) → circled (flg, x, i)

Theorem: circled-b-fa a (x) → (circled ('b, fa (x), n) = circled ('a, x, n − 1))

Theorem: b-level-fa-hack-lemma (b-level (fa (x)) ∈ N) → ((b-level (fa (x)) = (1 + a-level (x)))

= (¬ ((b-level (fa (x)) < (1 + a-level (x))) ∨ ((1 + a-level (x)) < b-level (fa (x))))))

Theorem: b-level-fa (a (x) ∧ (¬ a-core (x))) → (b-level (fa (x)) = (1 + a-level (x)))

;; On to Case 3 of j-1-j.  Our first subgoal is:
;(IMPLIES (AND (A X)
;              (NOT (A-CORE X))
;              (NOT (PARITY (A-LEVEL X)))
;              (NOT (B-CORE (FB-1 X)))
;              (PARITY (B-LEVEL (FB-1 X))))
;         (EQUAL (FB (FB-1 X)) X))
;; and this follows from the following two lemmas.

Theorem: not-parity-a-level-implies-in-fb-range (a (x) ∧ (¬ parity (a-level (x)))) → in-fb-range (x)

;; The next subcase of j-1-j is:
;(implies (and (a x)
;              (not (a-core x))

;              (not (parity (a-level x)))
;              (not (parity (b-level (fb-1 x)))))
;         (equal (fa-1 (fb-1 x)) x))
;; and this follows from:
;(prove-lemma b-level-fb-1 (rewrite)
;  (implies (and (a x)
;                (not (a-core x))
;                (in-fb-range x))
;           (equal (b-level (fb-1 x))
;                  (sub1 (a-level x)))))
;; I've proved nearly the analogous thing already for fa.  Let's prove that
;; one for fb and then deduce this from it.

Theorem: fb-1-inverts-fb b (x) → (fb-1 (fb (x)) = x)

Theorem: in-fb-range-fb b (x) → in-fb-range (fb (x))

Theorem: circled-a-fb b (x) → (circled ('a, fb (x), n) = circled ('b, x, n − 1))

Theorem: a-level-fb-hack-lemma (a-level (fb (x)) ∈ N) → ((a-level (fb (x)) = (1 + b-level (x)))

= (¬ ((a-level (fb (x)) < (1 + b-level (x))) ∨ ((1 + b-level (x)) < a-level (fb (x))))))

Theorem: a-core-fb b (x) → (a-core (fb (x)) ↔ b-core (x))

Theorem: a-level-fb (b (x) ∧ (¬ b-core (x))) → (a-level (fb (x)) = (1 + b-level (x)))

Theorem: b-level-fb-1 (a (x) ∧ (¬ a-core (x)) ∧ in-fb-range (x)) → (b-level (fb-1 (x)) = (a-level (x) − 1))

;; It remains only to prove the following subcase, and then we're done with j-1-j:
;(implies (and (a x)

;              (not (a-core x))
;              (not (parity (a-level x)))
;              (b-core (fb-1 x)))
;         (equal (fa-1 (fb-1 x)) x))
;; I've already proved a-core-fb, and this should be useful.

Theorem: b-core-implies-b b-core (x) → b (x)

Theorem: fb-fb-1 (a (x) ∧ in-fb-range (x)) → (fb (fb-1 (x)) = x)

Theorem: b-core-fb-1 (a (x) ∧ (¬ a-core (x)) ∧ (¬ parity (a-level (x)))) → (¬ b-core (fb-1 (x)))

;; Now finally for our first main goal:

Theorem: j-1-j a (x) → (j-1 (j (x)) = x)

;;;; We're ready now for the converse.  Here's the first sticking point:
;(implies (and (b-core y)
;              (a-core (fa-1 y)))
;         (equal (fa (fa-1 y)) y))
;; We need only the following two easy lemmas:

Theorem: b-core-implies-in-fa-range b-core (y) → in-fa-range (y)

Theorem: fa-fa-1 in-fa-range (y) → (fa (fa-1 (y)) = y)

;; Our next goal is:
;(implies (and (b-core y)
;              (not (a-core (fa-1 y)))
;              (not (parity (a-level (fa-1 y)))))
;         (equal (fb-1 (fa-1 y)) y))
;;; which is taken care of simply by:

Theorem: a-core-fa-1 in-fa-range (y) → (a-core (fa-1 (y)) ↔ b-core (y))

;; next we have to prove
;(implies (and (b y)
;              (not (parity (b-level y)))
;              (a-core (fa-1 y)))
;         (equal (fa (fa-1 y)) y))
;; which follows from fa-fa-1 together with an obvious analog of
;; NOT-PARITY-A-LEVEL-IMPLIES-IN-FB-RANGE:

Theorem: not-parity-b-level-implies-in-fa-range (b (y) ∧ (¬ parity (b-level (y)))) → in-fa-range (y)

;; It remains only to prove:
;(implies (and (b y)
;              (not (parity (b-level y)))
;              (not (b-core y))
;              (not (parity (a-level (fa-1 y)))))
;         (equal (fb-1 (fa-1 y)) y))
;; which follows from an analogue of B-LEVEL-FB-1:

Theorem: a-level-fa-1 (b (y) ∧ (¬ b-core (y)) ∧ in-fa-range (y)) → (a-level (fa-1 (y)) = (b-level (y) − 1))

;;; and we're done!!!

Theorem: j-j-1 b (y) → (j (j-1 (y)) = y)

;; To summarize:
;; From the axiom saying that fa maps a one-one into b and fb maps b one-one into a,
;(constrain fa-and-fb-are-one-one (rewrite)
;  (and (implies (and (a x) (a y) (not (equal x y)))
;                (not (equal (fa x) (fa y))))

;       (implies (and (b x) (b y) (not (equal x y)))
;                (not (equal (fb x) (fb y))))
;       (implies (a x) (b (fa x)))
;       (implies (b x) (a (fb x)))
;       (or (truep (a x)) (falsep (a x)))
;       (or (truep (b x)) (falsep (b x))))
;  ((fa id) (fb id) (a (lambda (x) t)) (b (lambda (x) t))))
;; to finish this off we simply prove the obvious lemmas needed for
;; j-iso below.  For the first, j-range,
;; we need a lemma (as seen from observing the failed proof transcript).

Theorem: in-fb-range-implies-b-fb-1 in-fb-range (y) → b (fb-1 (y))

Theorem: j-range a (x) → b (j (x))

Theorem: in-fa-range-implies-a-fa-1 in-fa-range (y) → a (fa-1 (y))

Theorem: j-1-range b (x) → a (j-1 (x))

Event: Disable j.

Event: Disable j-1.

Theorem: j-is-one-one (a (x1 ) ∧ a (x2 ) ∧ (x1 ≠ x2 )) → (j (x1 ) ≠ j (x2 ))

;; we were able to conservatively extend the theory culminating in
;; definitions of a function j which maps a one-one into b:

Definition: j-iso ↔ (∀ x (a (x) → b (j (x)))

∧ ∀ x1 , x2 ((a (x1 ) ∧ a (x2 ) ∧ (j (x1 ) = j (x2 )))

→ (x1 = x2 )) ∧ ∀ y (b (y) → ∃ x (a (x) ∧ (j (x) = y))))

Theorem: j-is-an-isomorphism j-iso

Index

a, 1, 2, 4–7, 9 a-core, 2–8 a-core-fa-1, 8 a-core-fb, 6 a-core-necc, 2 a-core-necc-base, 2 a-core-necc-induction, 2 a-core-suff, 2 a-fb-equality-rewrite, 5 a-level, 2, 3, 5–8 a-level-fa-1, 8 a-level-fb, 6 a-level-fb-hack-lemma, 6

b, 1–9 b-core, 2–4, 6–8 b-core-fa, 4 b-core-fb-1, 7 b-core-implies-b, 7 b-core-implies-in-fa-range, 7 b-core-necc, 3 b-core-necc-base, 3 b-core-necc-induction, 3 b-core-suff, 3 b-fa-equality-rewrite, 4 b-level, 3, 5, 6, 8 b-level-fa, 5 b-level-fa-hack-lemma, 5 b-level-fb-1, 6

circled, 2, 3, 5, 6 circled-a-fb, 6 circled-b-fa, 5 circled-implies-a, 5 circled-implies-b, 5 circled-monotone, 5

exists, 1, 9

fa, 1, 3–5, 7 fa-1, 1–4, 7–9 fa-1-inverts-fa, 4 fa-and-fb-are-one-one, 1 fa-fa-1, 7 fa-range-contained-in-b, 4 fb, 1–3, 5–7 fb-1, 2, 3, 6, 7, 9 fb-1-inverts-fb, 6 fb-fb-1, 7 fb-range-contained-in-a, 5 forall, 2, 9

id, 1

in-fa-range, 1, 2, 4, 7–9

in-fa-range-fa, 4

in-fa-range-implies-a-fa-1, 9 in-fa-range-necc, 1 in-fa-range-suff, 1 in-fb-range, 1, 2, 5–7, 9 in-fb-range-fb, 6 in-fb-range-implies-b-fb-1, 9 in-fb-range-necc, 2 in-fb-range-suff, 2

j, 3, 7–9 j-1, 3, 7–9 j-1-j, 7 j-1-range, 9 j-is-an-isomorphism, 9 j-is-one-one, 9 j-iso, 9 j-j-1, 8 j-range, 9

not-parity-a-level-implies-in-f

b-range, 5 not-parity-b-level-implies-in-f

a-range, 8

parity, 3, 5, 7, 8