Hi Bill,
| 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.
It is possible to express certain properties with types rather than
explicit set constraints, and this can indeed make things a lot
smoother and more convenient. On the other hand, HOL types are quite
restricted (compared, for example, to richer type theories like Coq's)
while set constraints are more general and flexible. Also, there is
no concept of one type being a "subtype" of another: different types
are considered disjoint and need explicit mappings between them, which
makes it more convenient to use sets where you want such subset
relationships. In general, it can be a difficult trade-off deciding
whether to use types or set constraints in a given situation.
| 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 ==> ...
If you literally define "plane" as a synonym of "point->bool" (which
can be done with "new_type_abbrev") then this would typecheck but
wouldn't adequately express the fact that you want plane to be a
member of "point->bool" with specific properties, not any member. On
the other hand, if you define a type ":plane" taking into account
those constraints, then you wouldn't be able to treat it as a set and
use IN directly, because of the disjointness issue I mentioned above.
This is why I think set constraints may work better, even at the cost
of slightly more involved statements. More experimentation may be
needed.
| 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.
Yes, that does seem surprising. OK then, I guess you should just
keep the planarity hypotheses there anyway.
| 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'.
I agree that it seems much simpler, and thinking of lines and planes
as sets of points certainly corresponds to my intuition. Though I
wonder if this is just because of the ubiquity of the set concept
in modern mathematics. Would, say, an 18th-century mathematician have
taken the same view?
| 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.
Perhaps because using sets might be felt to make things less clear
from a foundational perspective, since on the face of it you are also
using some set-theoretic properties in addition to the explicit
axioms. Now, in fact, I think it is clear that such uses are in some
sense inessential and eliminable. My point was that having a corpus of
totally explicit formal proofs might be a good starting-point for
making that belief more rigorous.
John.
------------------------------------------------------------------------------
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
