[FOM] strange phenomenon

[Robin Adams]

On Tue, 7 Jan 2003, Neil Tennant wrote:

> Hence my challenge: can anyone construct a completely detailed formal
> proof of Cantor's Theorem, in natural deduction, with every step
> primitive, to which neither of these two proposed reductions is
> applicable?

I very much doubt there is one.  I can show that there is no normalised
proof in Higher Order Logic.

As a warm-up, what goes wrong when normalising the usual proof?  When
deriving a contradiction from the assumption of a bijection F between A
and PA, we can produce as usual a term t such that
        t in F(t) <-> ~(t in F(t))
However, there is no normalised derivation of # from P <-> ~P; in fact,
there is no normalised derivation of Q from P -> P -> Q and (P -> Q) -> P.

For, any such proof must end with two applications of (-> E) to P -> P ->
Q:

                 (?1)
P -> P -> Q        P
--------------------        (?2)
         P -> Q              P
         ---------------------
                    Q

(?1) must end with an application of (-> E) to (P -> Q) -> P:

                                  (?3)
             (P -> Q) -> P       P -> Q
             --------------------------
P -> P -> Q                 P
-----------------------------                    (?2)
            P -> Q                                P
            ---------------------------------------
                                 Q

But the first of our new rules of reduction can be applied to any such
derivation.

Here is the only derivation of Q from P -> P -> Q and (P -> Q) -> P to
which cut elimination cannot be applied:

                P -> P -> Q        [P](1)
                ----------------------
                        P -> Q          [P](1)    P -> P -> Q  [P](2)
                        -------------------       ----------------
                                 Q                      P -> Q     [P](2)
                              --------(1)               --------------
           (P -> Q) -> P       P -> Q                          Q
           --------------------------                        ------(2)
P -> P -> Q              P                 (P -> Q) -> P     P -> Q
--------------------------                 ------------------------
              P -> Q                                  P
             ---------------------------------------------------
                                       Q

Call this derivation (A).  Applying the first new reduction to this
derivation yields:

                                           P->P->Q [P](2)
                                           -----------
          P->P->Q      [P](1)                  P->Q    [P](2)
          ----------------                     -----------
                 P -> Q     [P](1)                 Q
                 --------------                  ------(2)
                        Q            (P->Q)->P    P->Q
                     ------(1)       -----------------
                     P -> Q              P
                     ---------------------
                                 Q

Call this (B).  Applying cut elimination to (B) yields derivation (A)
again!  Thus, in this case, our first new reduction and cut elimination
are inverses of one another.

A similar analysis shows that there can be no normalised proof of Cantor's
Theorem in HOL; in fact, there can be no derivation of # from the
assumption that F : A -> PA is surjective:

              (A X : PA) (E a : A) (A x : A) (Xx <-> Fax)

For any such derivation would have to have the form:

 (AX:PA)(Ea:A)(Ax:A)(Xx<->Fax)    [(Ax:A)(phi(x)<->Fax)]
 -----------------------------        (D1)
   (Ea:A)(Ax:A)(phi[x,F]<->Fax)        #
   --------------------------------------
                    #

for some formula phi[x,F] with free variables x:A and F:A -> PA.  As
the only term of type A we have is a, (D1) must be of the form

                           (Ax:A)(phi[x,F] <-> Fax)
                           ------------------------           (D3)
(Ax:A)(phi[x,F] <-> Fax)          phi[a,F] <-> Faa           phi(a)
----------------------          -----------------------------------
     phi[a,F] <-> Faa                Faa
     ------------------------------------
                    phi[a,F]
                      (D2)
                       #

and so the first new rule of deduction can be applied to it.

I am sure a similar analysis could be made to show there is no normalised
first-order proof of Cantor's Theorem from the axioms of some set theory.

I hope all the above helps.  In particular, I think
(P -> P -> Q) -> ((P -> Q) -> P) -> Q may be a simpler and more useful
example to study than Cantor's Theorem to see why the first new rule of
reduction is problematic.