Ember Edison (Jun 22 2021 at 15:06): Ember Edison (Jun 22 2021 at 15:06):I read PCUICConsistency.v several times.
"PCUIC is consistent" computational interpretation is "PCUIC is soundness + strong normalization"
And wiki say "Σn-soundness has the following computational interpretation: if the theory proves that a program C using a Σn−1-oracle halts, then C actually halts".
So, What computational interpretation will "PCUIC has ω-model""PCUIC has transitive model" have?
Meven Lennon-Bertrand (Jun 23 2021 at 10:02):I am not sure anyone has looked at those, but I think this is because they are quite rooted in first-order logic. This is very different from what PCUIC does, for instance in higher logics such as PCUIC’s, there is not such a thing as non-standard integers in a model.
Ember Edison (Jun 24 2021 at 10:56):Meven Lennon-Bertrand said:
I am not sure anyone has looked at those, but I think this is because they are quite rooted in first-order logic. This is very different from what PCUIC does, for instance in higher logics such as PCUIC’s, there is not such a thing as non-standard integers in a model.
????????????
Do you mean that PCUIC is completeness and PCUIC does not exist non-standard integers model?
Meven Lennon-Bertrand (Jun 24 2021 at 12:07):First note that to go from the incompleteness of a theory (i.e. there exists non-provable statements) to the existence of non-standard models, one needs a notion of completeness (in the sense that statements true in every models are provable), but such a theorem cannot even be stated about CIC, because there is not yet a clear and general notion of models.
However, "non-standard" models of CIC definitely exist : although the general notion of model of CIC or of a standard model are not agreed upon, some constructions would most likely be considered models and are definitely non-standard. I think for instance of https://link.springer.com/chapter/10.1007%2F978-3-319-89884-1_9 , where inductive types all contain a new constructor corresponding to errors. In such models the type nat of natural numbers might, or not, be interpreted by itself. If not, one would get a form of "non-standard" integers.
But those have nothing to do with non-standard models of (first-order) arithmetic. First because first-order logic and higher order logic have quite different notions of model. Second, because a non-standard model of CIC would be more like a non-standard model of ZFC, which is not at all as simple as a non-standard model of arithmetic.
Ember Edison (Jul 11 2021 at 06:54):Meven Lennon-Bertrand said:
but such a theorem cannot even be stated in CIC
Wait. You mean is coq can't proof itself Completeness/Compactness/downward Lowenheim–Skolem Theorem? I always thought that not providing a definition about "unprovable" "undecidable" "incompleteness" "Godel number" was just for philosophical considerations.
But, why ?????? we can say "Canonicity" "Consistency" in PCUIC and can't say "completeness" "incompleteness"?
Paolo Giarrusso (Jul 11 2021 at 14:58):@Ember Edison "such a theorem cannot even be stated in CIC, because there is not yet a clear and general notion of models." <- emphasis added
Matthieu Sozeau (Jul 12 2021 at 08:51):You could consider a fragment of CIC with only Type, then any old MLTT model should apply.
Last updated: May 31 2023 at 04:01 UTC