Hi Mark,
Thanks for your clarification in response to my email available online at
https://groups.google.com/d/msg/metamath/EOw1J-TG26k/dp9bB977AgAJ
Preventing removal or redefinition of existing definitions in R0
is an effective way of providing the property of faithfulness
[Adams, 2016, p. 21], as I believe.
From a logical point of view, the logical kernel should be as small as possible.
For this reason, in R0 definitions are, unlike in HOL and its variants,
only implemented in the printer and parser, but are _not_ part (an extension)
of the logic,
as indicated in the email to John:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00087.html
For comparison, the definitional principles in HOL require an additional rule
introducing an axiom (!) for each single definition,
see subsection 2.5.1 (Extension by constant definition) at
http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-11/kananaskis-11-logic.pdf
If you think that the property of faithfulness does not hold for R0, as claimed
at
https://sourceforge.net/p/hol/mailman/message/35665823/
it would be helpful if you could provide a small counterexample.
Given the correctness of Mario's statement on Metamath at
https://groups.google.com/d/msg/metamath/EOw1J-TG26k/e6JLlvL9AgAJ
then currently HOL Zero, Metamath, and R0 are Pollack-consistent.
In R0, this concept (Pollack-consistency) is extended to whole proofs,
and also the property of faithfulness is provided.
Concerning this question, I haven't studied HOL Zero and Metamath yet.
Best regards,
Ken
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100
> Am 25.06.2017 um 11:17 schrieb Mark Adams <m...@proof-technologies.com>:
>
> Hi Ken,
>
> On 20/06/2017 12:38, Ken Kubota wrote:
>> This 2017 article by Thomas Hales et al. at _Forum of Mathematics, Pi_
>> seems to be identical with the 2015 article at:
>> https://arxiv.org/pdf/1501.02155.pdf
>
> Yes, as far as I am aware, if there are any differences they are tiny. Arxiv
> is a preprint service.
>
>> What I find even more interesting, is Mark's notion of
>> _faithfulness_,
>
> Unfortunately my definition of "faithfulness" is a bit vague. See below.
>
>> developing further Freek Wiedijk's notion of
>> _Pollack-consistency_ ("being able to correctly parse formulas that
>> it printed itself", quoted on p. 8).
>
> Strictly speaking from Freek's original paper, being able to correctly parse
> back printed formulas (i.e. forall tm. parse (print tm) = tm), is called
> having a "well-behaved" parser/printer. In his paper, "Pollack-consistency"
> is about not being able to derive "false" from assuming the equality of
> formulae that get printed the same. But when discussed, these concepts
> usually all get bundled together and described as "Pollack-consistency".
>
>> It seems as if Mark’s HOL Zero and my R0 are the only
>> implementations that have this property of Pollack-consistency.
>
> It's good to see that these properties are being taken seriously.
>
>> In the case of R0, this even holds for full proofs, and the
>> property of faithfulness is also implemented:
>> "Generally, definitions once introduced cannot be removed or
>> redefined (implementing the notion of 'faithfulness' as defined by
>> Mark Adams..)"
>
> The intention with my use of the term "faithfulness" was to capture what I
> understand others in the theorem proving community mean by the term. Freek's
> defintions are really basic properties of parsers/printers that users might
> naturally expect to hold, e.g. that parsing printed output always results in
> the original internal term. But if a printer printed "false" as "true" and
> "true" as "false", and the parser correspondingly parsed "true" as "false"
> and "false" as "true", then this would satisfy Freek's "well-behaved"
> property. So we need "faithfulness" to cover that sort of thing. Banning
> deletion or redefinition of theory isn't what I meant.
>
> Mark.
>
>
>>> Am 19.06.2017 um 23:15 schrieb Norman Megill <n...@alum.mit.edu>:
>>> Some of you may be interested in the following.
>>> A writeup of Hale's computer proof ("Flyspeck project") of the
>>> Kepler sphere-packing conjecture has just been published:
>>> T. Hale et. al, A Formal Proof of the Kepler Conjecture
>> https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC
>>> A blog entry on this:
>> http://blog.journals.cambridge.org/2017/06/12/proving-the-kepler-conjecture/
>>> The following paper discusses auditing issues for several proof
>>> languages in the context of the above proof:
>>> M. Adams, Proof Auditing Formalised Mathematics
>>> http://www.proof-technologies.com/papers/qed_paper.html
>>> Norm
>>> --
>>> You received this message because you are subscribed to the Google
>>> Groups "Metamath" group.
>>> To unsubscribe from this group and stop receiving emails from it,
>>> send an email to metamath+unsubscr...@googlegroups.com.
>>> To post to this group, send email to metam...@googlegroups.com.
>>> Visit this group at https://groups.google.com/group/metamath.
>>> For more options, visit https://groups.google.com/d/optout.
>> ------------------------------------------------------------------------------
>> 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@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
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@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
