*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Wed, 30 May 2012 23:12:12 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1205292251410.19391@macbroy22.informatik.tu-muenchen.de> (message from Makarius on Tue, 29 May 2012 23:00:05 +0200 (CEST))*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205030338.q433ciL9026861@poisson.math.northwestern.edu> <201205250512.q4P5Cgns004328@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205251146380.8953@macbroy22.informatik.tu-muenchen.de> <201205270818.q4R8IUWm022240@poisson.math.northwestern.edu> <alpine.LNX.2.00.1205292251410.19391@macbroy22.informatik.tu-muenchen.de>

Thanks, Makarius, and I really like your posts on hol info. I'd be happy for you to post there about miz3 ocaml dirty code cache issues. The Isabelle/Pure framework is centered around higher-order natural deduction, and Isabelle/Isar as a proof language continues these ideas. To understand these things properly, you should first blot out "FOL", then get used to Pure + Isar, then add HOL as object-logic, and then rediscover what predicate logic (including FOL) will do for you here via some add-on tools. I'm not opposed to learning Pure + Isar, but it would be a whole lot easier for me to learn if I knew in advance how it related to FOL, which as a mathematician I have a rudimentary (but not practical) understanding of. Let me make a rudimentary FOL point: I think writing down strict axiomatic FOL proofs would really be tedious because e.g. you have manually substitute variables every time you want to use an axiom. I don't have a full list of the tedium strict FOL can cause. But I'm only willing to write up FOL-type proofs if the proof assistant will automate that tedium. Do similar issues arise with Pure + Isar? Also, as you may have observed on hol info, I know next to nothing about HOL. Basically I understand the 20 pages of set theory John explains in his reference manual. Isn't Isabelle HOL much the same as HOL as in HOL Light HOL? Where is a good place to learn about HOL? > Yes, and thus locales are definitely a real advantage of Isabelle > over HOL Light right now. Still, I wonder why one can't just > define all the sets you'd want in HOL Light (only very lightly > typed) to get something like a locale. In principle any of the HOL systems could provide their own locale mechanism, or something similar. It is not possible to "just" do it, though. Isabelle has required 10+ years to get this all done right. It is also a matter of culture. John Harrison would certainly not add such complexity to his system. You have to use Isabelle or Coq for such sophisticated module concepts, or maybe Mizar. Sure, but I really dislike the Mizar type system, and I want to lightly typed sets to avoid any hard typing. More below: > But instead we could look at all models of Tarski's axioms, a > model being some sets and functions with some properties. Can > you do this in Isabelle too? If this means you want to study the meta-theory of Tarski axioms, then any of the HOL systems -- Isabelle/HOL included -- can do this for you, if you define the syntax and inference system more concretely (via datatypes and inductive relations). Great, but I don't know what meta-theory means. A model of Tarski's geometry axioms is be a set S (of points), a 3-ary relation Between on S and a 4-ary relation Equiv on S satisfying Tarski's axioms (so far I only use his first 7 axioms, and you coded them up in Isabelle). So there might be a predicate TarskiModel(S, Between, Equiv), and theorems in a Tarski model would begin assume TarskiModel(S, Between, Equiv)... I don't understand HOL well enough to actually pull this off, but John explained how to get started. My point is that I don't think any typing is involved here, beyond maybe something rudimentary like new_type("point",0);; new_type_abbrev("TarskiPlane",`:point->bool`);; -- Best, Bill

**Follow-Ups**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Makarius

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Makarius

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Makarius

- Previous by Date: [isabelle] Automation is awesome; one bibliography leads to another
- Next by Date: Re: [isabelle] Automation is awesome; one bibliography leads to another
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list