Feferman–Vaught

Stream: maths

[Keith J. Bauer]

Has Feferman–Vaught been formalized yet? It's the generalization of Łoś theorem to reduced products instead of ultraproducts. As motivation for this question, Łoś is already in mathlib.

[Keith J. Bauer]

Here are some relevant informational links:
Wikipedia article on Łoś: https://en.wikipedia.org/wiki/Ultraproduct#%C5%81o%C5%9B's_theorem
Mathlib resource that uses Łoś: https://leanprover-community.github.io/mathlib4_docs/Mathlib/ModelTheory/Ultraproducts.html
Wikipedia article on Feferman-Vaught: https://en.wikipedia.org/wiki/Feferman%E2%80%93Vaught_theorem

[Johan Commelin]

I don't know for sure, but my guess is that it hasn't been done yet.
@Aaron Anderson are you aware of anything?

[Aaron Anderson]

No, I don't believe anyone's tried that in Lean.

[Aaron Anderson]

To actually state Feferman-Vaught, one needs to either use Boolean-valued models, which were formalized in the Flypitch project https://flypitch.github.io/ but which haven't been ported to mathlib, or simulate them as two-sorted structures.

[Aaron Anderson]

This latter approach would require an understanding of boolean algebras themselves as first-order structures - this file is as far as we've gotten towards describing ordered structures in a first-order way in mathlib https://leanprover-community.github.io/mathlib4_docs/Mathlib/ModelTheory/Order.html

[Keith J. Bauer]

Should I consider contributing to the FlyPitch project, so I don't have to worry about porting existing code for model theory to Mathlib?

[Keith J. Bauer]

*Flypitch (as opposed to contributing to mathlib)

[Aaron Anderson]

The only thing that I mentioned Flypitch for is their treatment of Boolean-valued models, which are conceptually related to Feferman-Vaught.

[Aaron Anderson]

I think you're probably better off just defining the first-order theory of boolean algebras, and finding some way to express F-V in terms of that, in up-to-date mathlib.

[Aaron Anderson]

Most of Flypitch has not been updated in ages, and it's a project specifically of @Floris van Doorn and @Jesse Michael Han , so I don't know that contributing to it really makes sense as an option, even if you did want to use their definition of Boolean-valued models.

[Keith J. Bauer]

Oh, alright. I will focus on mathlib then.

[Floris van Doorn]

I agree with Aaron.
Flypitch might be a useful source of information for design decisions or guidance, but you should not make contributions to it. Porting our definitions over to Lean 4 and continuing working on it afterwards is of course welcome.