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?

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.

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?

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.

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"?

@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

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