walker (Oct 20 2022 at 11:56): walker (Oct 20 2022 at 11:56):I understand that strong normalization of PCUIC terms is not proven in metacoq, and the property is turned into Axiom.
I understand the general idea of godel incompleteness but not the details on any level and from there I have four questions:
1- what inspires confidence that PCUIC is strong normalizing if we cannot prove it in Coq ?
2- is there an axiom-free system stronger than Coq that can prove normalization of PCUIC ?
3- if yes then why that system is not the base for Coq ?
4- If yes .. lets call that system "FOO" and I will be asking again the previous 4 questions for FOO instead of PCUIC (It sounds ridiculus but I want to know how to get system with no trusted computing base, if possible).
Edit:
5- given that PCUIC is encoded in coq, does that mean PCUIC is strongly normalizing iff coq is strongly normalizing (implicitly)?
Pierre-Marie Pédrot (Oct 20 2022 at 12:17):Your point 4. is unrelated to the TCB, it's a foundational regression ad infinitum.
Pierre-Marie Pédrot (Oct 20 2022 at 12:18):In theory you could prove that CIC has all the good metatheoretical properties on paper in ZFC + ω universes
Pierre-Marie Pédrot (Oct 20 2022 at 12:18):but this does not affect the code
Pierre-Marie Pédrot (Oct 20 2022 at 12:21):As for the other points:
Pierre-Marie Pédrot (Oct 20 2022 at 12:22):but probably the most important thing about reasonable type theories is that you don't really care about SN in practice. What matters for inspectability of proofs is that they can be run (in theory) and you can check that on Σ01 formulae you get something that makes sense.
Pierre-Marie Pédrot (Oct 20 2022 at 12:22):if it converges, you're fine, otherwise just wait a bit more.
Pierre-Marie Pédrot (Oct 20 2022 at 12:23):The things one should be concerned about when talking about SN are the gaps between CIC as implemented in Coq, and the smaller toy theories.
Pierre-Marie Pédrot (Oct 20 2022 at 12:24):Typical sources of concern of mine: Prop, the guard condition, modules
walker (Oct 20 2022 at 12:57):I assumed that type systems are axiom free, they come with judgements and indution principle (unlike axiomatic systems like ones from hilbert).
I am sure what is Σ01 formulae,
Also can you point me to a simple proof layout for one of those languages with some form of dependent types ?
Pierre-Marie Pédrot (Oct 20 2022 at 13:09):this is probably the best you can find publicly: https://github.com/mr-ohman/logrel-mltt
Paolo Giarrusso (Oct 22 2022 at 01:14):I am sure what is Σ01 formulae
If you're not sure, I understand https://en.wikipedia.org/wiki/Arithmetical_hierarchy is relevant
Kenji Maillard (Oct 22 2022 at 09:27):I don't know how faithful it is, but whenever I talk with @Pierre-Marie Pédrot and he mentions a property only valid of formula I automatically translate that in my head into "plain finitary inductive data-types" (that do not involve functions for instance).
walker (Oct 22 2022 at 10:56):Paolo Giarrusso said:
I am sure what is Σ01 formulae
If you're not sure, I understand https://en.wikipedia.org/wiki/Arithmetical_hierarchy is relevant
oh that was one crucial missing word I meant "I am not sure" ...
Pierre-Marie Pédrot (Oct 22 2022 at 11:01):not only finitary, stuff like Σn : nat. n = 0 is also fine.
Kenji Maillard (Oct 22 2022 at 11:18):Pierre-Marie Pédrot said:
not only finitary, stuff like Σn : nat. n = 0 is also fine.
That's composed only of finitary inductives (finitary != finite)
Paolo Giarrusso (Oct 22 2022 at 12:55):Ooooh! Sigma01 etc is about first-order arithmetic not logic, and that's why you can't say "exists f : nat -> nat. ..."
Paolo Giarrusso (Oct 22 2022 at 12:56):(and yes, I understand quantifying over any sort of syntax for such functions is fine)
Paolo Giarrusso (Oct 22 2022 at 13:01):@Kenji Maillard so I guess in first-order arithmetic you can only quantify over N, and today we can take for granted that adding finitary data types is conservative thanks to Gödelization?
Paolo Giarrusso (Oct 22 2022 at 13:05):IIUC, a signature for a finitary datatype induces a specification, and Gödelization shows that you can implement it using nat as support, and primitive recursive functions for the introduction and elimination arrows?
Paolo Giarrusso (Oct 22 2022 at 13:08):My first guess was "Gödelization implements parsing and printing", but "parsing" can't be a function inside Peano arithmetic; you'd have to compose your functions on inductive type T with the T <-> nat isomorphism, normalize, and prove that T can be completely removed...
walker (Oct 22 2022 at 13:12):I am not sure I understand and the wikipedia isn't making things simpler. :(
Paolo Giarrusso (Oct 22 2022 at 13:14):Sorry, what I just wrote needs context, but you can ignore that
Paolo Giarrusso (Oct 22 2022 at 13:15):Sigma 01 just means a formula in peano arithmetic which can start with "exists a, b, c : nat, ..." and use no other quantifiers
Paolo Giarrusso (Oct 22 2022 at 13:16):if you have other datatypes for "syntax" they can be encoded, but that's the trickier part
Paolo Giarrusso (Oct 22 2022 at 13:16):Does that make sense @walker ?
walker (Oct 22 2022 at 13:19):yes, but how does this form of statements relate to showing that PCUIC can be used as logic?
Paolo Giarrusso (Oct 22 2022 at 13:22):I also wanted to ask! All I can see is that it's good for testing: running such a proof gives me witnesses for the existentials, and a proof of a decidable property.
Paolo Giarrusso (Oct 22 2022 at 13:23):(because quantifier-free properties in Peano arithmetic are decidable?)
Paolo Giarrusso (Oct 22 2022 at 13:25):So if after reduction you get (n, p) : exists n, P n, then you can double-check independently that P n holds.
Paolo Giarrusso (Oct 22 2022 at 13:28):But not sure if this is what @Pierre-Marie Pédrot is thinking about
Pierre-Marie Pédrot (Oct 22 2022 at 21:00):Indeed this is what I had in mind.
Last updated: May 31 2023 at 02:31 UTC