[bubblyworld]

Not my area at all, but surely you would just add the relevant induction schema as an axiom? Are nonstandard models relevant to proof assistants?

(to be clear - I know what nonstandard models are and how they work, and I've mucked around in coq/lean, just wondering why it matters to a proof assistant)

[agalunar]

My line of thinking roughly was, "each type system corresponds to a particular logic system and vice versa; in a proof by induction, the different cases correspond to the type constructors, but what does the necessary axiom schema or second-order axiom of induction correspond to? (in order to avoid the problem of nonstandard elements). And proof by infinite descent seems to require something other than induction, so where does well-foundedness come from?"

I realize these questions may not even be posed sensibly; maybe the answer is as simple as, "the naturals are defined constructively here; of course they are the naturals and therefore are well-founded". As I said, it's been a while, so things are hazy in my mind.

[bubblyworld]

I see, that's interesting. You inspired me to go read up about CIC, it's really cool, thanks! And in hindsight I realise my reply was totally wrong anyway haha.