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; Thu, 18 Feb 1993 19:03:36 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA27212;
          Thu, 18 Feb 93 10:48:34 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Ucthpx.UCT.AC.ZA by ted.cs.uidaho.edu (16.6/1.34) id AA27207;
          Thu, 18 Feb 93 10:48:24 -0800
Received: by ucthpx.uct.ac.za (/\==/\ Smail3.1.24.1 #24.2) id m0nPGIO-000NyqC;
          Thu, 18 Feb 93 20:48 SAST
Received: by elc.mth.uct.ac.za (4.1/SMI-4.1) id AA10379;
          Thu, 18 Feb 93 20:46:50+020
From: gavan@za.ac.uct.mth.elc (Gavan Tredoux)
Message-Id: <9302181846.AA10379@elc.mth.uct.ac.za>
Subject: Completeness proofs
To: info-hol@edu.uidaho.cs.ted (Info-hol mailing list)
Date: Thu, 18 Feb 93 20:46:49 EET
X-Mailer: ELM [version 2.3 PL11]

It struck me recently that nobody seems to have
constructed any *completeness* proofs in HOL, of
an embedded logics. Generally, metatheory has
taken a back place to the practical issues surrounding 
the use of HOL in applied contexts -- where it is
important to derive logics and then USE them rather than
reason ABOUT them.

Mounting a completeness proof would obviously involve 
formalizing the notion of proof. It would be interesting
to formalize proof in the *sequent* style employed
by HOL, within HOL itself. One way to do this is
to use recursive type definitions to provide the *form*
of proofs, equipped with a `meaning' function to 
deliver the proof in HOL itself (associate an abstract
`rule' with a rule in the HOL logic itself).

It might be interesting to throw this idea around a little,
if someone else is game.

Gavan Tredoux
FACCS Lab, Dept. Math
UCT