a uniqueness theorem for id[GAMES]

Johan G. F. Belinfante
2012 May 19

SetDirectory["l:"]; << goedel.12may16a

summary

The class  GAMES  of Conway games is constructed recursively, each game being an ordered pair of sets of previously constructed games, called the options for the players "left" and "right".   A game  x  is a prelude to a game  y  if  x  is one of the left or right options of the game  y.  Formally the relation  PRELUDE  is defined by the following rewrite rule (equation):

union[composite[id[GAMES], inverse[FIRST], E], 
      composite[id[GAMES], inverse[SECOND], E]]

The relation PRELUDE is well-founded and its inverse is thin, that is, every vertical section of  PRELUDE  is a set.  The relation  PRELUDE  is used in the theory of Conway games both to provide recursive definitions of important theorems, and to provide a convenient way to prove theorems about games inductively.  In this notebook, the basic theorems for proofs by prelude induction are derived, and illustrated on the proof of a basic theorem that which characterizes the identity function id[GAMES] which takes any game to itself as the unique solution of a certain recursion equation.

prelude-induction

The relation  PRELUDE  is well-founded and its inverse is thin.  On account of this, the following form of well-founded induction holds:

Theorem.  A basic form of prelude induction.

SubstTest[implies, 
        and[WELLFOUNDED[w], thin[inverse[w]], subvariant[w, x]], empty[x], 
        w -> PRELUDE] // Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Corollary.  (A better rewrite rule for prelude induction.)

equiv[subclass[x, image[PRELUDE, x]], equal[0, x]]

subclass[x_, image[PRELUDE, x_]] := equal[0, x]

Many proofs using prelude induction operate by showing that there can be no least counterexample.  The following theorem provides this version of prelude induction.  It will be used in the proof of theorem characterizing id[GAMES].

Theorem.  A "no least counterexample" form of prelude induction that will be used for an application provided below.

SubstTest[subclass, t, image[PRELUDE, t], t -> dif[GAMES, x]] // 
      Reverse

subclass[GAMES, union[x_, image[PRELUDE, complement[x_]]]] := 
      subclass[GAMES, x]

a recursion equation satisfied by id[GAMES].

Theorem.  A recursion equation for id[GAMES].

SubstTest[composite, cross[IMAGE[id[GAMES]], IMAGE[id[GAMES]]], 
        id[cart[P[t], P[t]]], t -> GAMES] // Reverse

composite[cross[IMAGE[id[GAMES]], IMAGE[id[GAMES]]], id[GAMES]] := 
      id[GAMES]

It will be shown later that  w = id[GAMES]  is the only solution of the recursion equation  w = (IMAGE[w] ⊗ IMAGE[w])  ∘ id[GAMES].  In the present section some elementary consequences of the recursion equation are derived.  In the first place, w must be a function.  The GOEDEL program recognizes this automatically using the built-in rewrite rules for equality; no proof is needed.

implies[equal[w, composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]]], 
      FUNCTION[w]]

It is often useful in deriving consequences of the recursion equation to begin by adding a funpart wrapper, and then removing this wrapper.  An example of this is the following.

Lemma.  (This contains the redundant literal FUNCTION[w].)

SubstTest[implies, 
        and[equal[w, funpart[t]], 
          equal[w, composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]]]], 
        equal[domain[w], GAMES], t -> w] // Reverse

(% /. w -> w_) /. Equal -> SetDelayed

Theorem.  The recursion equation implies domain[w] = GAMES.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
          not[implies[p1, p3]], {p1 -> 
              equal[w, composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]]], 
            p2 -> FUNCTION[w], p3 -> equal[domain[w], GAMES]}]] // 
      Reverse

or[equal[GAMES, domain[w_]], 
        not[equal[w_, composite[cross[IMAGE[w_], IMAGE[w_]], id[GAMES]]]]] := 
      True

Lemma.  A recursion equation involving APPLY.

SubstTest[implies, equal[w, t], 
        equal[APPLY[w, z], 
          APPLY[t, z]], {t -> 
            composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]], 
          z -> game[x]}] // Reverse

or[equal[APPLY[w_, game[x_]], 
          PAIR[image[w_, first[game[x_]]], image[w_, second[game[x_]]]]], 
        not[equal[w_, composite[cross[IMAGE[w_], IMAGE[w_]], id[GAMES]]]]] := 
      True

simplification rules for game[x]

It will be useful to introduce the wrapper game[x] in subsequent work.

Lemma.  The vertical section of inverse[PRELUDE] at games[x].

SubstTest[APPLY, VERTSECT[t], game[x], 
      t -> inverse[PRELUDE]]

image[inverse[PRELUDE], set[game[x_]]] := 
      union[first[game[x]], second[game[x]]]

Lemma.  Simplification rule.

equal[intersection[GAMES, first[game[x]]], first[game[x]]]

intersection[GAMES, first[game[x_]]] := first[game[x]]

Lemma.  Dual simplification rule.

equal[intersection[GAMES, second[game[x]]], second[game[x]]]

intersection[GAMES, second[game[x_]]] := second[game[x]]

Lemma.

equal[PAIR[first[game[x]], second[game[x]]], game[x]]

PAIR[first[game[x_]], second[game[x_]]] := game[x]

Lemma.

SubstTest[set, PAIR[first[t], second[t]], t -> game[x]]

cart[set[first[game[x_]]], set[second[game[x_]]]] := 
      set[game[x]]

derivation of the main theorem

The variable  w  will be wrapped with funpart for most of the derivation.

Lemma.

Map[
          implies[subclass[union[first[game[x]], second[game[x]]], 
                fix[funpart[w]]], #] &, 
          SubstTest[member, PAIR[u, v], 
            cart[set[first[t]], 
              set[second[t]]], {u -> image[funpart[w], first[game[x]]], 
              v -> image[funpart[w], second[game[x]]], t -> game[x]}]] // 
        MapNotNot // Reverse

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

Theorem.   If every prelude of  game[x]  is a fixed point of a solution  funpart[w]  of the recursion equation, then so is  game[x]  itself.

Map[not, 
        SubstTest[and, implies[p0, p4], implies[p1, p2], implies[p2, p3], 
          implies[and[p3, p4], p5], 
          not[implies[and[p0, p1], p5]], {p0 -> 
              and[subclass[first[game[x]], fix[funpart[w]]], 
                subclass[second[game[x]], fix[funpart[w]]]], 
            p1 -> 
              equal[composite[cross[IMAGE[funpart[w]], IMAGE[funpart[w]]], 
                  id[GAMES]], funpart[w]], 
            p2 -> 
              equal[APPLY[funpart[w], game[x]], 
                PAIR[image[funpart[w], first[game[x]]], 
                  image[funpart[w], second[game[x]]]]], 
            p3 -> equal[APPLY[funpart[w], game[x]], 
                pair[image[funpart[w], first[game[x]]], 
                  image[funpart[w], second[game[x]]]]], 
            p4 -> equal[game[x], 
                pair[image[funpart[w], first[game[x]]], 
                  image[funpart[w], second[game[x]]]]], 
            p5 -> equal[APPLY[funpart[w], game[x]], game[x]]}]] // 
      Reverse

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

Corollary.   (Eliminating APPLY from the statement in the theorem.)

Map[not, 
        SubstTest[and, implies[and[p0, p1], p3], implies[p1, p2], 
          implies[p2, p4], implies[and[p3, p4], p5], 
          not[implies[and[p0, p1], p5]], {p0 -> 
              and[subclass[first[game[x]], fix[funpart[w]]], 
                subclass[second[game[x]], fix[funpart[w]]]], 
            p1 -> 
              equal[composite[cross[IMAGE[funpart[w]], IMAGE[funpart[w]]], 
                  id[GAMES]], funpart[w]], 
            p2 -> equal[domain[funpart[w]], GAMES], 
            p3 -> equal[APPLY[funpart[w], game[x]], game[x]], 
            p4 -> member[game[x], domain[funpart[w]]], 
            p5 -> member[game[x], fix[funpart[w]]]}]] // 
      Reverse

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

Theorem.  (Eliminate the funpart wrapper.)

SubstTest[implies, equal[w, funpart[t]], 
        or[member[game[x], fix[w]], 
          not[equal[w, composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]]]], 
          not[subclass[first[game[x]], fix[w]]], 
          not[subclass[second[game[x]], fix[w]]]], t -> w] // 
      Reverse

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

Theorem.  (Eliminate the redundant FUNCTION[w] literal.)

Map[not, 
        SubstTest[and, implies[p1, p3], implies[and[p1, p2, p3], p4], 
          not[implies[and[p1, p2], p4]], {p1 -> 
              equal[w, composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]]], 
            p2 -> 
              and[subclass[first[game[x]], fix[w]], 
                subclass[second[game[x]], fix[w]]], p3 -> FUNCTION[w], 
            p4 -> member[game[x], fix[w]]}]] // Reverse

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

The elimination of the game wrapper in the following theorem is taken as an opportunity to formally introduce the PRELUDE relation.

Theorem.

SubstTest[implies, 
        and[equal[x, game[t]], 
          equal[w, composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]]], 
          subclass[image[inverse[PRELUDE], set[x]], fix[w]]], 
        member[x, fix[w]], t -> x] // Reverse

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

The variable  x  here will be eliminated using  reify  and  case, and the no-least-counterexample form of prelude induction automatically simplifies the result.

Theorem.  If  w  is a solution of the recursion equation, then  GAMES ⊂ fix[w].

Map[equal[V, domain[#]] &, 
      SubstTest[reify, x, 
        case[or[member[x, fix[w]], not[equal[w, t]], not[member[x, GAMES]], 
            not[subclass[image[inverse[PRELUDE], set[x]], fix[w]]]]], 
        t -> composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]]]]

(% /. w -> w_) /. Equal -> SetDelayed

Identity functions can be characterized as functions  w  that satisfy  domain[w] ⊂ fix[w].

Lemma.

SubstTest[implies, equal[w, funpart[t]], 
        or[equal[w, id[x]], not[equal[x, domain[w]]], 
          not[subclass[x, fix[w]]]], t -> w] // Reverse

(% /. {w -> w_, x -> x_}) /. 
      Equal -> SetDelayed

Main Theorem.  The only solution of the recursion equation   w = (IMAGE[w] ⊗ IMAGE[w])  ∘ id[GAMES]  is  w = id[GAMES].

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], implies[p1, p4], 
          implies[and[p2, p3, p4], p5], 
          not[implies[p1, p5]], {p1 -> 
              equal[w, composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]]], 
            p2 -> FUNCTION[w], p3 -> equal[domain[w], GAMES], 
            p4 -> subclass[GAMES, fix[w]], 
            p5 -> equal[w, id[GAMES]]}]] // Reverse

(% /. w -> w_) /. Equal -> SetDelayed

Corollary.   A better rewrite rule.

equiv[equal[w, composite[cross[IMAGE[w], IMAGE[w]], id[GAMES]]], 
      equal[w, id[GAMES]]]

equal[w_, composite[cross[IMAGE[w_], IMAGE[w_]], id[GAMES]]] := 
      equal[w, id[GAMES]]