The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

I can try to explain what this mysterious user meant :)

The process of designing a formal system like Coq usually involves picking a "sufficiently expressive logic". What this means can be a subject of debate, but most would agree that it at least is a logic which allows formalizing most of the interesting things that mathematicians prove. Just how much logical power you need to prove various important statements in mathematics is a very difficult question which is the subject of intense research in reverse mathematics.

However, a reasonable informal consensus is that ZFC + Universes (Grothendiek) proves more than 99% of the statements mathematicians outside of set theory are interested in. This happens to be about the strength of the Coq foundations (though the exact strength is still somewhat open I think). So conveniently, Coq is almost exactly the logic in which most proofs can easily be formalized. The reason for this strength comes in part from impredicative Prop. The strength of a predicative theory like Agda is much lower: in particular, you should be able to build models of the latter in the former.

This explains my comment: reassuring means "we have enough logical power for the foreseeable future" and "reasonable" means "we're not going to try and formalize large cardinal theory".

In theory though, most statements we're used to, like the prime number theorem and such, and even a lot of basic analysis, can be carried out in predicative theories, at the cost of much greater formalization complexity. I won't go into much detail because I'm out of my depth, but the wikipedia page on reverse mathematics has some more info. Here are some nice slides by Jeremy Avigad:
https://www.andrew.cmu.edu/user/avigad/Talks/asl04.pdf

Now the crux: a statement that is easy to prove in Coq with impredicative Prop but difficult or impossible to prove with Agda. This is tough for me I'm afraid. One example is normalization of system F, but that's cheating a bit. The statement in set theory that corresponds the closest to impredicative Prop is *unbounded seperation*. A mathoverflow question on the topic (http://mathoverflow.net/a/123583/36103) seems to suggest the statement:

"for each n a natural number, there exist n pairwise nonequinumerous infinite sets"

I'm not sure that this constitutes an actual example though. The SEP goes into more detail, but isn't terribly formal:

http://plato.stanford.edu/entries/set-theory-constructive/#PreConSetThe

Hope this helps,

Cody

On Wed, Feb 24, 2016 at 3:30 PM, Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi all,

Does anyone have a good resource to read about why Prop is impredicative, and why this is desirable? So far, I've found Adam Chlipala's Universes post and some answers to a stackexchange question. I'd like something a little more formal. For example, in the stackexchange post, Cody Roux notes:

> The expressiveness gained by impredicativity is "reassuring" in the sense 99% of "reasonable"
> mathematics can be formalized with it, and it is known to be consistent relative to set theory. This
> makes it likely they won't weaken it to something like Agda, which only has predicative universes.

I want to know more about that expressiveness. Why is it "reassuring," and what is "reasonable"? (I couldn't find a working email address for Cody Roux, or I'd try him as well.) Is it essential, or does it just make some things easier?

Similarly, Adam Chlipala's post has a few interesting examples of things we can do with impredicative Prop, but I'm interested in something broader and more formal. A research paper or talk would be great, if such a thing exists.

Thanks!

Talia

University of Washington