Zulip Chat Archive

Stream: maths

Topic: is continuum hypothesis true in Lean?


Kenny Lau (May 11 2018 at 15:24):

Is the continuum hypothesis true in Lean’s model of ZFC?

Gabriel Ebner (May 11 2018 at 15:39):

I believe that in the set-theoretic model of Lean, the inner model of ZFC is isomorphic to VκV_\kappa where κ\kappa is an inaccessible cardinal in the "outer" model of ZFC. So CH should be independent as usual. You can probably prove the independence in Lean using the typical Cohen forcing.

Kenny Lau (May 11 2018 at 15:40):

it’s a model, it can’t be independent

Gabriel Ebner (May 11 2018 at 15:41):

Oh yes, what you can (directly) prove inside Lean is of course only that CH is independent of ZFC... However CH is still independent of Lean.

Kenny Lau (May 11 2018 at 20:35):

@Gabriel Ebner I mean, we do have a model of ZFC, where "CH" is one specific sentence that can either be true or false

Kenny Lau (May 11 2018 at 20:35):

so I wonder if it is true or false in that specific model of ZFC

Kenny Lau (May 11 2018 at 20:35):

@Mario Carneiro maybe you have some idea

Gabriel Ebner (May 11 2018 at 20:42):

We have a model of ZFC inside a model of Lean inside a model of ZFC (+ some large cardinals); and CH is true in the inner ZFC model iff CH is true in the outer ZFC model. Since we can choose CH or ¬CH for the outer ZFC model, Set⊧CH should be independent of Lean.

Kenny Lau (May 11 2018 at 20:43):

why is CH true in the inner model iff CH is true in the outer model?

Kenny Lau (May 11 2018 at 20:43):

I have a hard time believing your claim, since a model has a valuation making statements either true or false, right?

Kenny Lau (May 11 2018 at 20:43):

things can't be independent in a model

Kenny Lau (May 11 2018 at 20:43):

if a sentence phi is independent of a theory, then phi is true in some models of the theory and false in others

Kenny Lau (May 11 2018 at 20:43):

that's what i'm taught

Gabriel Ebner (May 11 2018 at 20:47):

why is CH true in the inner model iff CH is true in the outer model?

I haven't worked out the details, but I think Set.{u} should be isomorphic to VκV_\kappa for the inaccessible cardinal κ\kappa that we use as the interpretation for Type u (maybe off by one or two universe levels). Then Set.{u} has the same cardinals and real numbers as the outer ZFC model.

Reid Barton (May 11 2018 at 20:47):

Indeed, CH is either true or false in the model. It is true in the model if it is true in the metatheory, and false in the model if it is false in the metatheory.

Kenny Lau (May 11 2018 at 20:47):

hmm...

Kenny Lau (May 11 2018 at 20:48):

I refuse to believe it..

Reid Barton (May 11 2018 at 20:51):

This is assuming we use the interpretation in which t : Type n means t is an element of the universe UnU_n (for some chosen universes U0U1U_0 \subset U_1 \subset \cdots), and a \to b means the set of all maps from the set of a to the set of b, etc.

Kenny Lau (May 11 2018 at 20:52):

can this actually be proved? i.e. if we assume CH outside, can we prove CH inside, and if we assume ¬CH outside, can we prove ¬CH inside?

Kenny Lau (May 11 2018 at 20:52):

or is this one of those things that would take 1000 lines?

Gabriel Ebner (May 11 2018 at 20:53):

can this actually be proved? i.e. if we assume CH outside, can we prove CH inside, and if we assume ¬CH outside, can we prove ¬CH inside?

Neither CH nor ¬CH follows from the axioms of Lean. It is just that CH or ¬CH can be true in different models of Lean.

Kenny Lau (May 11 2018 at 20:53):

assume, meaning have it as a variable

Reid Barton (May 11 2018 at 20:54):

Assuming CH outside isn't going to help you construct any proofs, presumably.

Kenny Lau (May 11 2018 at 20:54):

but you said that if CH is true outside then CH is true inside

Reid Barton (May 11 2018 at 20:54):

I mean, proofs inside the system. It will be true inside the model.

Gabriel Ebner (May 11 2018 at 20:56):

Whether a proposition is provable in Lean is a Σ10\Sigma^0_1-statement, and hence it does not really matter what metatheory you have. The Lean-provable statements are the same whether you work in ZFC, Lean, Coq, PA, or even weaker systems of arithmetic. (Well, assuming consistency.)

Kenny Lau (May 11 2018 at 20:59):

interesting

Gabriel Ebner (May 11 2018 at 21:04):

Essentially, this just means that all these formal systems agree on whether programs terminate on given inputs. (The Lean-provable statements are a computably enumerable set.) In order to represent program execution, you only need a bit of natural numbers. So pretty much every system that has natural numbers and can evaluate addition, multiplication, and comparison for concrete numbers knows exactly what theorems Lean can prove.

Mario Carneiro (May 12 2018 at 00:06):

In lean, you can only "assume CH inside". So if you assume it the proof is trivial by reference to the assumption. In order to "assume CH outside" you would have to do a proof at the meta level, in the outer ZFC system. In this case you would be able to prove a statement like "if CH is true (i.e. true outside), then lean |= CH is true". You will also be able to prove that (lean |- CH) is false (without any CH assumptions), because if lean |- CH then ZFC |- CH, and then you can refer to Godel and Cohen to show that is impossible.

Mario Carneiro (May 12 2018 at 00:09):

(actually if lean |- X then ZFC+inaccessibles |- X, but it is known that large cardinals don't affect the independence of CH.)


Last updated: Dec 20 2023 at 11:08 UTC