## Stream: maths

### Topic: model theory

#### Jalex Stark (May 18 2020 at 23:37):

@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 (May 18 2020 at 23:39):

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 (May 19 2020 at 03:46):

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 (May 19 2020 at 04:19):

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 (May 19 2020 at 04:21):

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

#### Floris van Doorn (May 19 2020 at 04:21):

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 (May 19 2020 at 04:22):

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

#### Jalex Stark (May 19 2020 at 04:22):

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 (May 20 2020 at 01:00):

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 (May 20 2020 at 10:19):

@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 (May 22 2020 at 05:14):

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 (May 22 2020 at 05:34):

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 (May 22 2020 at 16:09):

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 (May 22 2020 at 18:35):

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 (May 22 2020 at 18:51):

@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 (May 22 2020 at 18:55):

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 (May 22 2020 at 18:59):

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 (May 26 2020 at 04:49):

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 (May 26 2020 at 21:59):

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 (May 27 2020 at 06:26):

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

#### Floris van Doorn (May 27 2020 at 18:21):

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 (Jul 05 2020 at 17:17):

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 (Jul 05 2020 at 17:29):

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 (Jul 05 2020 at 17:31):

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 (Jul 05 2020 at 17:32):

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 (Jul 05 2020 at 17:37):

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 (Jul 05 2020 at 17:42):

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 (Jul 05 2020 at 17:43):

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 (Jul 05 2020 at 17:46):

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 (Jul 05 2020 at 17:49):

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 (Jul 05 2020 at 17:50):

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 (Jul 05 2020 at 17:51):

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

#### Aaron Anderson (Jul 05 2020 at 17:53):

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 (Jul 05 2020 at 17:56):

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 (Jul 05 2020 at 17:58):

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 (Jul 05 2020 at 17:59):

Did you see Reid's talk at FoMM 2020?

#### Aaron Anderson (Jul 05 2020 at 18:02):

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 (Jul 05 2020 at 18:03):

I'll definitely fix that today, though.

#### Johan Commelin (Jul 06 2020 at 05:37):

@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 (Jul 12 2020 at 05:37):

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

#### Aaron Anderson (Jul 12 2020 at 05:40):

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 (Jul 12 2020 at 05:40):

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

#### Aaron Anderson (Jul 23 2020 at 22:34):

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 (Jul 23 2020 at 22:35):

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

#### Floris van Doorn (Jul 23 2020 at 22:37):

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 (Jul 23 2020 at 22:38):

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

#### Floris van Doorn (Jul 23 2020 at 22:38):

(like fin_cases)

#### Adam Topaz (Jul 23 2020 at 22:47):

@Colter MacDonald you might find this thread useful!

Last updated: May 11 2021 at 16:22 UTC