Soundness of Lean/CIC

Stream: new members

[Alex Ozdemir]

Hi folks! I've been doing some work with Lean(3) that relies on its soundness (in the sense of "all provable theorems are true"), so I have two (naive) questions:

1. Is Lean believed to be sound?
2. What reference would you recommend for a claim like that (either directly about Lean, or about a similar CIC-based system)?

If it's relevant, I'm thinking only about the theory of Lean/CIC---I'm not concerned about implementation bugs. Also, I'm not particularly choosy about the meaning of "true".

I'd really appreciate any references that you can provide: I'm not at all familiar with the literature here.

[Mario Carneiro]

#leantt answers both of those questions

[Mario Carneiro]

in short: Yes, lean (3) is known to be consistent relative to ZFC + countably many inaccessible cardinals

[Alex Ozdemir]

Thanks for the reference!

A possibly naive question: what is the relationship between soundness and consistency?
(I think of the latter as saying: "For all theorems $t$, I can't prove $t$ and $\neg t$", which doesn't immediately preclude being able to prove the 'wrong' element of $\{ t, \neg t\}$.)

[Mario Carneiro]

More precisely, the proof of consistency is done via a model construction, so you also get soundness (relative to that model)

[Mario Carneiro]

in general soundness is more difficult to discuss in the abstract because it depends on having some kind of model or semantic interpretation of the theory

[Mario Carneiro]

while consistency is more "self-contained"

[Mario Carneiro]

basically, you have to be able to define which one of $\{t,\neg t\}$ is "wrong", and defining that already takes you most of the way through the proof

[Alex Ozdemir]

in general soundness is more difficult to discuss in the abstract because it depends on having some kind of model or semantic interpretation of the theory

while consistency is more "self-contained"

makes total sense

More precisely, the proof of consistency is done via a model construction, so you also get soundness (relative to that model)

I see, so your thesis would prove some notion of soundness for Lean (given a notion of soundness for ZFC+...)?

[Mario Carneiro]

it is a relative consistency proof, or a soundness proof using ZFC + omega inaccessibles as background theory

[Alex Ozdemir]

I think I see.

Thanks for the help, Mario!