Thanks, Rob! I don't Andrew's book to hand either, but his on-line article is causing me real trouble: http://plato.stanford.edu/entries/type-theory-church/
1.3.2 Elementary Type Theory We start by listing the axioms for what we shall call elementary type theory. (1) [pο ∨ pο] ⊃ pο (2) pο ⊃ [pο ∨ qο] (3) [pο ∨ qο] ⊃ [qο ∨ pο] (4) [pο ⊃ qο] ⊃ [[rο ∨ pο] ⊃ [rο ∨ qο] ] (5α) Πο(οα) f(οα) ⊃ f(οα) xα (6α) ∀xα[pο ∨ f(οα)xα] ⊃ [pο ∨ Πο(οα) f(οα)] The theorems of elementary type theory are those theorems which can be derived from Axioms 1–6α (for all type symbols α). We shall sometimes refer to elementary type theory as T . It embodies the logic of propositional connectives, quantifiers, and λ-conversion in the context of type theory. But in HOL, I think these Prop Logic results are theorems and not axioms. My feeling is that Andrews's book is great because it clearly establishes the fact that HOL (which Andrews says is a synonym for Church's type theory) is "the same" as Church's work which is "almost the same" as Russell-Whitehead. This is an important point relating to the homotopy type theory that Vladimir Voevodsky is doing. I don't feel that Andrews's book is readable enough to be satisfactory documentation. The primitive rules and axioms in HOL4 (and ProofPower) are different from HOL Light, but prove the same set of theorems. Thanks. Could you respond to my last disjointed post about the HOL meaning of typed Lambda calculus? That (perhaps) Church's typed LC allows us to elegantly deduce all the FOL we need (such as Andrews's axioms above) from some simple LC 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
