Russell originally wrote: | I'm looking at some of the Light source code, and curious about some | of the design decisions.
First a few general comments. In first-order logic, it's well-known how to define connectives in terms of a minimal set (e.g. ==> and F). Few of these definitions are intuitionistically valid, because most of the connectives are independent of each other in intuitionistic first-order logic (see, e.g. Prawitz's "Natural Deduction", chapter IV, corollary 9). In higher-order logic, however, one can define connectives in terms of a minimal set intuitionistically, although the definitions look a bit more obscure at first sight. Even though HOL supports classical logic, many of the definitions of connectives are done in this intuitionistic way. This may reflect the influence of some of the logicians Mike Gordon spoke to when developing the original HOL (Mike Fourman or Andy Pitts perhaps). In the case of HOL Light I was interested in seeing how far I could develop the logic before "going classical". | For example, this seems straightforward enough, given F: | | let NOT_DEF = new_basic_definition | `(~) = \p. p ==> F`;; | | ... but on the face of it, it would seem even simpler to have done | | let NOT_DEF = new_basic_definition | `(~) = \p. p <=> F`;; Indeed, that would be correct and in some ways preferable because <=>, that is equality on type "bool", is a primitive notion. The explanation is that the HOL Light foundations were arrived at in two stages via an intermediate version taking =, ==> and ! as primitive. (This was more or less when the paper "HOL Done Right" that Marco mentioned was written.) | And this one I'm also not clear about: | | let F_DEF = new_basic_definition | `F = !p:bool. p`;; | | falsehood is defined as "all propositions are true"... which is | certainly false, though on the face of it would seem a little | roundabout... does it have some particular felicitous properties, or | is it just a case of it being the simplest way to define false given | lambda and equals as primitives? This is one of these traditional intuitionistically valid definitions that has been around since the original HOL88. In that system, the primitive logical constants were equality (=, which also served as <=>), implication (==>) and the choice operator (@). The other logical connectives were defined as follows, at least in principle: F = !t. t T = (\x. x) = (\x. x) ~t = t ==> F t1 /\ t2 = !t. (t1 ==> (t2 ==> t)) ==> t t1 \/ t2 = !t. (t1 ==> t) ==> (t2 ==> t) ==> t (?) P = P ((@) P) (!) P = P = \x. T In the first step to HOL Light, my main change was to eliminate the use of the Hilbert choice operator "@" to define the existential quantifier. Otherwise I left things pretty much as they were. My definition was based on a natural infinitary generalization of the definition of disjunction (?) P = !q. (!x. P x ==> q) ==> q This definition is also standard, as it turned out. For example, Prawitz's "Natural Deduction", p67, defines a system of second-order logic with ==> and ! as primitive, and uses pretty much the same definitions for the other connectives. As for the ultimate origin, Prawitz observes in a footnote that Russell's "The Principles of Mathematics" (see chapter II, pages 16-18 in my edition) essentially has the definitions of /\ and F, at least if one assumes the equivalence of "not p" and "p implies false". Russell also remarks that the first definition "is highly artificial, and illustrates the great distinction between mathematical and philosophical definitions"! "pq (the logical product of p and q) means that if p implies that q implies r, then r is true" "not-p is equivalent to the assertion that p implies all propositions" The final step to the current HOL Light deductive system was to define conjunction and implication in terms of equality. I knew from reading Peter Andrews's book how to define all the connectives in terms of equality (I think the idea may go back to Henkin's 1963 paper "A Theory of Propositional Types", which is available online at "http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52123.pdf";). I'd not adopted such definitions because there were some parts that were not intuitionistically valid. But it eventually occurred to me that defining P /\ Q = (\f. f P Q) = (\f. f T T) P ==> Q = P /\ Q <=> P and otherwise using the existing definitions, the resulting system was quite simple and elegant and all the definitions seemed intuitionistically valid. Some time later, Konrad Slind pointed out to me that section II.2 of Lambek and Scott's "Introduction to higher-order categorical logic" has a very similar development of type theory based on equality, even including the unusual-looking HOL Light primitive rule DEDUCT_ANTISYM_RULE (their rule 2.3). Their motiviation was interpretation in toposes, and I was surprised and pleased to find that I had been led to the same result by quite different motives. John. ------------------------------------------------------------------------------ What You Don't Know About Data Connectivity CAN Hurt You This paper provides an overview of data connectivity, details its effect on application quality, and explores various alternative solutions. http://p.sf.net/sfu/progress-d2d _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
