Zulip Chat Archive

Stream: maths

Topic: model completeness of algebraically closed fields


Damiano Testa (Aug 17 2020 at 11:55):

Is it possible to (a) prove that the first order theory of algebraically closed fields is complete (via quantifier elimination or otherwise) and (b) use such a statement/proof to actually deduce things about the complex numbers (or arbitrary algebraically closed fields)?

For instance, I am thinking that Hilbert's Nullstellensatz can be proved quite quickly using quantifier elimination.

Johan Commelin (Aug 17 2020 at 11:57):

Sure, but I don't think that (a) is very easy. It will require quite a bit of prior work.

Adam Topaz (Aug 17 2020 at 11:59):

I do think it would be nice to have some more model theory in mathlib, in general

Damiano Testa (Aug 17 2020 at 12:00):

What about focusing on quantifier elimination? For algebraically closed fields, quantifier elimination and elimination theory are very close and formalizing this might be more at hand?

Damiano Testa (Aug 17 2020 at 12:01):

For instance, is it in theory possible in Lean to prove quantifier elimination by some form of induction on propositions, to show that every proposition reduces to true or false constructively? Is there an "induction on proposition"?

Damiano Testa (Aug 17 2020 at 12:02):

Something along the lines of: a proposition either begins with a \exist or a \forall. in the first case, do something, in the second case, negate, push negations through and repeat

Adam Topaz (Aug 17 2020 at 12:03):

I think unfortunately one has model first order sentences as some kind of inductive type. The closest thing I know of is in the flypitch project

Damiano Testa (Aug 17 2020 at 12:04):

Would working with the first order theory of ACF, possibly make this any easier?

Damiano Testa (Aug 17 2020 at 12:05):

Even just proving something about nested sequences of \exists and \foralls might be a good testing ground

Adam Topaz (Aug 17 2020 at 12:06):

I think with the current stuff from mathlib it would be easier to try to prove the AG formulation a la Chevalley's theorem.

Johan Commelin (Aug 17 2020 at 12:07):

@Damiano Testa Sure this can be done. Flypitch probably did a lot of similar stuff. But right now, there is no definition in mathlib of what it means to be a first order formula in the language of "whatever"

Damiano Testa (Aug 17 2020 at 12:07):

Adam Topaz said:

I think with the current stuff from mathlib it would be easier to try to prove the AG formulation a la Chevalley's theorem.

I was actually trying to get a proof of Chevalley's theorem and this is how I got to this question...

Damiano Testa (Aug 17 2020 at 12:08):

Johan Commelin said:

Damiano Testa Sure this can be done. Flypitch probably did a lot of similar stuff. But right now, there is no definition in mathlib of what it means to be a first order formula in the language of "whatever"

Ok, I do not know what Flypitch is, but I get the idea that this is not a viable approach, at least for the moment!

Adam Topaz (Aug 17 2020 at 12:11):

I think Chevalley's theorem is approachable in lean without going through general stuff about quantifier elimination

Adam Topaz (Aug 17 2020 at 12:12):

The first step would be to formalize constructive sets in the Zariski topology

Adam Topaz (Aug 17 2020 at 12:12):

This would presumably be done as some inductive relation building on top of the Zariski topology.

Adam Topaz (Aug 17 2020 at 12:13):

And inducting on this definition is essentially equivalent to induction on the quantifiers in a given first order formula

Kevin Buzzard (Aug 17 2020 at 12:15):

so you could make constructible sets as an inductive Prop, like the way Alex Best did topology generated by a collection of sets in LFTCM

Adam Topaz (Aug 17 2020 at 12:16):

Yeah that's approximately what I was thinking

Johan Commelin (Aug 17 2020 at 12:16):

@Damiano Testa https://github.com/flypitch/ is a formal verification of independence of the continuum hypothesis. Arguably the biggest milestone that Lean can brag about (-;

Kevin Buzzard (Aug 17 2020 at 12:16):

oh in fact he even did constructible sets:
https://github.com/leanprover-community/lftcm2020/blob/1948bfaf58e3b340b39cd9b8366aa4f13e5ffa7d/src/exercises_sources/wednesday/afternoon/topological_spaces.lean#L117-L122

Adam Topaz (Aug 17 2020 at 12:17):

We need the Zariski topology too

Kevin Buzzard (Aug 17 2020 at 12:17):

that might be there

Adam Topaz (Aug 17 2020 at 12:17):

In the sense of "classical" ag

Kevin Buzzard (Aug 17 2020 at 12:20):

Zariski top on prime spectrum is in algebraic_geometry.prime_spectrum. I guess we might be talking at cross purposes here. I was envisaging that Chevalley's theorem was some statement about finitely presented morphisms of schemes

Adam Topaz (Aug 17 2020 at 12:22):

Oh sure, but the original question was about quantifier elimination in algebraically closed fields, so for that it's just Chevalley's theorem for varieties over the alg. cl field in question

Damiano Testa (Aug 17 2020 at 12:23):

But is the Zariski part of the topology needed much more than just to say this: let R be a ring and c an element of R. The set of all prime ideals containing c is closed and "essentially equal to" Spec R/c, the complement is open and "essentially equal to" Spec R_c?

Damiano Testa (Aug 17 2020 at 12:23):

To go from here to the general case of finite presentation, indeed it is mostly playing around with quasi-compact opens, retrocompactness and complements of finitely generated ideals

Damiano Testa (Aug 17 2020 at 12:26):

(I am thinking of the proof of Chevalley's theorem in the stacks project:
https://stacks.math.columbia.edu/tag/00F5
)

Kevin Buzzard (Aug 17 2020 at 12:27):

yeah that should be fun to do in Lean, it will probably teach you a lot

Damiano Testa (Aug 17 2020 at 12:28):

I am trying to do it, in fact! Ahahaha (But you probably already knew this! ;)

Damiano Testa (Aug 17 2020 at 12:28):

(Anyway, now I am the one who has to go! Bye!)

Kevin Buzzard (Aug 17 2020 at 12:31):

oh this uses the EGA version of constructible, with retrocompact in, so the link to constructible I sent is no good

Kevin Buzzard (Aug 17 2020 at 12:31):

right, I guess it has to use this version because there are no Noetherian hypotheses

Aaron Anderson (Aug 17 2020 at 16:52):

I’m starting to adapt some flypitch to conventions that seem to match the rest of mathlib a little better at a branch, mathlib:fol_project.

Aaron Anderson (Aug 17 2020 at 16:56):

I’m still not particularly close, but I have a definition of definable sets that doesn’t require formulas.

Aaron Anderson (Aug 17 2020 at 16:57):

One thing I noticed is that I couldn’t find a super-suitable definition of the Boolean algebra generated by a particular subset. Perhaps I just need to look again, but I think that’d be useful for defining constructible


Last updated: Dec 20 2023 at 11:08 UTC