Thanks, Lorenzo, and I'm sorry, I messed up. I understand Julien's
proof of Hilbert's axiom B3. I meant to post B4, not B3. B4 is what
Greenberg calls Hilbert's full Pasch axiom:
let B4 = new_axiom
`! l A B C. Line l /\ ~Collinear A B C /\
~(A IN l) /\ ~(B IN l) /\ ~(C IN l) /\
(? X. X IN l /\ Between A X C) ==>
(? Y. Y IN l /\ Between A Y B) \/ (? Y. Y IN l /\ Between B Y C)`;;
So if A B C are noncollinear points, and l is a line not containing A,
B or C, but l intersects the segment AC, then l must intersect either
AB or BC. That's stronger than your inner Pasch axiom or Tarski's
alternate outer Pasch axiom.
I think Julien hadn't proved B4 the last time I looked at his code.
Thanks for offering to interpret Tarski's book. My German is pretty
good, so if you email me some pages, maybe I can hack it.
I think your B3 code is not in your file 2391 line long Tarski-HOL
Light.hl you posted. I think you have no other Pasch statement except
INNER_PASCH. Maybe I don't have the latest copy of your code.
I have trouble with your code, as I understand HOL Light poorly. If
you want me to understand, you may have to explain your proofs in
math. Pointers to Narboux's proofs are also good. I tried to read
your midpoint code, and I did a lot better than I expected!
I'm puzzled at your axiom list. Here's my segment construction axiom
let A4 = new_axiom
`!a q b c. ?x. Between(q,a,x) /\ a,x === b,c`;;
and I don't see anything like that in your axiom list. Could it be
let SEGM_CONSTR_TAC a b c d x =
X_CHOOSE_THEN x STRIP_ASSUME_TAC (SPECL [a;b;c;d] SEGM_CONSTRUCTION);;
I don't understand. I also have trouble with your axiom
let CONTINUITY = new_axiom
`!X Y. (?a. !x y. x IN X /\ y IN Y ==> BB (a,x,y))
==> (?b. !x y. x IN X /\ y IN Y ==> BB (x,b,y))`;;
I believe this is Hilbert's 2nd order Dedekind cuts axiom, and not
Tarski's 1st order axiom. In practice I'm not sure it matters much
(folks used to be really fussy about FOL before HOL), and you don't
seem to ever use it, or your EUCLID axiom. I'm happy you don't use
your EUCLID axiom. I have been wondering if Hilbert's Pasch axiom
requires your EUCLID axiom. Your last theorem I think is this:
g (`!a b. ?x. MM (x,a,b)`);;
So any two points a and b have a midpoint x. That's really cool! I
include your code below. Julien hadn't proved that the last time I
looked. I can't understand your proof. I'll tell you what I think:
tarski is the type which means point. First you consider the case
when a = b, and then of course x = a. And you handle that case really
easily? I don't know what "hp1" means. It looks like you're proving
the existence of the midpoint by constructing a perpendicular. I
tried to do that and failed. I think I follow this:
let MM = new_definition
`MM (m,a,b) <=> BB (a,m,b) /\ CC (a,m) (m,b)`;;
let PER = new_definition
`PER (a,b,c) <=> ? c'. MM (b,c,c') /\ CC (a,c) (a,c')`;;
let PERP_IN = new_definition
`PERP_IN (x,a,b,c,d) <=>
~ (a=b:tarski) /\ ~ (c=d:tarski) /\ COLL (x,a,b) /\ COLL (x,c,d) /\
(! u:tarski v:tarski. (COLL (u,a,b) /\ COLL (v,c,d) ==> PER (u,x,v)))`;;
let PERP = new_definition
` PERP (a,b,c,d) <=> ?x. PERP_IN (x,a,b,c,d)`;;
So MM (m,a,b) means m is the midpoint of a and b.
PER (a,b,c) means ab and bc are perpendicular, as
b is the midpoint of c & c', so c' is obtained by applying segment
construction to push c past b with bc = bc'. Now c and c' are
equidistant from a.
BTW I recommend writing comment lines to explain your code!
Then PERP_IN (x,a,b,c,d) means a & b are distinct, c & d are distinct,
x is in the intersection of the lines ab and cd. Now unless a, b, c &
d are collinear (your assumptions don't say they can't be), then x is
the only intersection of the lines ab and cd, by Hilbert's axiom I1,
which I proved and you must too (I'm including my proof below). So
let's assume that x is the only intersection point of the lines ab and
cd. Then you say that if u is on line ab, and v is on line cd, then
xu and xv are perpendicular.
Then PERP (a,b,c,d) means that lines ab and cd intersect at some point
x and then (basically) lines ab and cd are perpendicular.
OK, back to your code, on the "hp1" line. You're asserting that there
is a point q so that lines ab and qb are perpendicular? I think I did
not know how to prove that. My memory is a bit rusty. Let me try to
remember. Your UPPER_DIM axiom says that the points which are
equidistant from two distinct points u and v form a line, at least
they're all collinear. So if we use segment construction to push a
past b on line ab to get a point a', with b the midpoint of a and a',
then we can look at the points equidistant from a and a'. Well, b is
such a point, but how do we know there are any other such points, say
q? I'm pretty sure I never knew how to prove that. So good work!
--
Best,
Bill
Lorenzo's proof of the existence of midpoints.
let MM_EXISTENCE_AUX = top_thm ();;
g (`!a b. ?x. MM (x,a,b)`);;
e (INTRO_TAC "!a b");;
e (ASM_CASES_TAC `a=b:tarski`);;
e (TREAT_EQ_TAC);;
e (MESON_TAC [MM_TRIVIAL]);;
e (ASSERT_TAC "hp1" `?q. PERP (a,b,q,b)`);;
e (PERP_ASM_MESON_TAC [l8_21]);;
e (POP_ASSUM (X_CHOOSE_TAC `q:tarski`));;
e (ASSERT_TAC "hp2" `?p t. PERP (a,b,p,a) /\ COLL (a,b,t) /\ BB (q,t,p)`);;
e (APPLY_TAC l8_21);;
e (ASM_MESON_TAC []);;
e (POP_ASSUM (X_CHOOSE_TAC `p:tarski`));;
e (POP_ASSUM (X_CHOOSE_TAC `t:tarski`));;
e (ASSERT_TAC "hp3" `le (a,p)(b,q) \/ le (b,q)(a,p)`);;
e (APPLY_TAC le_CASES);;
e (ASM_CASES_TAC `le (a,p) (b,q)`);;
e (APPLY_TAC MM_EXISTENCE_AUX);;
e (ASM_MESON_TAC []);;
e (ASSERT_TAC "hp4" `?x. MM (x,b,a)`);;
e (APPLY_TAC MM_EXISTENCE_AUX);;
e (PERP_ASM_MESON_TAC [COLL_PERM4;BB_SYM]);;
e (MM_ASM_MESON_TAC []);;
let MM_EXISTENCE=top_thm();;
My miz3 proof of Hilbert's axiom I1, from
http://www.math.northwestern.edu/~richter/TarskiAxiomGeometry.ml
let I1_THM = thm `;
let a b x y be point;
assume ~(a = b) [H1];
assume ~(x = y) [H2];
assume a on_line x,y [H3];
assume b on_line x,y [H4];
thus x,y equal_line a,b
proof
cases;
suppose (x = b) [H5];
~(b = y) [P1] by -, H2;
b,a equal_line a,b [P2] by H1, LineEqA1_THM;
x,y equal_line b,y [P3] by H2, H5, LineEqRefl_THM;
a on_line b,y by H3, H5;
b,y equal_line b,a by -, P1, H1, I1part2_THM;
x,y equal_line b,a by -, H1, H2, P1, P3, LineEqTrans_THM;
qed by -, H1, H2, P2, LineEqTrans_THM;
suppose
~(x = b) [H6];
x,y equal_line x,b [P4] by -, H2, H6, H4, I1part2_THM;
a on_line x,b by -, H2, H6, H3, onlineEq_THM;
x,b equal_line a,b by -, H6, H1, I1part2Reverse_THM;
qed by H1, H2, H6, P4, -, LineEqTrans_THM;
end`;;
------------------------------------------------------------------------------
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
