## Stream: new members

### Topic: Soundness of Lean/CIC

#### Alex Ozdemir (Apr 11 2023 at 00:17):

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 (Apr 11 2023 at 00:19):

#leantt answers both of those questions

#### Mario Carneiro (Apr 11 2023 at 00:20):

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

#### Alex Ozdemir (Apr 11 2023 at 00:24):

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 (Apr 11 2023 at 00:28):

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

#### Mario Carneiro (Apr 11 2023 at 00:29):

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 (Apr 11 2023 at 00:30):

while consistency is more "self-contained"

#### Mario Carneiro (Apr 11 2023 at 00:30):

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 (Apr 11 2023 at 00:31):

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 (Apr 11 2023 at 00:32):

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

#### Alex Ozdemir (Apr 11 2023 at 00:34):

I think I see.

Thanks for the help, Mario!

Last updated: Dec 20 2023 at 11:08 UTC