Thanks, Rob and Konrad! I will read Andrews's book and the HOL4 Description manual.
Rob, I'm guessing Andrews isn't too happy with the HOL->FOL derivation you've argued must be in his book, as he advertised it so poorly. I'll agree with you and Konrad that Tarski, Quine and Henkin are the original provers of this result, as Andrews arguably says this in the 2nd paragraph of section 1.4 in http://plato.stanford.edu/entries/type-theory-church/, which I should not have said was clearly written. Konrad, I should definitely read Description's chapter Derived Inference Rules, which seems to be doing much the same thing as I was attempting in my post. I noticed that Gordon & Melham's book is only mentioned much later and is not in your bibliography. Could that be because Gordon wrote the first first version of Description? I do not understand the second proof, on p 46, of Symmetry of equality SYM : thm -> thm. I'm including below the proof I posted, which I derived from the HOL Light code for SYM in equal.ml. The Description proof is 3 lines long and I don't understand it: 1. Γ |- t1 = t2 [Hypothesis] 2. t1 = t1 [REFL] 3. t2 = t1 [SUBST 1,2] Lines 1 & 2 are fine, but I don't see what substitution you're performing in order to conclude t2 = t1. I realized I was confused about the nature of the HOL proofs I've been posting. My new idea is that my proofs reflect a similarity between HOL and FOL that I hadn't realized: In FOL you choose axioms (such as ZFC) and then use the FOL structure (quantifiers, inference rules etc.) to both state and prove the theorems which are consequences of your axioms. Obvious differences of HOL from FOL is that we have to build the FOL we need from our much more primitive typed LC axioms (e.g. the HOL Light axioms), and we'll then replace "first" with "higher." But the similarity between FOL and HOL is in the informal mathematical proof one can give. In both cases you can define a set of the "statements", the proto-theorems. In FOL, that's I think the wffs of the language, and in HOL, there doesn't seem to be a name, but I called them the proto-sequents, the ordered pairs (Gamma, t) where Gamma is a set of terms (assumptions) of type bool, and t is a term of type bool. HOL has inference rules for deducing that a proto-sequent is actually a sequent. The is 3-line Description proof above and my longer proof below are supposed to prove the existence of SYM-type sequents. So the similarity is that in both FOL and HOL, 1) You can define a set of statements to study (wffs and proto-sequents). 2) It's a mathematical question of which of the statements have formal proofs using the axioms and inference rules (and so are are provable (theorems or sequents). 3) We can try to give informal mathematical proofs wffs/proto-sequents are actually theorems/sequents. Now with ZFC/FOL, everyone says that informal mathematical proofs are much more readable than formal ZFC proofs. So why shouldn't the same be true for HOL? Perhaps it's even true that informal mathematical proofs of the FOL rules of HOL are quite easy to understand, while understanding the formal proofs is no easier than reading the source code of our proof HOL assistants HOL Light, HOL4, ProofPower, HOL Zero. -- Best, Bill Here's my HOL->Math translation of the equal.ml code for SYM, followed by the actual code Theorem AP_TERM: For all terms f, x and y and for all sequents A |- x = y we have the sequent A |- f x = f y. Proof: By axiom REFL, we have the sequent |- f = f. Now apply axiom MK_COMB to this sequent and our assumption, noting that A ∪ ∅ = A. \qed Theorem SYM: For all terms l and r and for all sequents A |- l = r we have the sequent A |- r = l. Proof: For precision, let α be the type of l, which is also the type of r. Applying =:α->α->bool to our assumption and using theorem AP_TERM, we have the sequent A |- (= l) = (= r) By axiom REFL we have the sequent |- (l = l). Applying axiom EQ_MP to these two sequents, we have the sequent A |- (= l) l = (= r) l since A ∪ ∅ = A. We rewrite this as the sequent A |- (l = l) = (r = l). By our REFL sequent above, axiom EQ_MP and A ∪ ∅ = A, we're done. \qed 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;; I couldn't undertand this code until I looked at the on-line help: # help "AP_TERM";; ------------------------------------------------------------------- AP_TERM : term -> thm -> thm SYNOPSIS Applies a function to both sides of an equational theorem. DESCRIPTION When applied to a term f and a theorem A |- x = y, the inference rule AP_TERM returns the theorem A |- f x = f y. A |- x = y ---------------- AP_TERM `f` A |- f x = f y FAILURE CONDITIONS Fails unless the theorem is equational and the supplied term is a function whose domain type is the same as the type of both sides of the equation. EXAMPLES # NUM_ADD_CONV `2 + 2`;; val it : thm = |- 2 + 2 = 4 # AP_TERM `(+) 1` it;; val it : thm = |- 1 + 2 + 2 = 1 + 4 SEE ALSO AP_THM, MK_COMB. -------------------------------------------------------------------- val it : unit = () # help "SYM";; ------------------------------------------------------------------- SYM : thm -> thm SYNOPSIS Swaps left-hand and right-hand sides of an equation. DESCRIPTION When applied to a theorem A |- t1 = t2, the inference rule SYM returns A |- t2 = t1. A |- t1 = t2 -------------- SYM A |- t2 = t1 FAILURE CONDITIONS Fails unless the theorem is equational. EXAMPLES # NUM_REDUCE_CONV `12 * 12`;; val it : thm = |- 12 * 12 = 144 # SYM it;; val it : thm = |- 144 = 12 * 12 COMMENTS The SYM rule requires the input theorem to be a simple equation, without additional structure such as outer universal quantifiers. To reverse equality signs deeper inside theorems, you may use GSYM instead. SEE ALSO GSYM, REFL, TRANS. -------------------------------------------------------------------- val it : unit = () # ------------------------------------------------------------------------------ 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
