slightly more general / specific versions of Łoś theorem

Stream: Is there code for X?

[Keith J. Bauer]

Right now I see that there is Łoś theorem for individual sentences, but not the easy generalization to theories, and not the specific special case of ultrapowers. I understand these are easy from Łoś itself, and I don't personally need them for anything serious at the moment, but they seem like they would be convenient to have in general.

[Fabian Odermatt]

I can't answer regarding the utility, but if it was the case, did you had in mind to formalize this yourself? I'm looking for a first project and I think I would manage to do that, and I'd be happy to contribute. I don't want to steal it from you, though. Just in case this was more of comment, than a project proposal.

[Keith J. Bauer]

I wouldn't mind if you were to "steal" it from me, primarily because it feels like there's a lot of small things I've noticed about the model theory part of MathLib that could have small additions.

[Snir Broshi]

Keith J. Bauer said:

it feels like there's a lot of small things I've noticed about the model theory part of MathLib that could have small additions.

Just in case you're not familiar with it: #CSLib, https://github.com/leanprover/cslib

[Keith J. Bauer]

Snir Broshi said:

Keith J. Bauer said:

it feels like there's a lot of small things I've noticed about the model theory part of MathLib that could have small additions.

Just in case you're not familiar with it: #CSLib, https://github.com/leanprover/cslib

I wasn't familiar with it, but I'm not sure exactly what the connection is. I do know that FlyPitch was probably the highest-tech model theory in Lean.

[Snir Broshi]

Keith J. Bauer said:

I wasn't familiar with it, but I'm not sure exactly what the connection is.

Isn't model theory a part of CS? It's kinda on the cusp between math and CS, but I believe papers in model theory always come from CS departments.
So I mentioned CSLib since that's where all the model theory people are (probably) at, the model theory in mathlib is from before CSLib was created.

[Yaël Dillies]

I think you have a very specific kind of model theory in mind, Snir! I personally care about model theory, and I don't have a CS background at all.

[Keith J. Bauer]

@Snir Broshi Maybe you are thinking of finite model theory? It has a lot of connections to universal algebra and constraint satisfaction problems, very much CS department topics. When I say "model theory" though I usually refer to infinite model theory.

[Snir Broshi]

https://en.wikipedia.org/wiki/Model_theory
I'm not sure what the distinction between finite and infinite is here (infinite signature maybe?), but I'm including Löwenheim-Skolem in the part I consider CS.
Is the infinite theory more related to set theorists?

[Chris Henson]

I don't think CSLib is relevant here, we do not have any model theory of any variety at the moment.

With regard to terminology, I think both historically and with respect to common usage "model theory" first refered to an area of mathematics (or logic) that later found applications to CS.

[Keith J. Bauer]

Snir Broshi said:

https://en.wikipedia.org/wiki/Model_theory
I'm not sure what the distinction between finite and infinite is here (infinite signature maybe?), but I'm including Löwenheim-Skolem in the part I consider CS.
Is the infinite theory more related to set theorists?

Ah, to clarify, I meant the size of the models in question, i.e. it's common to only care about infinite models because they have a nontrivial notion of elementary equivalence.

[James E Hanson]

Snir Broshi said:

https://en.wikipedia.org/wiki/Model_theory
I'm not sure what the distinction between finite and infinite is here (infinite signature maybe?), but I'm including Löwenheim-Skolem in the part I consider CS.
Is the infinite theory more related to set theorists?

Model theory in the sense that Keith is describing (i.e., my primary field) is historically related to set theory but is also considered a distinct field.

[James E Hanson]

But also I find the idea of Löwenheim-Skolem being primarily a CS thing kind of wild, to be honest.

[James E Hanson]

Formal logic in the context of CS very rarely talks about things like ultraproducts and elementary substructures.

[Snir Broshi]

Very odd, every model theorist I know is in CS, and Löwenheim-Skolem in my uni is only taught to CS majors and not math majors, but I guess that's not a common thing

[Snir Broshi]

I'm also kinda planning on doing a masters near model theory, which is in the CS department

[James E Hanson]

Snir Broshi said:

but I guess that's not a common thing

I don't know how common it is. Logic as a discipline is pretty fragmented.