On Wed, Aug 22, 2012 at 4:39 AM, Bill Richter <[email protected]
> wrote:
> John, I'm still excited by your SET_RULE, but I ran into a problem that
> maybe is a serious miz3/set problem, unlike miz3's incomplete ability to
> prove abstractions and sets were equal. I distilled my problem down to
> this example, where the first three results are fine, but the last
> (DoubletonPlusSymmetry) gets a #1 inference error:
>
> #load "unix.cma";;
> loadt "miz3/miz3.ml";;
> horizon := 0;;
> timeout := 50;;
>
> SET_RULE `X = Y ==> {a, b} UNION X = {b, a} UNION Y `;;
>
> let DoubletonSymmetry_THM = thm `;
> let a b be A;
> thus {a, b} = {b, a}
> by SET_RULE`;;
>
> let DoubletonXSymmetry_THM = thm `;
> let a b be A;
> let X be A->bool;
> thus {a, b} UNION X = {b, a} UNION X
> by SET_RULE`;;
>
> let DoubletonPlusSymmetry_THM = thm `;
> let a b be A;
> let X Y be A->bool;
> assume X = Y;
> thus {a, b} UNION X = {b, a} UNION Y
> by SET_RULE`;;
>
I don't know anything about SET_RULE, but does it pay attention to your
assumptions ("assume X=Y")?
That's the main difference between this proof that fails and what looks
equivalent (line starting "SET_RULE") above.
>
> I can't see any mistake I'm making. Maybe I should say how this actually
> came up. I have defs & thms
> let Segment_DEF = new_definition
> `seg A B = {A, B} union open (A,B)`;;
> IntervalSymmetry_THM |- ∀ A B. open (A,B) = open (B,A)
> DoubletonSymmetry_THM |- ∀ A B. {A, B} = {B, A}
> SegmentSymmetry_THM |- ∀ A B. seg A B = seg B A
>
> and the proof of the last is
> let SegmentSymmetry_THM = thm `;
> let A B be point;
> thus seg A B = seg B A
> by Segment_DEF, IntervalSymmetry_THM, DoubletonSymmetry_THM`;;
>
> and I thought I should be able to replace DoubletonSymmetry_THM by
> SET_RULE, and it did not work:
> let SegmentSymmetry_THM = thm `;
> let A B be point;
> thus seg A B = seg B A
> by Segment_DEF, IntervalSymmetry_THM, SET_RULE`;;
>
> I get a #1 inference error. I know you're real busy right now, and I
> can't argue this is high priority, but I think it would be nice for miz3 to
> have a good set-theory prover to go along with its good FOL prover MESON.
> I don't know exactly what this set-theory prover ought to prove, but I
> figure it should prove result analogous to what MESON already proves.
>
> My request that you install SET_RULE in miz3 was illogical, as later in my
> post I said I didn't want to use SET_RULE because it was as hard as
> IN_ELIM_THM. But heck, I was really excited to see SET_RULE give a
> stunning 1-line proof to replace my long and boring proof
>
> let DoubletonSymmetry_THM = thm `;
> let x y be A;
> thus {x, y} = {y, x}
>
> proof
> {x, y} = x INSERT {y} /\ {y, x} = y INSERT {x} [defDoubleton];
> ! P. P IN {x, y} <=> P = x \/ P = y [defxy] by defDoubleton,
> IN_INSERT, IN_SING;
> ! P. P IN {y, x} <=> P = x \/ P = y by defDoubleton, IN_INSERT,
> IN_SING;
> qed by -, defxy, EXTENSION`;;
>
> Eventually I want to discuss HOL with you, as your HOL Light documentation
> explains very little about it. Michael, Konrad, Rob, Ramana, Mark and Cris
> helped me a lot, but I have reading to do. Let me summarize:
>
> Tom Hales in his Notices article shows that he really understand HOL, but
> he doesn't explain it to novices. I'm trying to read Michael & Konrad HOL4
> Logic manual, which they assure me holds for HOL Light as well. Rob had a
> great slogan, that HOL would be better named "polymorphic typed set theory."
>
> Michael assured me that my first line of code, due to you (thanks again!)
> new_type("point",0);;
> means that `point' is the name of a set which right now we know nothing
> about it, but the axioms, also largely due to you (thanks again!), describe
> more and more precisely. So the set `point' is what's often called a
> Hilbert plane. Furthermore, Michael agreed, my next lines
> new_type_abbrev("point_set",`:point->bool`);;
> new_constant("Line",`:point_set->bool`);;
> means there is a function Line: P(point) ---> bool which is supposed to
> tell if a subset of our Hilbert plane `point' is actually a line. Again,
> the axioms describe (or constrain) the function Line.
>
> I think there's a lot of mutual distrust between the fields of Math and
> CS, and I'm hoping to help improve matters, but I'm maybe as bad as anyone,
> as I had sneered at the whole idea of HOL, thinking it's obvious they're
> just doing ZFC, why can't they explain this clearly. I'm now quite
> embarrassed by my old attitude, as it seems that HOL grows out of
> Russell-Whitehead's initial foundationalizing of math, and profited from
> Church's improvements in typed LC. I had no idea anything like this was
> going on, and I think I'm expert in LC! Math Logic (which I think is quite
> close to CS) isn't taken seriously in Math depts, but I've been exposed to
> Math Logic, but head nothing about Russell-Whitehead or Church math
> foundations.
>
I would love to see some of the sentiments of the paragraph above appear in
something you eventually publish about your experiences with HOL.
I can confirm that in my limited experience, mathematicians who are not
also computer scientists aren't interested in mathematical logic or
foundations.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
