Levy hierarchy

Stream: maths

[Violeta Hernández]

Asking this on behalf of a friend: do we have anything in Mathlib about the Levy hierarchy of formulas? Or, do we even have some model theoretic mechanism to talk about formulas currently?

[Yury G. Kudryashov]

Each file in ModelTheory/ has either @Aaron Anderson or @Chris Hughes as a (co-)author.

[Violeta Hernández]

This question is for myself though: what are some good resources for learning model theory that will help me understand Mathlib's model theory library?

[Violeta Hernández]

Usually, knowing a piece of mathematics translates decently well into knowing how to apply it in Lean. But I feel like due to the level of abstraction at play here, model theory is somewhat more subtle.

[Violeta Hernández]

Or, maybe I'm just entirely lost

[Aaron Anderson]

Here's an overview of where to find some relevant things in the model theory library:

• file#Mathlib/ModelTheory/Basic defines languages and structures
• file#Mathlib/ModelTheory/Syntax defines formulas and related concepts. This is where nearly all of the subtlety is that makes things difficult to read, coming from the inductive definition of formulas.
• file#Mathlib/ModelTheory/Semantics interprets formulas in structures. This is where you get to say that a given structure is a model of a given theory.
• file#Mathlib/ModelTheory/Satisfiability defines what it means for a theory, rather than a structure, to model a formula, as well as other useful properties of theories. Universe issues mean that at the moment this requires a bunch of other files containing higher-level concepts, up to the proof of the Löwenheim-Skolem theorem.
• file#Mathlib/ModelTheory/Complexity contains definitions related to quantifier complexity, which is the closest stuff we have to the Lévy hierarchy. We have what it means for a formula to be quantifier-free, or existential, or universal.

[Aaron Anderson]

As far as sources, I have mainly used three:

• the bulk of the subtle stuff about defining formulas is adapted from the flypitch project
• Marker's GTM on Model Theory
• Tent and Ziegler's A Course in Model Theory

[Aaron Anderson]

I have some thoughts on formula complexity hierarchies - there are 3 similar ones that I think it might be worth building a simultaneous API for. Specifically, we start with a particular class (sublattice? sub-boolean algebra?) of formulas that we call Δ0.

• For a general language, these should be quantifier-free formulas
• For the arithmetic hierarchy, in the language of ordered rings, these should be formulas with only bounded quantification
• For the Lévy hierarchy, in the language of set theory, these should be formulas with only bounded quantification (which means something a bit different in that context)

Then we define Σn, Πn, and Δn inductively by closing under quantifiers in the same way.