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?

https://github.com/coq-contribs/goedel/tree/v8.9 is known to work with Coq 8.10

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

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`

.

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

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

@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

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

fine with me, see here for an example of how the process usually works: https://github.com/coq-community/manifesto/issues/121

@Ana de Almeida Borges have you read Connor's post-mortem of his Gödel development.

?

As far as I can tell, it is not a good idea of follow that style; I think .

I'll take the liberty to copy @Yannick Forster @Fabian Kunze in case they'd be interested in your questions.

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.

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]

Maybe that's actually on Connor's thesis?

It was a nice description of all the things that went wrong with the development [many]

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.

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!

Thanks Emilio for conjuring us :)

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

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

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/)

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?

@Yannick Forster is autosubst2 compatible with latest Coq (8.12 and beyond?)

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

Amazing! Thanks for the links.

(The second one is repeated, but I assume you meant https://arxiv.org/abs/2004.07390 )

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.

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?

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.

There's an Autosubst 2 GitHub repo now: https://github.com/uds-psl/autosubst2

Last updated: Jun 01 2023 at 13:01 UTC