walker (Apr 20 2022 at 00:46): walker (Apr 20 2022 at 00:46):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?
Emilio Jesús Gallego Arias (Apr 20 2022 at 00:53):Yes @walker , I don't have the time now to expand on that, but there is a lot of work
Emilio Jesús Gallego Arias (Apr 20 2022 at 00:53):that studies your question, with different resutls
Emilio Jesús Gallego Arias (Apr 20 2022 at 00:54):You can start by having a look here https://en.wikipedia.org/wiki/Ordinal_analysis
Emilio Jesús Gallego Arias (Apr 20 2022 at 00:54):but there's plenty to be said about your question
walker (Apr 20 2022 at 01:04):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.
walker (Apr 20 2022 at 01:18):@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 ?
Paolo Giarrusso (Apr 20 2022 at 01:45):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?
Ali Caglayan (Apr 20 2022 at 07:06):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.
Karl Palmskog (Apr 20 2022 at 07:09):moving this to Miscellaneous, since the topic is not directly related to using Coq
Notification Bot (Apr 20 2022 at 07:09):This topic was moved here from #Coq users > Properties of logic by Karl Palmskog.
Emilio Jesús Gallego Arias (Apr 20 2022 at 10:18):@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"
Emilio Jesús Gallego Arias (Apr 20 2022 at 10:19):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.
Ulrik Buchholtz (Apr 30 2022 at 16:23):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 , which is closely related to Coq's type theory, though a bit weaker.
Last updated: Sep 15 2024 at 13:02 UTC