This might not be related to coq, but I am not sure where to ask, is there a way to tell how powerful certain logic is?

What I am trying to do is .. given some logic rules (CIC for example) try to figure out what can be represented in that logic and what cannot be represented in that logic.

In computer science we had the notion of turing completeness where if programming language can implement `and`

, `or`

, and `not`

. It is turing complete and it can implement any decidable algorithm.

Is there similar notion this is more generic and suitable for quantifying how powerful a logic is?

Yes @walker , I don't have the time now to expand on that, but there is a lot of work

that studies your question, with different resutls

You can start by having a look here https://en.wikipedia.org/wiki/Ordinal_analysis

but there's plenty to be said about your question

Well, ofcourse there must be a whole field of study for that (this is sad sarcasm)

I am reading the wikipedia article, If you know a good reading material for dummies (literally) that would make my life easy... note that my background is not mathematics but I willing to dive into the topic as long the the material asume minimal background.

@Emilio Jesús Gallego Arias well, this is exactly what I was looking for, wikipedia article explains it well, aside from the reading material I wanted to understand how how trivial / complex is the process of assigning ordinal to logic ?

That page says

Most theories capable of describing the power set of the natural numbers have proof-theoretic ordinals that are so large that no explicit combinatorial description has yet been given.

And AFAICT, impredicative theories (like Coq) _can_ describe the powerset of natural numbers. Can ordinal analysis say much about those?

The question becomes much harder when you consider Coq's impredicative prop. Typically in proof theoretic ordinal analysis, impredicative theories have a much larger ordinal. Intuitionistic ZF for instance is equiconsistent with ZF, which we have close to zero idea how to quantify with oridinal analysis. I believe I have seen people mention that the calculus of inductive constructions in equiconsistent with some impredicative flavour of set theory, but I can't be sure without having seen the details.

If you restrict Coq to the predicative fragment, i.e. only using Set and Type then it should be equiconsistent with something like Martin-Lof typt theory with an infinite hierarchy of universes and W-types, which the oridinal analysis of had been done. Therefore, I would assume that Coq lies somewhere inbetween this and ZF + countably many inaccessible cardinals.

In practice however, almost nobody uses the full logical strength of Coq, so it would be a safe assumption to restrict to the predicative fragment, as long as you are careful.

moving this to Miscellaneous, since the topic is not directly related to using Coq

This topic was moved here from #Coq users > Properties of logic by Karl Palmskog.

@walker logical strength analysis is not my specialty so I don't feel very qualified to recommend books on the subject [some people here may], another interesting thing to look at is "reverse mathematics" which asks the dual question "what is the weakest ordinal needed to prove a particular result"

walker said:

Well, ofcourse there must be a whole field of study for that (this is sad sarcasm)

I can see how it that realization may come with a bit of overwhelming feel, but I think your question is great and very much on topic here! And the fact that there is already a field of study doesn't mean that there is not a lot to think about it still.

Paolo Giarrusso said:

And AFAICT, impredicative theories (like Coq) _can_ describe the powerset of natural numbers. Can ordinal analysis say much about those?

Not directly, but see Michael Rathjen's Relativized ordinal analysis, the result of which then went into this chapter, giving the strength of a type theory $\mathrm{MLV}_{\mathrm{P}}$, which is closely related to Coq's type theory, though a bit weaker.

Last updated: Aug 19 2022 at 20:03 UTC