Model theory

Which pairs of structures (each in the language $\{<\}$) are elementarily equivalent? Choose all that apply.

Using the rule for Ehrenfeucht–Fraïssé games on finite linear orders, what is the least $m$ such that the linear orders with $m$ and $m + 1$ elements satisfy the same sentences of quantifier rank at most $4$?

In the inductive proof of Łoś's theorem, which step is the only one that uses that $U$ is an ultrafilter (and not merely a filter)?

The key lemma says: in a DLO, $\exists x\,(\bigwedge_{a \in A} a < x \wedge \bigwedge_{b \in B} x < b)$ is equivalent to $\bigwedge_{a \in A, b \in B} a < b$. In $(\mathbb{Z}, <)$ the equivalence fails for $A = \{0\}$, $B = \{1\}$. Which axiom of DLO does $\mathbb{Z}$ violate that the proof used here?

To show that $\varphi(a, b) = \exists x\,(a < x \wedge x < b)$ is not equivalent in $(\mathbb{Z},<)$ to any quantifier-free formula in $a, b$, which pair of inputs works?

With orderStructure ℚ and orderStructure ℝ as the structures, which Lean statement correctly formalises “$(\mathbb{Q}, \le)$ and $(\mathbb{R}, \le)$ are elementarily equivalent but not isomorphic”?

The Ax–Grothendieck theorem says injective polynomial maps $K^n \to K^n$ are surjective when $K$ is algebraically closed. Which of these are counterexamples over a field that is not algebraically closed? Choose all that apply.

How many complete $2$-types over $\emptyset$ does the theory DLO have? (Use quantifier elimination: a type in variables $x, y$ is determined by the atomic formulas it contains.)

Make the key lemma constructive in $\mathbb{Q}$. Write witness(lows, highs) that takes two lists of Fractions and returns a Fraction $x$ with $a < x$ for every $a$ in lows and $x < b$ for every $b$ in highs, or None if no such $x$ exists. Follow the four cases of the proof.