What do we mean by "model of Lean"?

Stream: general

[nrs]

Are we using the same notion of model as the one we use when talking about ZFC or theories of arithmetic? In these contexts, a model is a structure that satisfies a collection of sentences, where 'structure' is understood as an interpretation for the symbols for variables, constants, relations, and functions.

If we're using the same concept of model, what is the collection of sentences in question here? i.e. what is the collection of axioms the model satisfies? Is it the valid typing judgments and valid steps in the derivation of typing judgments?

[Trebor Huang]

I'm sure you've read Mario's paper on the type theory of Lean. But for a general and simplified explanation, a type theory can always cast in a form that only involves functions and equations, just like how the axioms of groups involves multiplication (functions) and associativity (equations). This is a special case of first order theories, so the definition of models applies.

But of course much stronger things are true: for example we can take direct products of type theory models just like how we can take direct products of groups, exactly because only equations are involved.

Another caveat is we usually express these using multi-sorted theories. For example in the definition of a module (in commutative algebra), we have two sets R and M, and the scalar multiplication is a map R * M -> M. The model theory for first order multi-sorted theories is essentially the same as the usual model theory you learn, but you just need multiple sets for the interpretation of variables, etc.

For an extremely simple example, a model for a dependent type theory would contain a set Ctx that models the possible contexts, and a set Typ for types. There is an operation ctx : Typ -> Ctx that assigns a type to the context it belongs in. So isOdd n : Prop is sent to the context n : Nat. Then there is a set Term and an operation ty : Term -> Typ. So a typing judgement x : X is expressed as ty(x) = X and can be interpreted in the model.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It is a similar notion, but not quite the same. The kind of 'structure' you mention, with interpretations for functions and relations, is the data of a model of a first-order theory. ZFC and certain theories of arithmetic are all first-order theories. On the other hand, Lean is not a first-order theory but rather a type theory. The definition of model is correspondingly different, though in many ways analogous.

[nrs]

Thank you very much for answers!