Email Gateway (Aug 22 2022 at 10:44): Email Gateway (Aug 22 2022 at 10:44):From: Ken Kubota <mail@kenkubota.de>
Dear Ramana Kumar and List Members,
Thank you for your criticism and questions available at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00149.html
concerning my project announcement at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html
There are two motivations for this project besides the elegance of Q0:
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:
http://dx.doi.org/10.4444/100.101
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.)
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
http://dx.doi.org/10.4444/100
Last updated: Apr 25 2024 at 20:15 UTC