Thanks, Konrad! I'll read your proof of NOT_FORALL_THM, and try to find Gordon and Melham's book. Two points:
I don't believe that Church ever explained how typed LC implies FOL. Church certainly does not explain this in his paper A Formulation of the Simple Theory of Types http://www.jstor.org/stable/2266170. In section 4 "Formal axioms", he lists exactly the FOL axioms that his student Peter Andrews lists http://plato.stanford.edu/entries/type-theory-church/ So maybe Gordon and Melham were the first people to figure out how to deduce FOL from typed LC and some simple LC axioms like the HOL Light axioms Tom Hale cites: http://www.ams.org/notices/200811/tx081101370p.pdf I've understood something pretty simple from hol_light/equal.ml, a proof (translated from SYM of equal.ml) that equality is symmetric, using Hale's axioms 1) Equality is reflexive; 3) Equal functions applied to equals are equal; 7) An ``equality-based'' rule of modus ponens holds. My written proof just amounts to understanding the actually quite nice code in equal.ml: let AP_TERM tm th = try MK_COMB(REFL tm,th) with Failure _ -> failwith "AP_TERM";; let SYM th = let tm = concl th in let l,r = dest_eq tm in let lth = REFL l in EQ_MP (MK_COMB(AP_TERM (rator (rator tm)) th,lth)) lth;; First a simple point involving infixes and currying. Take a term l. Note that (= l) x means l = x, by definition of infix, and that (= l) is the function λx. l = x if we choose a variable x which is not free in l. But by using (= l), equal.ml both avoids choosing such a free variable x, simplify the use of axiom 3 above, and means we don't have to understand how full beta-conversion version of Hales's axiom 5) The application of the function x |-> a to x gives a. How clever! Next we'll need the theorem implicit in AP_TERM obtained by combining axioms 1 and 3: applying the same function to an equation gives an equation. That is, if Gamma |- x = y, then Gamma |- f x = f y. Theorem: Take two terms l and r with Gamma |- l = r. Then Gamma |- r = l. Proof: We can suppress assumptions Gamma in the proof, because axiom 1 requires no assumptions, and axioms 3 and 7 take the union of the assumptions. Axiom 1 gives the equation l = l which we'll use twice below. l and r must have type A, and = has type A->(A->bool). So applying = to the equation l = r gives the equation (= l) = (= r), by the AP_TERM theorem. Axiom 3 applied to this function equation and l = l gives the equation ((= l) l) = ((= r) l) i.e. (l = l) = (r = l). Thus we have the equation r = l by Axiom 7, since l = l. \qed Now I'm ready to try harder things, like Rob's beta-conversion or your NOT_FORALL_THM. -- 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
