Thanks, John! You made a great Equiv improvement. I'm still really
confused about HOL Light types, and I would appreciate more guidance.
I think that everything I want to do with sets ought be easily doable
in HOL Light with types explaining the mathematical structures. I'm
reading the tutorial and reference manual and at least understand your
new_constant("===",`:point#point->point#point->bool`);;
which says that point#point is the type of ordered pairs (x, y) where
x and y have type point.
Yes, I like this approach. I would certainly very much support your
idea in another message of formalizing the whole paper, though of
course it would represent a lot of work.
Excellent! It's not as much work as you'd think, maybe, as reading my
own proofs (which are more details than I'm I'm used to) might be
easier than coding the proofs is HOL-Light/miz3. I'm glad you like my
set theory approach: point IN line SUBSET space. I just don't quite
know how to pull it off yet.
My own instinct would be be something like (1).
You're the boss, so we'll do it your way. The only objection to (1)
is that you have to redo everything if you start with just plane
geometry. But that's not an issue until I code up the plane geometry!
Then the 2-dimensional theorems would have some ambient plane P at
the beginning:
!P:point->bool. plane P ==> !x y. x IN P /\ Y IN P ==> ...
Great! A technical question:
You defined the type `point' here:
new_type("point",0);;
Can't we define the types `line' and `plane' to both be
point->bool
and then write
!P:plane. !x y. x IN P /\ Y IN P ==> ...
You would effectively relativize all quantifiers to this plane P
and then just assume in the first hypothesis that it is a plane.
Got it!
And for axioms or theorems that are true in higher dimensions, you
might as well omit the "plane" hypothesis.
Ah, but that's not the way Hilbert's axioms work. I'm still
absolutely amazed that Hilbert only needed 3 incidence axioms like
``If two distinct planes intersect, their intersection is a line.''
to handle 3-dim geometry on top of your relativized to any plane P
2-dim axioms.
The reason this works nicely is precisely that you do model most
other concepts as sets of points with certain properties instead of
some other unanalyzed category.
Great!
it might be a useful basis for analyzing, for example, just what
set-theoretic properties you actually end up using and hence
clarify the relationship with the other way of formalizing it using
unanalyzed concepts for "line" etc. instead of considering them as
subsets of points.
Here I don't quite follow you. I think the set theory approach is
just MUCH simpler than the `unanalyzed concepts' approach, but we
could with work turn all the set theory into `unanalyzed concepts'.
Here's the first Lemma in my paper.
Given two distinct lines l and m, if X IN l INTERS m, then l INTERS m = {X}.
We can state that axiomatically like this:
! l m be line . ! X be point . ~(l = m) /\ X /\ X on_line l /\ X on_line l
===> (! Y be point . Y on_line l /\ Y on_line l ==> Y = X)
I think the set theory version in my paper is much more readable.
It's just the usual difference between syntactic proofs and proofs in
a model. So I'm giving semantic proofs in any model of the Hilbert
axioms, and so by some math logic result that means there must be a
syntactic FOL proof, even though I used set theory in my model. In my
case, I don't think the translation from sets to `unanalyzed concepts'
is that hard, it just destroys readability.
And why would anyone want to do pure syntactic proofs with `unanalyzed
concepts' now that HOL Light handles sets so nicely? I assume the set
theory capability has a lot do with how HOL differs from FOL.
--
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
