Back

@julesh I think that's basically what the Calculus of Inductive Constructions (as used in Coq / Lean) provides.

The syntax only allows recursion on structurally smaller arguments.

Recursion on inductive types is always well-founded and you can define inductive types for a well-foundedness relation, which basically means that all provably total functions are definable.

The syntax ranges from "reasonable" (any obviously structural recursion requires no annotiation) to "custom proof required".

@julesh There is still a gap as far as I understand it: there exist functions that are computable and total but where the totatily cannot be proven inside the same system. This should be a consequence of Gödel's incompleteness.

However, the CIC can represent almost all of math, so I don't know if such functions can exist in practice. How do you "know" that it is total while being unable to prove it?

Like, I think you can prove their existence but never provide an example. (I'm fuzzy on this)

@julesh @artificialmind Oops, you were faster to answer yourself than I was! I'm not sure of the exact construction, but I seem to remember there is a TM that you can write with a low logical power, but whose termination is independent of ZFC. Presumably there's some sort of diagonalisation happening, and a similar argument can be adapted to generate a TM whose termination is independent of your favourite CIC?

@julesh @artificialmind Actually, for CIC, there is a very simple (or at least not too artificial) function: a normaliser for well-typed terms in the language!

@mevenlennonbertrand @julesh Awesome, thanks already for the replies! I'm still trying to wrap my head around why self-evaluation is impossible.

I was under the impression that CICs are quite strong higher-order logics, especially if you add a few axioms for classical reasoning.

Presumably, there are human-understandable proofs that CIC terms are strongly normalizing.

What kind of argument do they use that makes it impossible to encode in classical CIC?

Or is it a Type-in-Type-like issue?

@artificialmind @julesh There are some proofs like this from the 90s, yes, although they typically do not cover all the things we have in today's proof assistants. But in any case, these proofs are typically done in some form of set theory, with adequate assumptions about large cardinals or similar. In essence, they resemble relative consistency proofs from set theory. Although we get a stronger statement, because we are talking about evaluation of functions.

@artificialmind @julesh In principle, these ideas would port over to CIC. However, these proofs seem to use an awful lot of subtle set-theoretic shenanigans, like material inclusion, various strong forms of irrelevance, (ab)using the fact that 2 is closed under arbitrary product in classical logic (which is very useful to interpret impredicative propositions), etc.

@artificialmind @julesh Consequently, afaik the only formalised proof of such a normalisation result for an impredicative theory (Coq in Coq, by Bruno Barras) actually formalises the set-theoretic argument in a set-theory embedded in Coq (!!) rather that conducting the argument in CIC itself.

@artificialmind @julesh For predicative theories, the story is a bit better, but you still need your "meta-theory" to be stronger than your object theory. Out there I know of proofs that rely on (ranked by order of logical power of the meta-theory):
- impredicativity (Wieczorek & Biernacki, and I think also this unpublished one by McGill people https://github.com/Beluga-lang/McLTT)
- induction recursion (Abel, Öhman & Vezzosi)
- more universes (myself and others)

@mevenlennonbertrand @julesh Again thanks a lot for the detailed answers, it really is much appreciated!