other kinds of inductive types

Stream: general

[Kevin Buzzard]

My impression from hearing people talk about inductive types in Lean v in other languages is that there are some things you can do in one system with inductive types that you can't do with another system. In some sense doesn't this represent a major difference in the systems? Is the idea supposed to be that in theory anything you can do in one of these systems you can do in another one a la Church-Turing or is it more complicated?

Couldn't you prove false in Coq relatively recently, maybe because of an issue with an inductive type? Could the same thing happen to Lean? Could someone make some insane inductive type involving a dodgy recursion which the kernel buys but whose existence can't be "justified" -- whatever that means? For example, say its existence immediately implied a contradiction. Is the idea that one could just fix up the C++ and nothing would break because all the inductive types in lean and mathlib are sensible, and that stupid inductive type was exploiting some kind of bug and should never have been allowed to exist anyway.

[Marc Huisinga]

Church-Turing regards computation (for functions N -> N), it doesn't make any statement about type systems. afaik even when considering computability, things start getting more complicated when you consider other notions of computability (e.g. computability at higher type). specifically, i remember this: https://cstheory.stackexchange.com/questions/1117/realizability-theory-difference-in-power-between-lambda-calculus-and-turing-mac

my understanding is that lean's inductive types are relatively "primitive", which enables people like mario to prove the relative consistency of lean, while e.g. systems like agda make these primitives much more powerful. this probably leads to a nicer user experience, but it also makes it way more difficult to prove relative consistency (and apparently, sometimes the resulting systems are not actually consistent, given that there are occasionally proofs of false in some other provers, caused not only by an implementation bug). i'm not sure about coq and its extensions. maybe the proof of false used an extension that is not commonly used in coq?

so the theory of lean is ok, but perhaps the kernel might still be buggy. lean contains this issue by keeping the kernel as small as possible, and in fact there has been no proof of false in lean so far (at least this was the case when i asked sebastian a while back).

i think that if the theory is okay, and there was a bug in the implementation, you could usually fix it without everything "sensible" (whatever that means) breaking, yes.

[Mario Carneiro]

Lean's inductive types are simple-ish, but note that the relative consistency proof needs a bunch of universes over ZFC. The existence of inductive types in isabelle doesn't need this, by comparison

[Mario Carneiro]

When I first learned lean, I was gobsmacked that we have these complicated recursion principles, and no proof of existence, it's just taken for granted

[Mario Carneiro]

It leads to by far the most complicated axiomatic system in current practical usage, and Coq and Agda go further still

[Mario Carneiro]

This coq bug was indeed an issue in the theory, not the implementation, a "dodgy recursion" leading to a proof of inconsistency with classical axioms. It wasn't an outright contradiction, so it lead to a minor existential crisis when the Coq developers weren't sure if they were okay with that or not

[Mario Carneiro]

AFAIK there has still never been a proof of false on trust level 0 using the kernel of lean

[Marc Huisinga]

were there any proofs of false in agda that weren't just bugs in the implementation? i know that there were plenty of bugs that resulted in a proof of false (cf. https://github.com/agda/agda/issues?page=1&q=is%3Aissue+label%3Afalse)

[Mario Carneiro]

this question presupposes that there is such a thing as a "theory of agda"

[Mario Carneiro]

as far as I know, agda is a type theorist playground. The theory is the implementation