Re: [Hol-info] Pollack-consistency (HOL Light, Isabelle, and others); Introductions to HOL4 and HOL Zero

[Ken K. <ma...@ke...>]

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 <ma...@pr...>:
> 
> 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