Thanks, Mark! I figured out the constant = myself, but it would have saved me a 
 lot of time if I checked my mail yesterday when you explained it :)  

   I should have said '@' instead of '?' here.  The constant '?' is
   actually defined in these axiomatisations (using '@').

This is true for HOL4 but not HOL Light.  In bool.ml we have the definition 

let EXISTS_DEF = new_basic_definition
 `(?) = \P:A->bool. !q. (!x. P x ==> q) ==> q`;;

p 29 of the HOL4 manual LOGIC says 

|- ∃ = λP:α→bool . P (ε P )

   Leon Henkin seems to get the credit for showing that propositional
   calculus follows from LC, actually Church's type theory in
   particular ("A theory of propositional types", Fundamenta
   Mathematicae 52:323-344, 1963
   http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52123.pdf).

Thanks, Cris! I don't yet believe that Henkin proves what I want.  Can you read 
Konrad's reference: 

BR> I'm having trouble seeing your derivation of the expected FOL-like
BR> rules in HOL Light.  Is there a paper where somebody

KS> This was done in the early days of HOL. In Chapter 22.3 of
KS> "Introduction to HOL", by Gordon and Melham, the standard rules
KS> are derived, and a fascinating business it is.

Here's some circumstantial evidence that Henkin doesn't do this.  

I couldn't print your Henkin pdf, but eventually it displayed on my screen, and 
I couldn't see anywhere in his paper where he claimed this result.  I could 
have missed it, because his notation is so old-fashioned. 

You included the first page of Andrew's followup paper, and Andrew praises 
Hankin warmly, but does not (on the 1st page at least) attribute the result I 
want to Hankin, but only the result that there is only one primitive constant.  
Is Hankin's sole primitive constant in fact =, as in HOL?  Is that what you're 
giving Hankin credit for?  I could believe that, and I see that Church's 1940 
paper has many more primitive constants, e.g. Pi, the universal quantifier, 
which in HOL is explained with =.  Are you saying that Hankin first figured 
that out? 

The claim (which you may not be making) that Hankin derived FOL from the basic 
LC axioms (e.g. the HOL axioms) seems to contradict Andrew's link
http://plato.stanford.edu/entries/type-theory-church/
which as I posted lists Prop Logic axioms in 
1.3.2 Elementary Type Theory
(1)     [pο ∨ pο] ⊃ pο
So Andrews didn't derive the proofs of statements (1--6alpha) from the standard 
LC axioms, but took them as axioms.  

-- 
Best,
Bill 

------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to