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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
