Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Sat, 13 Feb 1993 08:11:10 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07437;
          Fri, 12 Feb 93 23:58:57 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from relay.pipex.net by ted.cs.uidaho.edu (16.6/1.34) id AA07432;
          Fri, 12 Feb 93 23:58:48 -0800
X400-Received: by mta relay.pipex.net in /PRMD=pipex/ADMD=cwmail/C=GB/; Relayed;
               Sat, 13 Feb 1993 07:57:57 +0000
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2));
               Relayed; Sat, 13 Feb 1993 07:55:21 +0000
Date: Sat, 13 Feb 1993 07:55:21 +0000
X400-Originator: R.B.Jones@uk.co.icl.wins.win0109
X400-Recipients: info-hol@edu.uidaho.cs.ted
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600002263]
Original-Encoded-Information-Types: undefined (0)
X400-Content-Type: P2-1984 (2)
Content-Identifier: 2263
From: R.B.Jones@uk.co.icl.wins.win0109
Message-Id: <"2263*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: A definition of Proof Theoretic strength







         
         What I mean when I talk about the strength of logical systems is 
         what is technically known as "proof theoretic strength".
         
         Roughly this is defined:
         
              A is Proof Theoretically at least as strong as B if:
              
              (a)  A is consistent
              
              and
              
              (b)  There is an interpretation of B in A such that the 
                   interpretation of a provable formula of B is a provable 
                   formula of A, and this fact is provable in Peano 
                   Arithmetic.
         
         (My source is Beesons book "Foundations of Constructive 
         Mathematics" but I don't have the book to hand so I might not have 
         got it exactly right)
         
         This measure has absolutely no connection with the useability of a 
         specification, or even the expressiveness of one, for which I no 
         metrics.  (even the best specification language in the world has 
         no proof theoretic strength until you define a logic for it, and 
         when you define a logic it can be proof theoretically weak even if 
         the language is semantically rich)
         
         Roger Jones
         International Computers Limited
         R.B.Jones@win0109.wins.icl.co.uk