Stream: Miscellaneous

Topic: Formal theories and Provability Logic in Coq


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2020 at 23:06):

?

view this post on Zulip 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 .

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Emilio Jesús Gallego Arias (Nov 11 2020 at 00:02):

Maybe that's actually on Connor's thesis?

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Yannick Forster (Nov 11 2020 at 09:26):

Thanks Emilio for conjuring us :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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/)

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Nov 11 2020 at 09:42):

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

view this post on Zulip 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

view this post on Zulip Ana de Almeida Borges (Nov 11 2020 at 12:27):

Amazing! Thanks for the links.

view this post on Zulip 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 )

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yannick Forster (Dec 02 2020 at 08:24):

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


Last updated: Aug 19 2022 at 21:02 UTC