*To*: HOL-info list <hol-info at lists.sourceforge.net>, cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Correction on Hilbert-style systems (Metamath) and comment on prooftoys.org / mathtoys.org*From*: Ken Kubota <mail at kenkubota.de>*Date*: Sun, 19 Mar 2017 12:26:41 +0100*Cc*: "Prof. Peter B. Andrews" <andrews at cmu.edu>, Cris Perdue <cris.perdue at gmail.com>*References*: <1B749F74-5E4B-4C91-A3DF-E9EBE6140492@kenkubota.de>

Dear List Members, 1. An earlier statement of mine in the HOL and Isabelle mailing lists on R0 has to be corrected. The claim that "Unlike all other existing proof assistants or proof checkers, it is a Hilbert-style system", has to be relativized, since, depending on how strictly a Hilbert-style system is defined, Metamath may be considered a Hilbert-style system, too: "Natural Deduction in the Metamath Proof Explorer (MPE) MPE is fundamentally a Hilbert-style system." http://us.metamath.org/mpegif/mmnatded.html 2. Another discovery is Cris Perdue's implementation of a natural deduction variant of Peter B. Andrews' logic Q0 at prooftoys.org and mathtoys.org Although the equation solver is quite strong and impressive, Cris Perdue considers his implementation as "work in progress". Interestingly, it seems as if independently in same cases for this variant of Q0 exactly the same design decisions were made as for R0, in particular, the replacement of the turnstile by the logical implication, and the corresponding implementation of Rule R'. Kind regards, Ken Kubota ____________________ Ken Kubota http://doi.org/10.4444/100 > Anfang der weitergeleiteten Nachricht: > > Von: Ken Kubota <mail at kenkubota.de> > Betreff: Aw: [Hol-info] Pollack-consistency (HOL Light, Isabelle, and others); Introductions to HOL4 and HOL Zero > Datum: 14. Februar 2017 um 17:42:44 MEZ > An: Mark Adams <mark at proof-technologies.com> > Kopie: cl-isabelle-users at lists.cam.ac.uk, "Prof. Peter B. Andrews" <andrews at cmu.edu>, John Harrison <John.Harrison at cl.cam.ac.uk>, Freek Wiedijk <freek at cs.ru.nl>, Michael Norrish <Michael.Norrish at data61.csiro.au>, HOL-info list <hol-info at lists.sourceforge.net> > > Dear Mark, > > For the property of "faithfulness" defined in your paper, I have added a flag > which is necessary in order to redefine or undefine a (non-temporary, i.e., > non-local) definition. Hence in default mode, if you start the program > supplying first the definitions relevant for you, for example with > ./R0 definitions1.r0.txt undefine.r0.txt > attempts to modify definitions produce an error message: > > [...] > ## Undefine truth definition > := T > # error 1 [undefine.r0.txt]: definition removal not allowed without flag > # 1 error generated > > For the definitions in file "definitions1.r0.txt", see pp. 356 f. of > http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf > > I expect a publication of the formulae of R0 in March or April, and of the > software in the course of the year. > > But let me remark that R0 is designed for expressiveness, not for automation; > hence for foundational research rather than practical purposes. Unlike all > other existing proof assistants or proof checkers, it is a Hilbert-style > system; moreover, it doesn't have a tactical meta-language (such as ML used by > HOL) at all. Formalizing larger proofs in it will be quite exhausting (although > of course, in principle possible). In this respect, it is less efficient than > the HOL family, and more or less the exact opposite to Isabelle (with its focus > on automation). > > Being designed for expressiveness (reducibility) in the spirit of Q0 means that > all elements of the formal language are reduced to the most basic components, > trying to introduce both symbols and rules as far as possible as derived, and > not as primitive symbols and rules. The concept of expressiveness is carried > out consequently, e.g., by reducing the variable binders to lambda as the > single one for binding type variables also, which leads to type abstraction > (Gordon: "'second order' [lambda]-terms"), see, for example, the definition of > the universal quantifier involving \t ([lambda] t with t of type tau, the type > of types) provided with the link above. The design principles are chosen to > arrive at the natural language of mathematics. > > For the reduction of rules, see for example the HOL primitive rule of inference > for discharging an assumption [DISCH] as described in [Gordon, 2001, p. 20] > http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf > which in Q0 is obtained as a derived (!) rule of inference in form of a > Hilbert-style metatheorem [Andrews, 2002, pp. 228 f. (5240 = Deduction > Theorem)], and like all other derived rules, from the single rule of inference > of Q0. > > I have only a partial understanding of Isabelle, but it seems to go further > than HOL in terms of that the "Meta-logic" operator ==> mentioned on p. 11 of > http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016-1/doc/main.pdf > is supposed to symbolically represent what in Hilbert-style systems can only be > informally stated as a metamathematical statement (e.g., "If [...] then [...]." > [Andrews, 2002, p. 228 (5240)]). > > The philosophical idea is to relate the different representations of > mathematics, showing that Hilbert-style is more fundamental and natural than > "natural deduction", as it has less prerequisites and as it reveals the > dependencies (e.g., between primitive and derived rules of inference), or, > generally speaking, by going further down to the logical grounds. Ideally, it > should be possible to formalize the deductive systems within a system (like in > Goedel's proof) and show that they are isomorphic in terms of the theorems that > can be obtained in them. I would then argue that the other systems (natural > deduction) derive their legitimacy through this isomorphism to the original > more basic (Hilbert-style) logic. > > Ken > > ____________________ > > Ken Kubota > http://doi.org/10.4444/100 > > > >> Am 13.02.2017 um 20:28 schrieb Mark Adams <mark at proof-technologies.com>: >> >> Unfortunately, and embarrassingly, there is not yet a system description paper for HOL Zero. I plan to write one soon (but I think I said that a few years ago..). >> >> I should take a good look at R0 some time and could then comment on it, but good to hear that steps have been taken to address concerns about pretty printing. Clearly the qualities enumerated in Freek's paper are all desirable, but remember that there is also "faithfulness", which isn't fully addressed by the concept of Pollack-consistency. You could print something wrongly but also parse it back in correspondingly wrongly (so, for example, print & parse "true" as "false" and vice versa). >> >> Mark. >> >> On 13/02/2017 15:38, Ken Kubota wrote: >>> Dear List Members, >>> Through Mark Adams' paper "HOL Zero's Solutions for Pollack-Inconsistency" >>> (2016) linked at the HOL Zero homepage, I became aware of the notion of >>> Pollack-consistency coined by Freek Wiedijk for the property of "a system being >>> able to correctly parse formulas that it printed itself": >>> Freek Wiedijk: Pollack-inconsistency >>> http://doi.org/10.1016/j.entcs.2012.06.008 >>> http://www.cs.kun.nl/~freek/pubs/rap.pdf >>> It is amusing to see how the parsing and printing functions of John's HOL Light >>> are put on the rack and stretched quite a bit. >>> Also Isabelle and other systems are examined. >>> The interesting point for me was to see that somebody had the same idea. In the >>> R0 implementation, not only a formula, but whole printed proofs can be parsed >>> again. In fact, if it is compiled and started with "make check", R0 loops >>> through all proofs, and this is done twice, with the output of the first run as >>> the input of the second, stopping immediately with an error message if a proof >>> fails or if the output of the two runs differ. This was implemented quite >>> early, so the system was designed from the very beginning to comply with a >>> notion of Pollack-consistency not only in terms of formulae, but in terms of >>> whole proofs. Like for HOL Zero, this was done in order "to achieve the highest >>> levels of reliability and trustworthiness through careful design and >>> implementation of its core components" - quoted from: >>> Mark Adams: HOL Zero's Solutions for Pollack-Inconsistency >>> http://doi.org/10.1007/978-3-319-43144-4_2 >>> http://www.proof-technologies.com/holzero/hzsyntax_itp2016.pdf >>> Concerning HOL4 and HOL Zero, I am looking for introductions to them in the >>> literature. The appropriate candidates seem to be, at the first glance (without >>> having read them already): >>> Mark Adams: Introducing HOL Zero (Extended Abstract) >>> http://doi.org/10.1007/978-3-642-15582-6_25 >>> Konrad Slind, Michael Norrish: A Brief Overview of HOL4 >>> http://doi.org/10.1007/978-3-540-71067-7_6 >>> The latter I found as reference no. 14 of Mark's 2016 paper. >>> Please let me know if you have other suggestions. >>> Kind regards, >>> Ken Kubota >>> ____________________ >>> Ken Kubota >>> http://doi.org/10.4444/100 > > > ------------------------------------------------------------------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, SlashDot.org! http://sdm.link/slashdot > _______________________________________________ > hol-info mailing list > hol-info at lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info

- Previous by Date: Re: [isabelle] LaTeX and underscores in theory names
- Next by Date: Re: [isabelle] Pushouts in Isabelle
- Previous by Thread: Re: [isabelle] LaTeX and underscores in theory names
- Next by Thread: Re: [isabelle] Pushouts in Isabelle
- Cl-isabelle-users March 2017 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