Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: chou@edu.ucla.cs, info-hol@edu.uidaho.cs.ted
In-Reply-To: chou@cs.ucla.edu's message of Fri, 9 Apr 1993 10:27:12 +0200 <9304090827.AA22336@maui.cs.ucla.edu>
Subject: A few Q's
Message-Id: <93Apr9.173439met_dst.8067@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 9 Apr 1993 17:34:38 +0200


Ching Tsun writes

> (1) Who was the first person who used a general logical formalism
>    (eg, HOL) to embed a specialized logic (eg, temporal logic or
>    Hoare logic)?  

I think Godel's undecidability-of-arithmetic result marked the first
time the meta/object language distinction was drawn and exploited. As
for embeddings in computer implementations of logic I dunno - Shankar's
thesis on metamathematics in the Boyer-Moore system? (I doubt that the
embedded logic was used to do inference though.)

If one is looking for work on giving semantics to "weak" formalisms by
defining them in "strong" formalisms and then deriving inference rules
for the weak formalism by operations in the strong formalism, the
simplest example (and thus maybe the earliest historically, no guarantee
though) might be to examine the addition of equality to first order
logic. For example, section 26 in Andrews' book gives such a
development.

If one is looking for embedding of "weak" formalisms in computer logic
implementations, some of the early Cambridge HVG theses might help. I
think Jeff Joyce did some modal logic in his thesis, but I haven't read
it.


> (2) Is there any embedding work using other general logical formalisms
>    such as ZFC or Nuprl?  

Sure, everybody and their dog does it: Isabelle, Coq, lambdaProlog, Elf,
Lego, .... 

A reference for embedding in Nuprl is "Nuprl as a general logic",
Constable and Howe, in the book edited by Oddifreddi "Logic and Computer
Science".

> (By the way, is there a good theorem prover for ZFC?)

As far as good theorem provers for set theory, I heard that the EVES
system from ORA Ottawa had adopted a set theory, not sure what flavour
though. 


> (3) What is your view about general versus specialized logics?
>    For the former, I can see several advantages: higher security
>    (if the base logic can be trusted and only definitional extensions
>    are used), flexibility of mixing specialized reasoning with
>    general mathematical reasoning, and no need to worry about the
>    completeness of axioms and rules since new ones can always be
>    proved and added when necessary.  

In the "Little Theories" paper from the last CADE conference, Guttman et
al. discuss these issues, although with a slightly different slant.

> What are the latter's [specialized logics] advantages?

    1. Pure unbridled speed (see message a few months ago of Paul
       Loewenstein on BDDS). 
    2. The ability to use admissible but not derivable rules of inference.

Konrad.