Ana de Almeida Borges (Nov 10 2020 at 17:09): Ana de Almeida Borges (Nov 10 2020 at 17:09):Is there a standard somewhere implementing eg EA, ISigma_n and PA in Coq? Such a development would include their definitions and enough lemmas and tools to allow one to prove theorems inside of these formal theories. Then it would also include famous theorems, such as Gödel's Incompleteness theorems, Löb's theorem, etc.
I know that the Incompleteness theorems have been formalized here: http://r6.ca/Goedel/goedel1.html but this is old and doesn't seem like it turned into a standard for working on top of these results... Or am I wrong?
I do research in provability logic and I enjoy implementing my research in Coq, but although implementing purely modal results is relatively straightforward (because it's elementary), I despair of ever starting to implement arithmetical results, because they are built on top of so much mathematics. So... has someone started doing this? Or is it a project to add to my to-do list? And if I hypothetically wanted to build such a library, would adapting Russell O’Connor's one (linked above) be a good place to start?
Karl Palmskog (Nov 10 2020 at 17:15):https://github.com/coq-contribs/goedel/tree/v8.9 is known to work with Coq 8.10
Karl Palmskog (Nov 10 2020 at 17:17):the only thing nominally "standard" in Coq is the Stdlib. You might be able to build what you want by combining directly using packages (e.g., coq-goedel is available in OPAM), or taking package sources and rolling your own project
Ana de Almeida Borges (Nov 10 2020 at 17:20):Thanks. I think your link is an updated version of mine (at least they have the same original authors). It is probably a good place to start!
I would also be interested in any work relying on coq-goedel.
Karl Palmskog (Nov 10 2020 at 17:22):some stuff that may be related: https://github.com/JasonGross/lob https://github.com/uds-psl/coq-library-undecidability https://github.com/coq-community/comp-dec-modal
Karl Palmskog (Nov 10 2020 at 17:23):The coq-contribs/goedel link is basically the most recently updated of O'Connor's formalization, can't see that any other package we have is using it
Karl Palmskog (Nov 10 2020 at 17:26):@Ana de Almeida Borges if you're interested in actually using/maintaining/updating the goedel development to work with Coq 8.11+, we could assist with that, see: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
Ana de Almeida Borges (Nov 10 2020 at 17:28):Karl Palmskog said:
Ana de Almeida Borges if you're interested in actually using/maintaining/updating the goedel development to work with Coq 8.11+, we could assist with that, see: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
I might! Maybe not literally today, but I'll look into it
Karl Palmskog (Nov 10 2020 at 17:29):fine with me, see here for an example of how the process usually works: https://github.com/coq-community/manifesto/issues/121
Emilio Jesús Gallego Arias (Nov 10 2020 at 23:06):@Ana de Almeida Borges have you read Connor's post-mortem of his Gödel development.
Emilio Jesús Gallego Arias (Nov 10 2020 at 23:06):?
Emilio Jesús Gallego Arias (Nov 10 2020 at 23:07):As far as I can tell, it is not a good idea of follow that style; I think .
Emilio Jesús Gallego Arias (Nov 10 2020 at 23:07):I'll take the liberty to copy @Yannick Forster @Fabian Kunze in case they'd be interested in your questions.
Ana de Almeida Borges (Nov 10 2020 at 23:19):Emilio Jesús Gallego Arias said:
Ana de Almeida Borges have you read Connor's post-mortem of his Gödel development.
Do you mean http://r6.ca/Goedel/goedel1.html ? I only skimmed it.
Emilio Jesús Gallego Arias (Nov 11 2020 at 00:00):I don't recall the exact reference sorry, may try to look it up; maybe Paulson commented on it [I assume you know Paulson's two fantastics articles on Gödel's 2nd]
Emilio Jesús Gallego Arias (Nov 11 2020 at 00:02):Maybe that's actually on Connor's thesis?
Emilio Jesús Gallego Arias (Nov 11 2020 at 00:02):It was a nice description of all the things that went wrong with the development [many]
Ana de Almeida Borges (Nov 11 2020 at 00:13):Yeah, the page I linked sumarizes some of the difficulties and decisions that Connor later regretted. Seems useful in case one wanted to do everything from scratch... But I didn't get the idea that the design decisions were bad enough to justify such an effort... Maybe some refactoring could be done, although at this point I have a hard time gauging the costs and benefits of doing so.
Ana de Almeida Borges (Nov 11 2020 at 00:14):Emilio Jesús Gallego Arias said:
I don't recall the exact reference sorry, may try to look it up; maybe Paulson commented on it [I assume you know Paulson's two fantastics articles on Gödel's 2nd]
I didn't, but I think I found them and I'll take a look, thanks!
Yannick Forster (Nov 11 2020 at 09:26):Thanks Emilio for conjuring us :)
Yannick Forster (Nov 11 2020 at 09:28):We did lots of work regarding first-order logic in Coq recently, and learned quite a bit how to precisely mechanise its definition in Coq. The TLDR is: Use de Bruijn indices, and ideally use Autosubst2 to get good simplification tactics which will ease your life a lot
Yannick Forster (Nov 11 2020 at 09:29):A good benchmark is always to check how hard it is to prove weakening - and with the definition we now use that's really easy
Yannick Forster (Nov 11 2020 at 09:30):Unfortunately, the "perfect" mechanisation does not exist yet. We used one that we were very happy with to mechanise completeness proofs (https://www.ps.uni-saarland.de/extras/fol-completeness/), and Dominik Kirst and Dominique Larchey-Wendling used a very similar definition to prove Trakthenbrot's theorem (https://www.ps.uni-saarland.de/extras/fol-completeness/)
Yannick Forster (Nov 11 2020 at 09:31):Also, Dominik is working on mechanisations of PA at the moment, maybe the preliminary results there will help you to answer your questions. I'll try the conjuring thing again: @Dominik Kirst, can you help?
Karl Palmskog (Nov 11 2020 at 09:42):@Yannick Forster is autosubst2 compatible with latest Coq (8.12 and beyond?)
Yannick Forster (Nov 11 2020 at 09:43):Autosubst 2 is a Haskell program which prints Coq files, so there is no universal statement regarding newer versions of Coq. But in my experience (I've used it for a System F variant recently) it is compatible with Coq 8.12, yes
Ana de Almeida Borges (Nov 11 2020 at 12:27):Amazing! Thanks for the links.
Ana de Almeida Borges (Nov 11 2020 at 12:28):(The second one is repeated, but I assume you meant https://arxiv.org/abs/2004.07390 )
Dominik Kirst (Nov 11 2020 at 14:43):Yep, that's the right link to our paper on Trakhtenbrot's theorem :)
Regarding PA, we're currently working on undecidability by reduction from diophantine equations (which also yields a weak version of incompleteness) and on Tennenbaum's theorem (which in our framework states that no countable non-standard model of PA exists with addition and multiplication given as Coq functions). The underlying FOL mechanisation is a merge of lessons learned from our completeness and Trakhtenbrot developments and hopefully close to a fixed point.
Ana de Almeida Borges (Nov 11 2020 at 15:06):I look forward to reading about that when it's done!
Do you know of any work built on top of your previous Coq mechanisations? And did I understand correctly that although you were inspired by your previous work, you are not directly relying on it in your current development?
Emilio Jesús Gallego Arias (Nov 11 2020 at 20:25):But I didn't get the idea that the design decisions were bad enough to justify such an effort... Maybe some refactoring could be done, although at this point I have a hard time gauging the costs and benefits of doing so.
Indeed it is always hard to measure the tradeoff between reworking an implementation or trying to extend it and accept the flaws. In my opinion, and based on other efforts, I'd recommend starting from some other approaches, and in particular pay attention to Paulson's comments on the tricky parts.
Yannick Forster (Dec 02 2020 at 08:24):There's an Autosubst 2 GitHub repo now: https://github.com/uds-psl/autosubst2
Last updated: Apr 16 2024 at 05:01 UTC