:: Boolos' Curious Inference
:: Complete Proof
:: Author: Chad E Brown

environ

 vocabularies FUNCT_1, FINSEQ_1, RELAT_1, FINSET_1, CARD_1,
   BOOLE, PARTFUN1, ARYTM_1, INT_1, RLSUB_2, TARSKI, FINSEQ_4,
   ORDINAL2, ARYTM, ZFMISC_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1,
   ORDINAL2, RELAT_1, NUMBERS, XCMPLX_0, FINSEQ_1, FUNCT_1,
   PARTFUN1, CARD_1, FUNCT_2, FINSET_1, INT_1, NAT_1, FINSEQ_3,
   XXREAL_0, ZFMISC_1, RELSET_1;
 constructors TARSKI, XBOOLE_0, ENUMSET1, WELLORD2, FUNCT_2,
   XXREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_3, ORDINAL2,
   ZFMISC_1;
 registrations XBOOLE_0, FINSEQ_1, FUNCT_1, INT_1, FINSET_1,
   RELSET_1, MEMBERED, ARYTM_3;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems XBOOLE_0, TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1;
 schemes XBOOLE_0;

begin
  
reserve A for non empty set;
reserve a,n,x,y for Element of A;
reserve s for Function of A,A;
reserve f for Function of [: A,A :],A;
reserve D for (Subset of A);
reserve X,z,N,E,M,P,Q for set;
  
:: Typing lemma for s
theorem stype:
  for x holds s.x is Element of A;
  
:: Typing lemma for f
theorem ftype:
  for x,y holds f.[x,y] is Element of A
  proof
    let x,y;
    xA: x in A;
    yA: y in A;
    A1: [x,y] in [:A,A:] by ZFMISC_1:106,xA,yA;
    then A2: [:A,A:] <> {} by XBOOLE_0:def 1;
    f.[x,y] in A by FUNCT_2:7,A1,A2;
    hence thesis;
  end;
  
theorem inference42:
  (for z holds (z in M) iff z in A & (for x holds (x in N)
                              implies f.[z,x] in E))
  &
  (for n holds (n in N) implies (n in M))
  implies
  (for n holds (n in N) implies
  (for x holds (x in N) implies (f.[n,x] in E)))
  proof
    assume Mdef: (for z holds (z in M) iff
           z in A & (for x holds (x in N) implies f.[z,x] in E));
    assume NM: (for n holds (n in N) implies (n in M));
    let n such that nN: (n in N);
    let x such that xN: (x in N);
    (n in M) by nN,NM;
    hence thesis by Mdef,xN;
  end;
  
theorem inference4313:
  (for z holds (z in Q) iff z in A & f.[a,z] in E)
  &
  (for x holds (x in N) implies (x in Q))
  implies
  (for x holds (x in N) implies f.[a,x] in E)
  proof
    assume Qdef:(for z holds (z in Q) iff z in A & f.[a,z] in E);
    assume NQ: (for x holds (x in N) implies (x in Q));
    let x such that xN: x in N;
    x in Q by xN,NQ;
    hence thesis by Qdef;
  end;
  
theorem inference4326:
  (for z holds (z in P) iff z in A & f.[s.n,z] in E)
  &
  (for x holds (x in N) implies (x in P))
  implies
  (for x holds (x in N) implies f.[s.n,x] in E)
  proof
    assume Pdef: (for z holds (z in P) iff
                      z in A & f.[s.n,z] in E);
    assume NP: (for x holds (x in N) implies (x in P));
    let x such that xN: x in N;
    x in P by xN,NP;
    hence thesis by Pdef;
  end;
  
theorem inference432725:
  f.[s.n,x] in N
  &
  n in M
  &
  (for z holds (z in M) iff z in A & (for x holds (x in N)
                                       implies f.[z,x] in E))
  implies
  f.[n,f.[s.n,x]] in E
  proof
    assume fsnxN: f.[s.n,x] in N;
    assume nM: n in M;
    assume Mdef: (for z holds (z in M) iff
         z in A & (for x holds (x in N) implies f.[z,x] in E));
    ftA: f.[s.n,x] is Element of A by ftype;
    (for x holds (x in N) implies f.[n,x] in E) by Mdef,nM;
    hence thesis by fsnxN,ftA;
  end;

theorem Nindprinc:
  (for z holds z in N iff z in A &
  (for X holds (((a in X) &
  (for y holds (y in X) implies (s.y in X))) implies (z in X))))
  &
  (a in X)
  &
  (for y st (y in X) holds (s.y in X))
  implies
  (for n holds (n in N) implies (n in X))
  proof
    assume Ndef: (for z holds z in N iff z in A &
    (for X holds (((a in X) &
    (for y holds (y in X) implies (s.y in X)))
    implies (z in X))));
    assume aX: a in X;
    assume sX: (for y st (y in X) holds (s.y in X));
    let n such that nN: n in N;
    (for X holds
    (((a in X) &
    (for y holds (y in X) implies (s.y in X))) implies (n in X)))
    by nN,Ndef;
    hence thesis by aX,sX;
  end;
  
theorem BoolosCuriousInference:
  (for n holds ((f.[n,a]) = s.a)) &
  (for x holds ((f.[a,s.x]) = s.(s.(f.[a,x])))) &
  (for n,x holds f.[s.n,s.x] = f.[n,f.[s.n,x]]) &
  (a in D) &
  (for x st (x in D) holds (s.x in D))
  implies
  f.[s.(s.(s.(s.a))),s.(s.(s.(s.a)))] in D
  proof
    assume that
    H1: (for n holds ((f.[n,a]) = s.a)) and
    H2: (for x holds ((f.[a,s.x]) = s.(s.(f.[a,x])))) and
    H3: (for n,x holds f.[s.n,s.x] = f.[n,f.[s.n,x]]) and
    H4: (a in D) and
    H5: (for x st (x in D) holds (s.x in D));
  :: 1. existence of N
    defpred Np[set] means (for X holds
    (((a in X) &
      (for y holds (y in X) implies (s.y in X)))
     implies ($1 in X)));
    consider N such that
    Ndef:for z holds z in N iff z in A & Np[z]
    from XBOOLE_0:sch 1;
  :: 2. existence of E
    defpred Ep[set] means (($1 in N) & ($1 in D));
    consider E such that
    Edef:for z holds z in E iff z in A & Ep[z]
    from XBOOLE_0:sch 1;
  :: 3. Lemma 1
  :: 3.1
    LEMMA1a: (a in N)
    proof
      Np[a];
      hence thesis by Ndef;
    end;
  :: 3.2
    LEMMA1b: (for y holds (y in N) implies (s.y in N))
    proof
      let y such that yN: (y in N);
      Npy: Np[y] by Ndef,yN;
      Np[s.y]
      proof
        let X such that aX: a in X and
        sX: (for y st (y in X) holds (s.y in X));
        y in X by aX,sX,Npy;
        hence thesis by sX;
      end;
      hence thesis by Ndef;
    end;
  :: 3.3
    LEMMA1c: s.(s.(s.(s.a))) in N
    proof
      a in N by LEMMA1a;
      then s.a in N by LEMMA1b;
      then s.(s.a) in N by LEMMA1b;
      then s.(s.(s.a)) in N by LEMMA1b;
      hence thesis by LEMMA1b;
    end;
  :: 3.4
    LEMMA1d: a in E by LEMMA1a,H4,Edef;
  :: 3.5
    LEMMA1e: (for y holds (y in E) implies (s.y in E))
    proof
      let y such that yE: y in E;
      y in N by Edef,yE;
      then syN: s.y in N by LEMMA1b;
      y in D by Edef,yE;
      then s.y in D by H5;
      hence thesis by syN,Edef;
    end;
  :: 3.6
    LEMMA1f: s.a in E by LEMMA1d,LEMMA1e;
  :: 4
    LEMMA2: (for n holds (n in N) implies
             (for x holds (x in N) implies (f.[n,x] in E)))
    proof
      :: 4.1 (existence of M)
      defpred Mp[set] means (for x holds (x in N)
                              implies f.[$1,x] in E);
      consider M such that
      Mdef:(for z holds (z in M) iff z in A & Mp[z])
      from XBOOLE_0:sch 1;
      :: 4.2 Begin We want...
      wewant42: (for n holds (n in N) implies (n in M))
                           implies thesis by inference42,Mdef;
      (for n holds (n in N) implies (n in M))
      proof
        :: 4.3 Begin Enough to show...
        ets43: a in M & (for n holds (n in M) implies (s.n in M))
                                implies thesis by Nindprinc,Ndef;
        :: 4.3.1 Begin
        aM: (a in M)
        proof
          :: 4.3.1.1 Begin Want...
          want4311:(for x holds (x in N) implies f.[a,x] in E)
                                         implies thesis by Mdef;
          (for x holds (x in N) implies f.[a,x] in E)
          proof
            :: 4.3.1.2 Q exists
            defpred Qp[set] means f.[a,$1] in E;
            consider Q such that
            Qdef:(for z holds (z in Q) iff z in A & Qp[z])
            from XBOOLE_0:sch 1;
            :: 4.3.1.2 End
            :: 4.3.1.3 Begin Want...
            want4313: (for x holds (x in N) implies (x in Q))
                           implies thesis by inference4313,Qdef;
            (for x holds (x in N) implies (x in Q))
            proof
              :: 4.3.1.4 Begin Enough to show...
              ets4314: (a in Q) &
                       (for x holds (x in Q) implies (s.x in Q))
                               implies thesis by Nindprinc,Ndef;
              :: 4.3.1.4.1 Begin
              aQ: (a in Q)
              proof
                :: 4.3.1.4.1.1 Begin Want
                want431411:(f.[a,a] in E) implies thesis by Qdef;
                f.[a,a] in E by H1,LEMMA1f;
::                proof
::                :: 4.3.1.4.1.2
::                  fact431412: f.[a,a] = s.a by H1;
::                :: 4.3.1.4.1.3
::                  s.a in E by LEMMA1f;
::                  hence thesis by 
::                end;
                hence thesis by want431411;
                :: 4.3.1.4.1.1 End
              end;
              :: 4.3.1.4.1 End
              :: 4.3.1.4.2 Begin
              sQ: (for x holds (x in Q) implies (s.x in Q))
              proof
              :: 4.3.1.4.2.1
                let x such that xQ: x in Q;
              :: 4.3.1.4.2.2
                fact431422: f.[a,x] in E by xQ,Qdef;
              :: 4.3.1.4.2.3
                fact431423: f.[a,s.x] = s.(s.(f.[a,x])) by H2;
              :: 4.3.1.4.2.4 Begin "By Lemma 1 twice"
                faxA: f.[a,x] is Element of A by ftype;
                then sfaxA: s.(f.[a,x]) is Element of A by stype;
                s.(f.[a,x]) in E by fact431422,LEMMA1e,faxA;
                then s.(s.(f.[a,x])) in E by LEMMA1e,sfaxA;
                then f.[a,s.x] in E by fact431423;
              :: 4.3.1.4.2.4 End
              :: 4.3.1.4.2.5
                hence s.x in Q by Qdef;
              end;
              :: 4.3.1.4.2 End
              thus thesis by ets4314,aQ,sQ;
              :: 4.3.1.4 End
            end;
            hence thesis by want4313;
            :: 4.3.1.3 End
          end;
          hence thesis by want4311; :: 4.3.1.4.2.6 interesting
          :: 4.3.1.1 End
        end;
        :: 4.3.1 End
        :: 4.3.2 Begin
        sM: (for n holds (n in M) implies (s.n in M))
        proof
        :: 4.3.2.1
          let n such that nM: (n in M);
        :: 4.3.2.2
          (for x holds (x in N) implies f.[n,x] in E) by nM,Mdef;
        :: 4.3.2.3 Begin Want
          want4323: (s.n in M) implies thesis;
          (s.n in M)
          proof
        :: 4.3.2.4 Begin IE
            ie4324:(for x holds (x in N) implies f.[s.n,x] in E)
                                         implies thesis by Mdef;
            (for x holds (x in N) implies f.[s.n,x] in E)
            proof
            :: 4.3.2.5 P exists
              defpred Pp[set] means f.[s.n,$1] in E;
              consider P such that
              Pdef:(for z holds (z in P) iff z in A & Pp[z])
              from XBOOLE_0:sch 1;
            :: 4.3.2.5 End
            :: 4.3.2.6 Begin Want
              want4326: (for x holds (x in N) implies (x in P))
                            implies thesis by inference4326,Pdef;
              (for x holds (x in N) implies (x in P))
              proof
            :: 4.3.2.7 Begin Enough to Show...
                ets4327: (a in P) &
                      (for x holds (x in P) implies (s.x in P))
                                implies thesis by Nindprinc,Ndef;
            :: 4.3.2.7.1
                aP: (a in P)
                proof
            :: 4.3.2.7.1.1 Begin Want
                  want432711: f.[s.n,a] in E implies thesis
                  by Pdef;
                  f.[s.n,a] in E
                  proof
            :: 4.3.2.7.1.2
                    eh1: f.[s.n,a] = s.a by H1;
            :: 4.3.2.7.1.3
                    s.a in E by LEMMA1f;
                    hence thesis by eh1;
                  end;
                  hence thesis by want432711;
            :: 4.3.2.7.1.1 End
              end;
            :: 4.3.2.7.2
              sP: (for x holds (x in P) implies (s.x in P))
              proof
            :: 4.3.2.7.2.1
                let x such that xP: x in P;
            :: 4.3.2.7.2.2
                f.[s.n,x] in E by xP,Pdef;
            :: 4.3.2.7.2.3
                then fact432723: f.[s.n,x] in N by Edef;
            :: 4.3.2.7.2.4 Begin Want...
                want432724: f.[s.n,s.x] in E implies thesis
                by Pdef;
                f.[s.n,s.x] in E
                proof
            :: 4.3.2.7.2.5
                  fact432725: f.[n,f.[s.n,x]] in E
                  by fact432723,nM,inference432725,Mdef;
            :: 4.3.2.7.2.6
                  fact432726: f.[n,f.[s.n,x]] = f.[s.n,s.x]
                  by H3;
            :: 4.3.2.7.2.7
                  thus f.[s.n,s.x] in E by fact432725,fact432726;
                end;
                hence thesis by want432724;
            :: 4.3.2.7.2.4 End
              end;
              thus thesis by ets4327,aP,sP;
            :: 4.3.2.7 End
              end;
              hence thesis by want4326;
            :: 4.3.2.6 End
            end;
            hence thesis by ie4324;
        :: 4.3.2.4 End
          end;
          hence thesis by want4323;
        :: 4.3.2.3 End
        end;
        :: 4.3.2 End
        hence thesis by ets43,aM,sM;
        :: 4.3 End
      end;
      hence thesis by wewant42;
:: 4.2 End
    end;
  :: 5
    s.(s.(s.(s.a))) in N by LEMMA1c;
  :: 6
    then f.[s.(s.(s.(s.a))),s.(s.(s.(s.a)))] in E
    by LEMMA2,H1,H2,H3,H4,H5;
  :: 7
    hence thesis by Edef;
  end;