Thanks, Rob! You're right, I hadn't looked at Section 1.4 "A Formulation Based on Equality" of Andrew's link > http://plato.stanford.edu/entries/type-theory-church/ and more to the point, > I didn't read the longer version Andrew's wrote in his book To Truth Through > Proof: More details about Q0 can be found in Andrews 2002. So you're right, that's not a fair reading of mine.
But I don't see anywhere in Andrews's very readable Section 1.4 where he says that we can recover all the FOL we need from some simple typed LC axioms, why he's not going to need the 6 axioms he listed in section 1.3.2 Elementary Type Theory. Can you get to the bottom of this? Obviously you know how to deduce FOL from something like the HOL Light axioms, because you needed to to write your proof assistant ProofPower. So where did you learn it? From Konrad's book Gordon and Melham? From Andrews's book? -- 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
