Stream: Coq users

Topic: Reverse Mathematics in Coq


view this post on Zulip saddle196883 (Aug 19 2023 at 07:58):

Hello all! I am really new to proof assistants and Zulip, so I apologize if I don't have any idea about what I am asking, or if I'm in the wrong stream.

TL:DR: Suppose I want to try to formalize reverse mathematics in Coq as a project. Is this sane?

I'm in my third year of my undergraduate mathematics degree and I am starting to think about projects to do for a bachelor's thesis. I am especially interested in reverse mathematics, but a general theme in computability theory is that the proofs are given in a kind of "procedural" style, where you give a sort of recipe to construct a set in an attempt to convince the reader something is true. I figure it would be nice to be able to formalize proofs about classical reverse mathematics in a proof assistant, say Coq, but I am not sure if this works because I can't seem to find any such work online.

My "plan" is to somehow formalize RCA_0 in Coq, somehow have the ability to add extra axioms to state and prove certain classic analysis theorems (e.g. Heine Borel), and do the reverse part by proving the additional axioms assuming the theorem. I think this would make a passable project if I do succeed...

Normally for such questions, it would be wise to approach a faculty member in my university to ask, but I don't think any of the faculty in my university works with proof assistants (not that I know of). I know a professor who works with reverse mathematics but I don't believe he has experience with proof assistants. A quick google search reveals that there was a seminar a decade ago that did this, but unfortunately I did not find any materials related to the seminar at all, despite heavy googling.

Hence this post. I want to know if what I'm suggesting is sane for an undergraduate to do as a project, and if it is, is there any resources I can look at. Thank you!

view this post on Zulip Karl Palmskog (Aug 19 2023 at 08:02):

I recommend taking a look at previous work on reverse math in Coq like this one: https://arxiv.org/abs/2009.00416 https://github.com/uds-psl/churchs-thesis-coq

cc: @Yannick Forster who may be able to link more previous work on rev math in Coq.

view this post on Zulip saddle196883 (Aug 19 2023 at 08:04):

I will take a look at it. Thank you!

view this post on Zulip Yannick Forster (Aug 19 2023 at 08:44):

Hello, always happy to see reverse mathematics questions pop up here! :) Thanks for the ping Karl

view this post on Zulip Yannick Forster (Aug 19 2023 at 08:45):

First, let me mention that there are two related but relatively separate areas of reverse mathematics: Classical Reverse mathematics á la Friedman, with the important book by Simpson. Here everything is based on RCA_0, a logic which allows the law of excluded middle, i.e. classical proofs, but has almost no set comprehension principles. The central question then is how strong comprehension principles need to be to prove certain results, e.g. the mentioned Heine Borel theorem

view this post on Zulip Yannick Forster (Aug 19 2023 at 08:47):

And then there is Constructive Reverse Mathematics à la Ishihara: Here one works in a Bishop style constructive logic with arbitrary comprehension principles but no classical principles such as the law of excluded middle, and then asks similar questions

view this post on Zulip Yannick Forster (Aug 19 2023 at 08:47):

With Dominik Kirst and other colleagues, I have worked on constructive reverse mathematics questions for computability theory and for first-order logic

view this post on Zulip Yannick Forster (Aug 19 2023 at 08:47):

The relevant papers are linked here https://github.com/uds-psl/coq-synthetic-computability/ and here https://github.com/uds-psl/coq-library-fol

view this post on Zulip Yannick Forster (Aug 19 2023 at 08:49):

I would say that a RCA_0 proof of Heine Borel in Coq would make up for very exciting work, but I would expect it to be very, very, very challenging, to the point where my first gut feeling is that it is too challenging - not even just from the perspective of being a Bachelors' thesis topic, but even from the perspective of being a machine-checkable result

view this post on Zulip Yannick Forster (Aug 19 2023 at 08:49):

The reason is that one has to formalize RCA_0, and then carry out all proofs in this logic, meaning that results in libraries of Coq proofs or Coq tactics become useless - one has to construct derivations for everything explicitly, which creates a huge overhead

view this post on Zulip Yannick Forster (Aug 19 2023 at 08:51):

But: @saddle196883 you can drop me an email at yannick.forster@inria.fr and maybe it makes sense to chat via Zoom a bit? I don't know whether I can really help in the end with finding a suitable topic in this area, but I can try :)

view this post on Zulip Karl Palmskog (Aug 19 2023 at 08:52):

on the other hand, there has been work on "proof modes" for reasoning inside a logic embedded in Coq using tactics. The most famous is the Iris proof mode. However, proof modes are in my view definitely not bachelor level material.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 08:57):

Also, I'd have to recommend bachelor-level projects that do some small well-defined contribution to an existing Coq library over making new projects from scratch

view this post on Zulip saddle196883 (Aug 19 2023 at 09:03):

Yannick Forster said:

But: saddle196883 you can drop me an email at yannick.forster@inria.fr and maybe it makes sense to chat via Zoom a bit? I don't know whether I can really help in the end with finding a suitable topic in this area, but I can try :)

Sure! I am writing an email now.

view this post on Zulip saddle196883 (Aug 19 2023 at 09:05):

Karl Palmskog said:

Also, I'd have to recommend bachelor-level projects that do some small well-defined contribution to an existing Coq library over making new projects from scratch

This sounds like a good idea, but if no one in my faculty does Coq related work, I am not sure if they are willing to supervise such a project. I will certainly try asking around though.

view this post on Zulip Karl Palmskog (Aug 19 2023 at 09:09):

I was hinting at that Yannick might point to a project that performs some extension on top of the UDS-PSL Coq libraries, but he may already have thoughts in that direction. Just saying that something like this would likely have a much higher chance of success than a "new" project.

view this post on Zulip Yannick Forster (Aug 19 2023 at 09:11):

Mark Koch indeed implemented a FOL proof mode, heavily inspired by Iris, as part of the uds-psl FOL library: https://coq-workshop.gitlab.io/2021/slides/Coq2021-02-01-slides-fol-toolbox.pdf And I agree, maybe we can find something that extends previous work by Dominik and colleagues rather than starting from scratch

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 15:21):

In addition to all the great info here, Lawrence Paulson paper about the formalization of Gödel's 2nd incompleteness theorem has a great writeup of the challenges of working in a "reductionist" setting, in his case HF sets .


Last updated: Jun 18 2024 at 22:01 UTC