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