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 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.
--
Best,
Bill
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
