Email Gateway (Nov 15 2023 at 20:07): Email Gateway (Nov 15 2023 at 20:07):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi all,
An exciting new entry formalizes Q0, Peter Andrews’ flavor of classical higher-order logic, and proves its soundness and consistency:
Metatheory of Q0
by Javier Diaz
Abstract: This entry is a formalization of the metatheory of Q0 in Isabelle/HOL. Q0 is a classical higher-order logic equivalent to Church's Simple Theory of Types. In this entry we formalize Chapter 5 of "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof" (Andrews, 2002), up to and including the proofs of soundness and consistency of Q0. These proof are, to the best of our knowledge, the first to be formalized in a proof assistant.
https://www.isa-afp.org/entries/Q0_Metatheory.html
Could this be a starting point to formally verify soundness and consistency of Isabelle/HOL?
Enjoy!
Dmitriy
Email Gateway (Nov 16 2023 at 13:14):From: Anders Schlichtkrull <cl-isabelle-users@lists.cam.ac.uk>
Dear Javier Díaz, Dmitriy and Isabelle Users
Javier, let me congratulate you on your great work! I have taken a look at it, and I have to say that I am very impressed! This is a very thorough formalization of Peter Andrews' Q0 system!
I have myself also formalized the soundness result for theorems in Q0.
It is available here:
https://github.com/IsaFoL/IsaFoL/tree/master/Q0
(Previously it was at https://bitbucket.org/isafol/isafol/src/master/Q0/ )
By coincidence my plan was (and still is) to submit this to AFP tomorrow.
I have uploaded the generated pdf, if someone is curious to take a look already now:
https://github.com/IsaFoL/IsaFoL/blob/master/Q0/document-13Nov2023.pdf
Javier, I will of course update my submission to cite your impressive AFP entry.
Cheers,
Anders
Email Gateway (Nov 16 2023 at 18:39):From: Javier Díaz <cl-isabelle-users@lists.cam.ac.uk>
Dear Anders and Isabelle users,
Anders: Thanks a lot for your kind words, they're much appreciated. :)
Just to clarify matters, please allow me to point out that Anders'
formalization includes the proof of the _weak_ soundness of Q0 (Theorem
5402(a)), whereas my formalization includes both the weak and strong forms
(Theorem 5402(a) and 5402(b)). Proving the strong form is a quite complex
task, since the proof uses the Deduction Theorem, whose proof needs virtually
all the results in Section §52 of Andrews' textbook.
Kindest regards,
Javier
Email Gateway (Nov 17 2023 at 16:53):From: Anders Schlichtkrull <cl-isabelle-users@lists.cam.ac.uk>
On Nov 16, 2023, at 19:39, Javier Díaz <cl-isabelle-users@lists.cam.ac.uk> wrote:
Dear Anders and Isabelle users,
Anders: Thanks a lot for your kind words, they're much appreciated. :)
The kind words are well deserved! :)
Just to clarify matters, please allow me to point out that Anders'
formalization includes the proof of the _weak_ soundness of Q0 (Theorem
5402(a)), whereas my formalization includes both the weak and strong forms
(Theorem 5402(a) and 5402(b)). Proving the strong form is a quite complex
task, since the proof uses the Deduction Theorem, whose proof needs virtually
all the results in Section §52 of Andrews' textbook.
Yes, I agree with you. This is a clear distinction between the two formalizations.
Kindest regards,
Anders
Last updated: May 04 2024 at 20:16 UTC