> 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?
The HOL4 Description and Logic manuals are essentially taken from the
Gordon&Melham book, and further adapted
as the HOL system has evolved since 1988.
> 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.
SUBST is a complex primitive, which John Harrison did away with in HOL
Light. SUBST essentially allows controlled replacement of an equality. What
I believe line 3 says is
replace some number of occurrences of the lhs of the theorem of line 1
in the theorem of line 2
> 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:
There is very little difference between FOL and HOL: the major data
structures are as follows.
FOL: term --> formula --> sequent --> theorem
HOL: type ---> term ------------------> sequent --> theorem
In HOL, the use of types lets terms of type bool serve as formulas. At the
level of proofs,
every FOL inference has a corresponding HOL inference, plus HOL needs rules
allowing
instantiation of type variables and some lambda calculus stuff like alpha,
beta, and eta conversion.
Konrad.
On Tue, Mar 25, 2014 at 2:27 AM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> 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 S!
> YM-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
