model.lean
Model theory formalized in Lean
Link to file: type theory

A language is given by specifying "functions'', "relations" and "constants" along with the arity of each function and each relation. Note that languages are purely syntactic – they have no sematics (i.e. meaning assigned to them).

The words "functions", "relations", and "constant" are written in quotes here to emphasize that these are just the names we give to these pieces of data. We could equivalently have called them F, R, and C. They do not yet behave like actual functions, relations and constants because we have not added any semantic information to them. For now, they are merely symbols in our language.

In lean, we use structure to bundle data (think of it like classes in Python). So, we bundle functions and relations in a structure and call it a language.

Implementation details –

1. Constants are included in the mathematical definition of languages but not in out immediate implementation of lang (see subsection that follows for an explanation).
2. The definition says that every function and relation is supposed to have an arity. In our implementation, we invert this and instead stipulate that every arity (i.e. every natural number) has a type assiciated with it. What type is that? The type corresponding to \((n : ℕ)\) is the type of all \(n\)-arity functions in our language.
3. Thus, \(F : ℕ → Type\) is the function that returns a type for each natural number. Similarly for \(R\).
4. We also note that since each lang contains an F and an R that themselves return types, the type of lang itself is Type 1, which one universe higher than Type. In other words, Type is too small to contain lang, so languages must live in a higher universe. This is a small detail that does not affect the rest of treatment of model theory in any way.

We define the constants in a language to simply be the \(0\)-arity functions i.e. L.F 0. (Think of constants as simply a convenient way to refer to \(0\)-arity functions). They do not add any new information to the lang already defined above.

1. This uses the fact that natural numbers in Lean begin at \(0\), not \(1\).
2. This is the reason why we did not need to include constants in out implementation of languages.

The language that is of primary interest to us is the language of dense linear ordering.

A dense linear ordering (without endpoints) (DLO) is a language containing a single binary relation symbol \((\le)\) satisfying some axioms. The exact axioms are not important at the moment since axioms are semantic statements, while we are interested only in syntactic statements right now.

Thus, a DLO's lang is a language with no constant, no functions and only one binary relation. (Refer to the type theory primer for the meaning of empty, unit etc.).

We can now declare that lang is an inhabited (read: nonempty) type since we know that DLO_lang is a lang. This declaration is made using Lean's instance keyword. This declaration automatically makes the nonemptiness of lang available as a fact to Lean's typeclass resolver if needed.

We can now declare that struc L is an inhabited (read: nonempty) type for every language \(L\). In other words, every language has at least one structure defined on it.

The default value for struc L has –

• a universe/domain with only one element
• corresponding to every symbolic function \(f\) in \(L\), f^M is the function that maps everything to the singleton element.
• corresponding to every symbolic relation \(r\) in \(L\), r̂M is the empty relation.

Given two structures on the same language, an embedding between them is a map that is injective on the universe/domain and preserves the interpretation of all the elements of the language.

For ease of writing, we first introduce some notation. Given a function of arity \(n\) (f : Func α n), and an \(n\)-vector \(v\), we will write \(f\otimes v\) to mean that the function \(f\) is to be applied to the \(n\) elements of \(v\) to yield a value in α.

To start, we let \(L\) denote the language, and \(M\) and \(N\) denote the structures on \(L\). Then the map η : M.univ → N.univ is an embedding –

1. If \(\eta\) it is injective
2. For every \(n\)-vector \(v\) and every \(n\)-arity symbolic function \(f\) in \(L\), we have η(f^M ⊗ v) = f^N ⊗ η(v), where \(\eta(v)\) denotes the vector obtained by mapping every coordinate of \(v\) under \(\eta\).
3. For every \(n\)-vector \(v\) and every \(n\)-arity symbolic relation \(r\) in \(L\), we have v ∈ r̂M ↔ η(v) ∈ r̂N, where \(\eta(v)\) again denotes the vector obtained by mapping every coordinate of \(v\) under \(\eta\).

We argue that every structure has an embedding to itself via the indentity map.

For this embedding, the \(\eta\) map is the identity map on the universe of \(M\). This map is clearly injective and it trivially preserves the interpretation of every function, relation, and constant.

Thus, embedding M M is an inhabited type (read: nonempty), for every structure \(M\).

An isomorphism is a bijective embedding between two \(L\)-structures. To implement this, we define an isomorphism to be a structure in Lean that extends embeddings. This means –

1. there is a natural map to_embedding : isomorphism M N → embedding M N.
2. an isomorphism is the data contained in an embedding bundled with a proof of the bijectivity of the \(\eta\) map.

We argue that every structure has an isomorphism to itself via the identity map.

Thus, isomorphism M M is an inhabited type (read: nonempty), for every structure \(M\).

The cardinality of a structure is defined to be the cardinality of its domain. In Lean, the cardinals are their own separate type which is why we need to "make" the cardinal from the universe of \(M\).

We can then claim that if \(\eta : M \rightarrow N\) is an embedding of \(M\) in \(N\), then the cardinality of \(M\) must be at most the cardinality of \(N\). In other words, only smaller structures can be embedded into larger structures.

The proof hinges on the injectivity of \(\eta\) and follows from the fact cardinal.mk_le_of_injective (which is already proved in mathlib).

\(L\)-Terms are defined inductively as –

• constants of the language are all terms.
• there is a countably infinite supply of indexed "variables", each of which are also distinct terms.
• an \(n\)-ary symbolic function of \(L\) applied to exactly \(n\) other terms also yields a term.

This definition of terms has 2 distinct parts –

1. There are atomic terms like constants and variables,
2. There are higher-order terms (i.e. terms made of other terms) like ones formed by function application.

The trickiest part of the definition of terms is checking that in higher-order terms, an \(n\)-ary symbolic function is being applied to exactly \(n\)-many terms. This check needs a proof of a fact like (length = n). However, we cannot incorporate this proof into the definition directly without running into lean's issues of nested inductive types.

Our solution is to incorporate the notion of atomic/higher-order into our implementation. To each term we associate a level. We start by stipulating that atomic terms have level \(0\). A symbolic function applied to all its arguments also has level \(0\), while a partially applied function has positive level.

We summarize the term to level translation below –

Having defined terms as words in our language, we can then define an interpretation for each word.

Recall that an \(L\)-structure can be seen as a way of interpreting symbolic functions and relations as real functions and relations. This interpretation carries over to terms as well once we define how variables and function application are to be interpreted. A term of level \(n\) is interpreted as an \(n\)-ary function on the universe of \(M\).

We denote the interpretation of term \(t\) under variable assignment \(va\) as t^^va.

An \(L\)-formula on \(L\) is any one of the following "words" on the alphabet \(L \cup \text{Var} \cup \{\top, \bot, =\}\), where Var denotes the set of all variables –

1. \(\top\) and \(\bot\) are formulas
2. \(t_1 = t_2\) is a formula, where \(t_1\) and \(t_2\) are \(L\)-terms.
3. \(r t_1 \ldots t_n\) is a formula, where \(r\) is a symbolic \(n\)-ary relation in \(L\), and the \(t_i\)'s are \(L\)-terms.
4. If \(\phi, \psi\) are \(L\)-formulas, then so are \((\neg \phi)\), \((\phi\wedge\psi)\), and \((\phi\vee\psi)\). Note: we have added parenthesis here merely for ease of writing. They are not really a part of the formula.
5. If \(x\) is a variable, and \(\phi\) is an \(L\)-formula, then \(\exists x \phi\) and \(\forall x \phi\) are \(L\)-formulas.

We implement this definition of an \(L\)-formula inductively by enumerating all the cases. Since we do not have a separate type for variables in our implementation, we simply denote variable \(x_i\) by the natural number \(i\).

We then introduce some notation for logical operators. We mark all symbols with a "prime" in order to distinguish them from Lean's built-in symbols for equality, and, or, not etc.

• vars_in list
• vars_in_formula

A variable occurs freely in a formula if it present outside of a quantification, meaning it occurs in the formula somewhere where it is not immediately preceded by ∃' or ∀'.

We need to be careful with our implementation of this definition because it contains two distinct ideas. A variable occurs freely in a formula if –

1. It occurs in a formula.
2. Some occurrence in the formula is free.

For example, in the formula \(\phi = \neg'(\forall' v_2 \top) \wedge' (v_1 =' v_4)\wedge' (\exists v_3 (v_2 =' v_3))\),

• the variables \(v_1\) and \(v_4\) occur freely in the formula
• the variable \(v_3\) does not occur freely in the formula.
• the variable \(v_5\) does not occur freely in the formula (because it does not occur in the formula at all).
• Surprisingly, the variable \(v_2\) occurs freely in the formula.

A formula in which no variable occurs freely is a sentence. We create a subtype of \(L\)-formulas that we call \(L\)-sentences.

Every sentence is consequently a formula. The explicit map for this can be written as

example : setence L → formula L := λ s, s.val

We wish to always be able to recover the formula underlying a sentence without having to specify the above function explicitly. To do this, we declare a has_coe instance from sentence L to formula L. Thereafter, we can always reference the underlying formula of a sentence s as ↑s.

We now define what it means for a formula to be true in an \(L\)-structure \(M\), or consequently, what it means for a structure \(M\) to model/satisfy a formula.

Let va : ℕ → M.univ be a given variable assignment. We denote \(M\) satisfying the formula \(\phi\) by \(M\models\phi\) and define it inductively as –

• \(M\) always satisfies \(\top'\).
• \(M\) never satisfies \(\bot'\).
• \(M\) satisfies \(t_1 = t_2\) if t₁^^va and t₂^^va match.
• \(M\) satisfies \(r\,t_1\ldots t_n\) if the (t₁^^va, ..., tₙ^^va) is in the set r̂M.
• \(M\) satisfies \(\neg \phi\) if it does not satisfy \(\phi\).
• \(M\) satisfies \(\phi_1\wedge\phi_2\) if it satisfies both \(phi_1\) and \(\phi_2\).
• \(M\) satisfies \(\phi_1\vee\phi_2\) if it satisfies either \(phi_1\), or \(\phi_2\), or both.
• \(M\) satisfies \(\exists v, \phi\) for some variable \(v\) if there exists some \(x\) in the domain of \(M\) such that \(M\) satisfies the formula obtained by replacing all occurrences of \(v\) in \(phi\) by \(x\).
• \(M\) satisfies \(\forall v, \phi\) for some variable \(v\) if for every \(x\) in the domain of \(M\), \(M\) satisfies the formula obtained by replacing all occurrences of \(v\) in \(phi\) by \(x\).