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 <m...@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@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
