model theory

Stream: general

[Johan Commelin]

Model theory is a field of mathematics that I know very little about but that can sometimes have very surprising applications. I'm now actually learning some of this stuff because there are applications in Hodge theory.

If I understand things correctly, the Flyspeck project must have formalised quite a bit of the basics of formal logic. On the other hand, we have omega which must also deal with first order formulas etc...

Would it be worth it to generalise a bunch of stuff? If I understand things correctly, model theory can be used as a way to crank out a bunch of tactics that will help us prove stuff.

[Jesse Michael Han]

what sort of tactics do you have in mind?

maybe a first_order_transfer sort of thing, e.g. proving something in the hyperreals, automatically constructing a reification of the proven theorem as a first-order sentence, and then re-interpreting it in the reals?

[Johan Commelin]

To give a concrete example: when developing the theory of Witt vectors you have a commutative ring R and a thing W(R) called "the Witt vectors of R", depending on a prime number p. Now there are a whole bunch of lemmas that you want to prove about W(R) that are usually proven as follows in math texts:
"It suffices to check this when p is invertible in the ring R, and then the statement is obvious."
(Whether or not the statement becomes obvious if p is invertible is not important. I'm interested in the first step of that proof.)
One example of such a lemma is "W(R) is a commutative ring". Most authors never explain why this strategy works, but I think that in almost all examples the claim in the lemma is a universal formula in the language of rings. Now W(mv_polynomial int R) surjects onto W(R) and W(mv_polynomial int R) injects into W(mv_polynomial rat R). And mv_polynomial rat R is a ring where p is invertible. So model theory says that it suffices to check universal formulas for that special case (because of substructures and homomorphic maps and blah...)

I would be very interested in knowing if it is conceivable that we could set up generic model theory so that it becomes easy to crank out little mini helper tactics that make the beginning of these proofs ("It suffices to check the statement when p is invertible in R") into one line steps in the Lean proofs.

[Johan Commelin]

@Jesse Michael Han Yes, that sounds like a similar thing.

[Johan Commelin]

And instead of all such tactics requiring to set up a whole bunch of framework, I would want there to be some lemma real_closed_fields_complete or something like that. This lemma should not be meta, and then a generic tactic that turns this lemma into a mini-helper tactic that you can apply.

[Johan Commelin]

Of course if you have lemma Presburger_complete then this does not mean that you some can crank out omega. Because I guess omega does lots of smart things under the hood. (Instead of just enumerating sentences and checking if it produced a proof by chance.)

[Johan Commelin]

But there might still be room for a lot of shared framework.

[Jesse Michael Han]

So model theory says that it suffices to check universal formulas for that special case (because of substructures and homomorphic maps and blah...)

this also gives a cute proof that to check non-singularity of a matrix one can compute its determinant in a larger ring of coefficients

[François G. Dorais]

The lemma real_closed_fields_complete is called the Tarski-Seidenberg Theorem.

https://en.wikipedia.org/wiki/Tarski%E2%80%93Seidenberg_theorem

The details of the decision algorithm are in Jacobson's Basic Algebra, for example.

[Jesse Michael Han]

Of course if you have lemma Presburger_complete then this does not mean that you some can crank out omega.

in principle, such a lemma would use a computable def where one describes the decision procedure, and one could conceive of a horrifyingly slow tactic where things in the scope of omega are reified to Presburger formulas and then processed by the decision procedure

[Johan Commelin]

Exactly... so for something like omega you still need other optimizations. But for the other applications you need a tactic that takes a language L and checks that the goal is a first order formula in L and then applies some lemma model_theory.cool_lemma.

[Johan Commelin]

There is necessarily some meta involved at some point. But I think it can be very little. Mostly the phase of "inspecting the goal to check that it is a first order formula". I don't think that you can avoid meta there.

[Johan Commelin]

The lemma real_closed_fields_complete is called the Tarski-Seidenberg Theorem.

https://en.wikipedia.org/wiki/Tarski%E2%80%93Seidenberg_theorem

The details of the decision algorithm are in Jacobson's Basic Algebra, for example.

Right. So I wouldn't want to autogenerate a tactic that applies quantifier elimination. But I would like a tactic that allows me to transform https://en.wikipedia.org/wiki/Hilbert%27s_seventeenth_problem for a certain non-negative polynomial f into the analogous claim over the real closed field that has a bunch of indeterminates adjoined. "And then the statement is obvious".

[Johan Commelin]

And I feel like such a tactic can be autogenerated from Tarski_Seidenberg + model_theory.structural_lemma_1 and model_theory.structural_theorem_2 or something like that.

[Johan Commelin]

But like I said... I actually know very little about model theory, and I would be very happy to hear opinions from some experts.

[Jesse Michael Han]

Mostly the phase of "inspecting the goal to check that it is a first order formula".

the "inspection" hides a bunch of computation, as usual: one would probably use typeclass resolution to infer a first-order structure on the type being quantified over and also on the type one wants to work in instead, and also construct the formula, re-interpret it in the other type, remove the syntactic clutter from the reinterpretation, and prompt the user for a proof of the transferred statement

[Johan Commelin]

Exactly!

[Johan Commelin]

But that sounds like a very generic thing to do. In my formalization of Witt vectors, I hand-rolled the statements that I need for rings. But I'dd rather just do it for all theories in one go and apply a meta-meta theorem wherever needed.

[Kevin Buzzard]

@Abhimanyu Pallavi Sudhir formalised the hyperreals in Lean recently, and I know that he was thinking about this transfer principle but I'm pretty sure he wasn't thinking about it in meta land. I see now that this is somehow what he could do next.

[Jesse Michael Han]

i was playing around with something like this in Flypitch a while ago; see parse_formula.lean (link), where toy examples of Lean expressions are parsed into deeply-embedded FOL formulas

[Jesse Michael Han]

there's also a toy example of "reflection" for abelian groups worked out by hand here. (this example is kind of stupid because the proof which i'm reflecting was generated by using the completeness theorem to turn a Lean proof into a FOL proof, so that I could turn it back into the same Lean proof, but in principle the starting Lean proof could be different from the ending Lean proof, as envisioned by Johan)

[Seul Baek]

My general impression is that the optimal semantics to formalize varies significantly depending on the objective, so there isn't much mileage you'd get out of having a universal framework. For instance, the definition of models for the Vampire interface (https://github.com/skbaek/mathlib/blob/vampire/src/tactic/vampire/model.lean) makes no distinction between functions/relations and assigns no fixed arities, which is probably not the best choice for formalizing model theory for its own sake.

[Jeremy Avigad]

Johan's initial application is just an instance of transfer, and there the model theory doesn't help much. If I understand correctly, there is a function f from W(R) to W(whatever) that preserves the meaning of atomic formulas, and hence the quantifier-free ones. So, from all x, P x on W(whatever), we get all y, P (f y), where y ranges over W(R), and then transfer should tell us that P(f y) is equivalent to P y. Many model-theoretic arguments translate to syntactic arguments of this kind, and, conversely, lots of syntactic procedures (like decision procedures) are understood in model-theoretic terms.

Given a first-order statement in the language of ordered rings that is true of the reals, a more serious (and noneliminable) use of model theory could conclude, for free, that the statement is true of every real-closed field -- and, hence, even provable from the axioms for a real-closed field (without explicitly exhibiting such a proof!). I don't know of we have any pressing application of that.

Of course, model theory is an interesting branch of mathematics in its own right, and well worth formalizing.

So, I guess my answer to Johann is that, well... it depends on what you want to do.