[isabelle] Addendum - Implementing the higher-order logic Q0 within the Isabelle proof assistant software

Dear Ramana Kumar and List Members,

Thank you for your criticism and questions available at
concerning my project announcement at

There are two motivations for this project besides the elegance of Q0:

1. The implementation of Q0 should be realized as a Hilbert-style system, since 
axiomatic (Hilbert-style) systems and natural deduction systems show a 
different behavior.
Theorems (and each line of a proof) in Hilbert-style systems always have a 
constant number (one or zero) of occurrences of the deduction symbol 
(turnstile), hence the theorem proved in the files available at 
http://dx.doi.org/10.4444/100.102 cannot be expressed, and Goedel's First 
Incompleteness Theorem cannot be obtained in a Hilbert-style system (like any 
other theorem with two or more occurrences of the deduction symbol, unless it 
is a metatheorem, i.e., it makes use of syntactical variables).
Since Q0 is a Hilbert-style system, the proof of Goedel's First Incompleteness 
Theorem fails in it (step 7101.4 has no syntactic justification), although this 
is not caused by unwanted restrictions of Q0. For details, please see: 
Thus axiomatic (Hilbert-style) systems and natural deduction systems differ not 
only in terms of the proof style, but also in terms of the expressiveness of 
the language.
I do not want to discard the results of natural deduction systems as a whole, 
but the class of theorems that can be obtained in natural deduction systems 
only seems problematic to me. For this reason, I prefer axiomatic 
(Hilbert-style) systems such as Q0.
(The Isabelle implementations of higher-order logic are natural deduction 
systems, as of my knowledge, and Isabelle is the only proof assistant software 
I know of that is easy and convenient to handle according to the specification 
in the announcement.)

2. On the basis of an implementation of Q0, an implementation of my own 
(currently unpublished) system R0 within Isabelle might be possible, which 
allows for type variables and binding of type variables with lambda and 
therefore has the expressiveness of polymorphic and dependent type theory, thus 
removing the limitations of Q0. I already finished the R0 software 
implementation as an independent proof verification system on my own and 
carried out many of Andrews' proofs in it, but for the layer of proof 
automation on top of that, a machinery is desirable, the development and 
maintenance of which would go beyond the capabilities of a single person.

If there are any further questions, please check my website (see below) instead 
of the mailing list only, as I might include a project page there. Also, I 
might need some time to answer appropriately.

Kind regards,

Ken Kubota


Ken Kubota
doi: 10.4444/100

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.