model completeness of algebraically closed fields

Stream: maths

[Damiano Testa]

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]

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

[Adam Topaz]

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

[Damiano Testa]

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]

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]

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]

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]

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

[Damiano Testa]

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

[Adam Topaz]

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]

@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]

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]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

Yeah that's approximately what I was thinking

[Johan Commelin]

@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]

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]

We need the Zariski topology too

[Kevin Buzzard]

that might be there

[Adam Topaz]

In the sense of "classical" ag

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Aaron Anderson]

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]

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

[Aaron Anderson]

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