model theory

Stream: maths

[Jalex Stark]

@Aaron Anderson and I have been talking about doing some model theory in Lean. It seems like the path forward involves PRing some of the basic stuff from the flypitch project into mathlib. Does that seem sane? Has this project already been started? @Floris van Doorn?

[Jalex Stark]

one of the goals of this would be to prove goedel's incompleteness theorem "the right way" (I don't know, Aaron's the model theorist, not me) and knock it off of freek's list

[Aaron Anderson]

I'm largely interested in the transfer principles that flypitch has already stated they want to do at some point. A few concrete examples would be using the theory of real closed fields to prove Hilbert's 17th, and proving Ax-Grothendieck.

[Mario Carneiro]

I'm not sure exactly what you mean by Ax-Grothendieck but if it is what I think then it's not provable in lean

[Reid Barton]

https://en.wikipedia.org/wiki/Ax%E2%80%93Grothendieck_theorem; seems okay to me?

[Floris van Doorn]

Yeah, we've been planning to PR some basic first-order logic from flypitch to mathlib for a while already. We haven't taken much concrete steps yet. I'll work on it soon.

[Mario Carneiro]

heh, I thought Ax meant axiom, as in the Tarski-Grothendieck axiom

[Jalex Stark]

Mario Carneiro said:

I'm not sure exactly what you mean by Ax-Grothendieck but if it is what I think then it's not provable in lean

that's strange. Do you think it's not provable that the complexes are isomorphic to an ultraproduct of a certain sequence of algebraic closures of finite fields?

[Jalex Stark]

Floris van Doorn said:

Yeah, we've been planning to PR some basic first-order logic from flypitch to mathlib for a while already. We haven't taken much concrete steps yet. I'll work on it soon.

I (and probably Aaron) am happy to pitch in. @Floris van Doorn Do you have a private branch? The first step for the branch seems like "copy-paste a few files and get them compiling with current mathlib". I'm happy to start that task if you haven't.

[Matt Earnshaw]

@Luiz Carlos Rumbelsperger Viana has some nice FOL at https://github.com/maxd13/logic-soundness, so far a proof of soundness but also intention for it to serve as a framework. I'm not sure what's at stake in the divergences between their approach to FOL and that of flypitch, and if one or the other is used, it's probably easier to port Luiz's soundness proof to the flypitch encoding than vice-versa. Just mentioning because when reading Luiz's work I thought, "why shouldn't this be in mathlib"?

[Jesse Michael Han]

Aaron Anderson said:

I'm largely interested in the transfer principles that flypitch has already stated they want to do at some point. A few concrete examples would be using the theory of real closed fields to prove Hilbert's 17th, and proving Ax-Grothendieck.

compactness is already there, so what you need for Ax-Grothendieck is a definition of ACF and the fact that it's complete in characteristic 0

i would suggest going the route of showing that ACF admits quantifier elimination, and then using the equivalence of QE with substructure-completeness (it might help if you work in ACF conservatively expanded with symbols for every rational)

[Jesse Michael Han]

if you want to skip the model theory and just get the result, then the more conventional argument for completeness of ACF about uncountable transcendence degrees might be faster

[Aaron Anderson]

That is essentially the approach I'd take. I'd believe that the necessary functionality's all there in flypitch, I just don't have much experience with Lean yet, and Jalex found issues with mathlib compatibility when we started tinkering.

[Jesse Michael Han]

there isn't an API for quantifier elimination; the closest thing is a definition of what it means to be quantifier-free, and an induction on quantifier depth in fol.lean (term_model_ssatisfied_iff) in the proof of completeness for Henkin theories

it might help if you work in ACF conservatively expanded with symbols for every rational

actually, you might even want to add function symbols parametrized by polynomials themselves, which might make it easier to actually show that $\mathbb{C} \vDash \mathsf{ACF}_0$

[Jalex Stark]

@Jesse Michael Han should Aaron and I start PRing to mathlib the stuff we want to use? or have you and Floris secretly started this? I just want to avoid duplicating effort

[Jesse Michael Han]

i'm not working on it and am fine with you guys PRing the stuff you want to use, but @Floris van Doorn might have other plans

[Jesse Michael Han]

definitely coordinate with him on any FOL-related PRs, because he designed the FOL infrastructure and knows what parts of flypitch's to_mathlib supports it

[Floris van Doorn]

I started porting the Flypitch repo to the latest version of Lean/mathlib. It's on this branch: https://github.com/flypitch/flypitch/tree/lean-3.14.0
@Jalex Stark and @Aaron Anderson, if you want I can give you write access if you want to help with that (the files fol.lean and bfol.lean compile, which are the most important to PR).

[Jalex Stark]

maybe a smarter way to break up work is that I'll start a PR putting fol.lean and bfol.lean into mathlib?

[Johan Commelin]

cc @Floris van Doorn @Jesse Michael Han :up:

[Floris van Doorn]

Sounds good! Let's start with fol.lean. There is quite some cleanup to do:

• it doesn't always use mathlib style
• docstrings
• We use stuff from to_mathlib.lean when there is a more canonical way to do something in mathlib. In particular, I would like to use tuples (fin n -> A) instead of dvector A n.

I'm happy to help with this as well.

[Aaron Anderson]

I stepped away from this for checks calendar more than a month just to get my bearings on the library with some more basic projects, and I'm still working on those, but I've started some preliminary experiments to learn flypitch

[Aaron Anderson]

I started by just trying to define the Peano axioms. The alternate symbols made the Robinson's Q axioms a little clunky, but it's not too bad, and probably inevitable.

[Aaron Anderson]

For the induction schema, I'm sure you have enough substitution definitions to pull this off, but to talk about it more naturally, I think we might want a "variable-tuple" to be a fintype, whose elements are variables.

[Aaron Anderson]

For instance, one could define x to be a singleton, y to be a variable-tuple on fin n, define φ to be a formula on variable x ⊕ y, or perhaps a formula on two variable-tuples, x and y.

[Aaron Anderson]

Whatever precisely the formalism, I think what would come most naturally to me is to be able to type the induction axiom for φ as ∀' y ((φ 0 y ⊓ ∀' x (φ x y ⟹ φ (S x) y) ⟹ ∀' x (φ x y))

[Aaron Anderson]

Of course, I have no idea yet if that's technically feasible, but I thought I'd put it on the record.

[Jesse Michael Han]

it is certainly more idiomatic to use finite tuples of variables/constants, and it's important to build that kind of API around the syntactic foundations if serious model theory is to be done

(note that when the theories are multi-sorted, you have to keep track of what sort the variables belong to also)

[Aaron Anderson]

Yeah, at some point, one has to decide whether it's better to make everything fundamentally multi-sorted one-sorted, and I imagine the decision is based around whether it's shorter to type a multi-sorted-to-one-sorted workaround or a one-sorted-to-multi-sorted workaround.

[Aaron Anderson]

Perhaps in a multi-sorted system you can handle the question of variable-tuples by making the cartesian products and powers of "basic sorts" into sorts themselves, and then you can just quantify over M ^ n, but that might make referencing the sub-variables too much of a mess

[Aaron Anderson]

I know that Lou van den Dries would vote for multi-sorted, and he's probably the only model theorist I've ever read who's precise enough in the actual meat of a paper to really get a vote on this...

[Jesse Michael Han]

have you already seen the existing statement of the Peano axioms in flypitch/old/peano.lean?

[Aaron Anderson]

I hadn't, partly because I was trying to see how I naturally would approach it, as I knew we wanted to move away from dvectors to something more mathlib-idiomatic.

[Aaron Anderson]

The rest of the axioms look basically exactly how I thought, and induction doesn't look too complicated, but I'd still be really pleased if I could work directly with variable-tuples as above.

[Aaron Anderson]

Speaking of van den Dries, @Reid Barton @Johan Commelin, I just found out about your o-minimality presentation (project?). That's 100% what I would like to be working on, once I get competent enough at Lean, and potentially also connected to my thesis work. I'd love to hear what you've managed (or what problems have popped up) so far.

[Kevin Buzzard]

Did you see Reid's talk at FoMM 2020?

[Aaron Anderson]

I just found out about it a few minutes ago from the video uploads thread, so all I've done is read the slides so far.

[Aaron Anderson]

I'll definitely fix that today, though.

[Johan Commelin]

@Aaron Anderson I've tried to write some basics, building on flypitch, but it didn't really get anywhere. It would be fun to get back to this!

[Aaron Anderson]

I've just pushed a few preliminary ideas to the folder src/model_theory on mathlib:fol-attempt

[Aaron Anderson]

It's based on some basic flypitch ideas, and everything in it would be really easy to do in flypitch if I understood dvectors etc., but I'm just trying to see what problems I run into with fin n, and get some mwes

[Aaron Anderson]

I've basically just picked the shortest possible route to defining o-minimality

[Aaron Anderson]

Floris van Doorn said:

Sounds good! Let's start with fol.lean. There is quite some cleanup to do:

• it doesn't always use mathlib style
• docstrings
• We use stuff from to_mathlib.lean when there is a more canonical way to do something in mathlib. In particular, I would like to use tuples (fin n -> A) instead of dvector A n.

I'm happy to help with this as well.

@Floris van Doorn Do you have a strong opinion as to whether it should use fin or fin2?

[Aaron Anderson]

I see that fin2 is a lot closer to how flypitch was written

[Floris van Doorn]

I think fin is better, there are functions like docs#fin.tail that will give you most of the dvector operations that are used.

[Floris van Doorn]

I don't think the inductive structure of fin2 is necessary, given some of the tools built around fin.

[Floris van Doorn]

(like fin_cases)

[Adam Topaz]

@Colter MacDonald you might find this thread useful!

[Johan Commelin]

Is anyone planning to add examples of languages/structures to mathlib? I think it would be good if the general theory is developed somewhat in parallel with such concrete examples. It will provide checks and balances on how to build a useful API.
Can we build the language of rings, and somehow connect it to ring?

cc @Aaron Anderson @Floris van Doorn

[Kevin Buzzard]

@Joseph Hua has done this in his MSc thesis https://github.com/Jlh18/ModelTheoryInLean8

[Aaron Anderson]

There is some of this in Flypitch as well, and I have been thinking about it, but there are many other things I'm trying to do at the same time.

[Aaron Anderson]

I can bump it to next on my mental queue.

[Kevin Buzzard]

Joseph uses flypitch (he and Yakov bumped parts of it to work with mathlib master)

[Joseph Hua]

Johan Commelin said:

Is anyone planning to add examples of languages/structures to mathlib? I think it would be good if the general theory is developed somewhat in parallel with such concrete examples. It will provide checks and balances on how to build a useful API.
Can we build the language of rings, and somehow connect it to ring?

cc Aaron Anderson Floris van Doorn

I could quite easily adapt at least the initial setup of my work to the new model theory in mathlib. It's all about the language of rings

[Johan Commelin]

@Joseph Hua That's great! I'm really happy to hear that. Are you planning to PR parts of your work?

[Joseph Hua]

Johan Commelin said:

Joseph Hua That's great! I'm really happy to hear that. Are you planning to PR parts of your work?

It would take a long time, but I could do some parts. I could perhaps start by making some API to convert between different class instances related to various rings and their model-theoretic counterparts. In my current project I have done this for commutative rings and fields, so I could make this a bit more general. The idea is just to make instances of fact (M |= ring_theory) and so on and have nice instances going in between. It's been nice so far because if use this to show comm_ring M and field M and so on, everything works together quite nicely. I can for example take a model of ACF and automatically have it as a commutative ring and field etc, all compatible instances.

[Aaron Anderson]

Your work looks quite good - I think it's worth PRing. We can discuss how to split the work of adapting it to my modified formalism.

[Aaron Anderson]

A few ideas occur to me now:

• I can make it so that M |= ring_theory is a class instance, without the need for fact
• We could put in the example of Rings first, but I think that there should be classes for "a language with +" and "a language with *" that lead directly to has_add and has_mul instances on terms.
• Perhaps to work out some of my design issues independently of your algebra work, I can work on orders and graphs. If I define ordered structures, and #12611 goes through, then I can define o-minimality.

[Joseph Hua]

the first two points look like great ideas. As for the third, do you mean I should wait until you iron out any problems with the current setup before starting to make ring related PRs? By the way, I noticed that you chose to go with the usual definition of terms, rather than the de Bruijn-like definition from flypitch - is this working out well? I also noticed you didn't introduce notation for terms and bounded formulas, will this be added soon?

[Aaron Anderson]

I am adding some of that Flypitch notation in #12630 - let me know if there’s other notation I’m missing

[Aaron Anderson]

You can make ring-related PRs as soon as you want to, and if you find problems with my setup, you can let me know.

[Joseph Hua]

If I understand correctly the de Bruijn way of defining terms makes induction easier, since we only introduct a single term at a time in the induction, rather than n of them at once