Bill,
On 23 Mar 2014, at 18:44, Bill Richter <rich...@math.northwestern.edu> wrote: > > 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. I don't think you are giving Andrews' article a fair reading. Section 1.4 presents an alternative formulation of simple type theory based only on equality (which Andrews attributes to Tarski). Regards, Rob. ------------------------------------------------------------------------------ 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
