Re: little theories and encryption

• Mail folder: QED
• Next message: David McAllester: "Why should a mathematician be interested in QED?"
• Previous message: jt@linus.mitre.org: "bourbaki"
• In-reply-to: Lawrence C Paulson: "little theories and encryption"

To: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Cc: qed@mcs.anl.gov
Subject: Re: little theories and encryption
In-reply-to: Your message of Mon, 19 Apr 93 17:57:03 +0100. <"swan.cl.ca.644:19.04.93.16.57.14"@cl.cam.ac.uk>
Date: Thu, 22 Apr 93 02:48:05 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-id: <"swan.cl.cam.:133330:930422014815"@cl.cam.ac.uk>
Sender: qed-owner
Precedence: bulk

Larry Paulson writes:

  [...] Perhaps 'little theories' could prevent this; each theorem would
  be proved in the weakest framework possible for that particular
  theorem.

I agree this is a very desirable goal. But finding such a framework is
of course a highly nontrivial creative process (unless you include
P |- P that is).

I would imagine that almost all algebraic structures arose from an
attempt to generalize existing proofs and identify precisely which
assumptions they rest on.

Which general structures are worth defining is something people will
disagree over (witness Javier's comments on uniform spaces).

Furthermore, given two proofs of a theorem from widely differing
assumptions, do we have any a priori reasons to expect there to be an
appropriate elegant and nontrivial abstraction (by this I mean to exclude
the conclusion itself or the disjunction of the two assumptions) that
unifies them?

Indeed, might not a proof from one set of assumptions be used as
a lemma in the proof from another set? (Perhaps in an apparently
"essential" way.) For example, Gauss' proof that if a ring R is a
unique factorization domain then so is its polynomial ring R[x] uses as
a lemma the fact that the ring of polynomials over a field is a UFD.

John Harrison (jrh@cl.cam.ac.uk)