Yes Section 7 in HOL Done Right discusses the rationale behind the changes in HOL Light, which helps. But still, it would be nice to see coverage of all of the "traditional" HOL definitions. I now notice that this section says that the definitions are precisely those of Prawitz, 1965. But it would be nice if there were a freely-available HOL document that explicitly explains these definitions. Is there not something like this for HOL4? A quick trawl through the documentation suggests not..
I was thinking about the original question, regarding the definitions of falsity and logical negation. I suppose that `!(p:bool). p` holding means the logic is inconsistent (simply by definition of inconsistency), so the definition of falsity is saying that `false` holding is the same as inconsistency in the system. Mark. On Fri, 25 Feb 2011 15:24:30 +0000, Russell Wallace <[email protected]> wrote: > Ah, that's a lot of what I was looking for, thanks! > > On Fri, Feb 25, 2011 at 1:26 PM, <[email protected]> wrote: >> Some implementation choices behind the design of HOL Light are >> discussed >> in this paper: >> >> John Harrison "HOL Done Right" >> http://www.cl.cam.ac.uk/~jrh13/papers/holright.html >> >> See e.g. section 7 where it is discussed in details the definition >> of >> the >> existential quantification. >> >> Marco >> >> >> Quoting Mark <[email protected]>: >> >>> I think you ask an interesting question, and I would also like to >>> know >>> the answer. It seems that these definitions have been handed down, >>> but >>> it's difficult to find the original reasons why they were done the >>> way >>> they were. Or maybe there's some crucial document I don't know >>> about.. >>> >>> Interestingly, HOL Light deviates from the other HOL systems for >>> the >>> definitions for some constants (e.g. conjunction, implication and >>> existential quantification), enabling a smaller logical core. In >>> HOL >>> Zero, I just stuck with the conventional definitions of HOL88, >>> HOL90, >>> ProofPower HOL, HOL4, etc. I did, however, attempt to give >>> informal >>> English explanations of the logical core's definitions and axioms >>> in >>> source code comments, but this didn't stretch to falsity and >>> logical >>> negation (but I would like it to!). >>> >>> Mark. >>> >>> On Wed, 23 Feb 2011 13:40:54 +0000, Russell Wallace >>> <[email protected]> wrote: >>>> Hi all, >>>> >>>> I'm looking at some of the Light source code, and curious about >>>> some >>>> of the design decisions. >>>> >>>> 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`;; >>>> >>>> Is there a reason implication was chosen over equality for this >>>> definition? >>>> >>>> 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? >>>> >>>> Is there any documentation anywhere on the reasoning behind these >>>> decisions? >>>> >>>> >>>> >>>> ------------------------------------------------------------------------------ >>>> Free Software Download: Index, Search & Analyze Logs and other IT >>>> data in >>>> Real-Time with Splunk. Collect, index and harness all the fast >>>> moving >>>> IT data >>>> generated by your applications, servers and devices whether >>>> physical, >>>> virtual >>>> or in the cloud. Deliver compliance at lower cost and gain new >>>> business >>>> insights. http://p.sf.net/sfu/splunk-dev2dev >>>> _______________________________________________ >>>> hol-info mailing list >>>> [email protected] >>>> https://lists.sourceforge.net/lists/listinfo/hol-info >>> >>> >>> >>> ------------------------------------------------------------------------------ >>> Free Software Download: Index, Search & Analyze Logs and other IT >>> data in >>> Real-Time with Splunk. Collect, index and harness all the fast >>> moving IT data >>> generated by your applications, servers and devices whether >>> physical, virtual >>> or in the cloud. Deliver compliance at lower cost and gain new >>> business >>> insights. http://p.sf.net/sfu/splunk-dev2dev >>> _______________________________________________ >>> hol-info mailing list >>> [email protected] >>> https://lists.sourceforge.net/lists/listinfo/hol-info >>> >> >> >> >> >> ------------------------------------------------------------------------------ >> Free Software Download: Index, Search & Analyze Logs and other IT >> data in >> Real-Time with Splunk. Collect, index and harness all the fast >> moving IT data >> generated by your applications, servers and devices whether >> physical, virtual >> or in the cloud. Deliver compliance at lower cost and gain new >> business >> insights. http://p.sf.net/sfu/splunk-dev2dev >> _______________________________________________ >> hol-info mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info >> > > > ------------------------------------------------------------------------------ > Free Software Download: Index, Search & Analyze Logs and other IT > data in > Real-Time with Splunk. Collect, index and harness all the fast moving > IT data > generated by your applications, servers and devices whether physical, > virtual > or in the cloud. Deliver compliance at lower cost and gain new > business > insights. http://p.sf.net/sfu/splunk-dev2dev > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Free Software Download: Index, Search & Analyze Logs and other IT data in Real-Time with Splunk. Collect, index and harness all the fast moving IT data generated by your applications, servers and devices whether physical, virtual or in the cloud. Deliver compliance at lower cost and gain new business insights. http://p.sf.net/sfu/splunk-dev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
