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)?
Your point 4. is unrelated to the TCB, it's a foundational regression ad infinitum.
In theory you could prove that CIC has all the good metatheoretical properties on paper in ZFC + ω universes
but this does not affect the code
As for the other points:
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.
if it converges, you're fine, otherwise just wait a bit more.
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.
Typical sources of concern of mine: Prop, the guard condition, modules
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 ?
this is probably the best you can find publicly: https://github.com/mr-ohman/logrel-mltt
I am sure what is Σ01 formulae
If you're not sure, I understand https://en.wikipedia.org/wiki/Arithmetical_hierarchy is relevant
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 $\Sigma^0_1$ formula I automatically translate that in my head into "plain finitary inductive data-types" (that do not involve functions for instance).
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" ...
not only finitary, stuff like Σn : nat. n = 0 is also fine.
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)
Ooooh! Sigma01 etc is about first-order arithmetic not logic, and that's why you can't say "exists f : nat -> nat. ..."
(and yes, I understand quantifying over any sort of syntax for such functions is fine)
@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?
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?
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...
I am not sure I understand and the wikipedia isn't making things simpler. :(
Sorry, what I just wrote needs context, but you can ignore that
Sigma 01 just means a formula in peano arithmetic which can start with "exists a, b, c : nat, ..." and use no other quantifiers
if you have other datatypes for "syntax" they can be encoded, but that's the trickier part
Does that make sense @walker ?
yes, but how does this form of statements relate to showing that PCUIC can be used as logic?
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.
(because quantifier-free properties in Peano arithmetic are decidable?)
So if after reduction you get (n, p) : exists n, P n
, then you can double-check independently that P n holds.
But not sure if this is what @Pierre-Marie Pédrot is thinking about
Indeed this is what I had in mind.
Last updated: May 31 2023 at 02:31 UTC