Classes in Model Theory

Stream: maths

[Aaron Anderson]

I've made several recent PRs adding more model theory to the library, and one of my goals is to prove the existence and uniqueness of Fraisse limits. I have some work to that effect at branch#fraisse_limit.

[Aaron Anderson]

However, I'm not sure what the best formalism is for a Fraisse class.

[Aaron Anderson]

In that branch, so far, I've really used a notion of a Fraisse family, that is, {ι : Type*} (K : ι → Type*) [Π i, L.Structure (K i)].

[Aaron Anderson]

Is this better than considering a Fraisse class as a predicate on structures which is invariant under isomorphisms? The latter seems a little harder to work with, but more honest to my mathematical intuition, and seems more amenable to discussing whether a class of structures is axiomatizable.

[Aaron Anderson]

People who might have opinions: @Patrick Lutz @Floris van Doorn

[Kevin Buzzard]

@Joseph Hua did you see this?

[Floris van Doorn]

I'm not too familiar with the mathematics here, but if the main usage is to construct a new model M out of a collection of existing models K i, then it makes sense to define it as a family of structures as you wrote in your messages.

[Aaron Anderson]

As I've been playing with this, I've realized that even if one starts with a family of structures, one in practice has to reduce everything to the case of a family indexed by nat. Thus I think it using a family doesn't give me the practical advantage I thought, so I may switch to a property.

[Aaron Anderson]

#12138