arXiv subjects
Publications and source records attributed to Sven Manthe.
We present a formalization of Borel determinacy in the Lean 4 theorem prover. The formalization includes a definition of Gale-Stewart games and a proof of Martin's theorem stating that Borel games are determined. The proof closely follows Martin's "A purely inductive proof of Borel determinacy".
The monadic theory of $(\mathbb R,\le)$ with quantification restricted to Borel sets is decidable. The Boolean combinations of $F_\sigma$ sets form an elementary substructure of the Borel sets. Under determinacy hypotheses, the proof extends to larger classes of sets.
Let $α,β\in \mathbb{R}_{>0}$ be such that $α,β$ are quadratic and $\mathbb{Q}(α)\neq \mathbb{Q}(β)$. Then every subset of $\mathbb{R}^n$ definable in both $(\mathbb{R},{<},+,\mathbb{Z},x\mapsto αx)$ and $(\mathbb{R},{<},+,\mathbb{Z},x\mapsto βx)$ is already definable in $(\mathbb{R},{<},+,\mathbb{Z})$. As a consequence we generalize Cobham-Semenov theorems for sets of real numbers to $β$-numeration systems, where $β$ is a quadratic irrational.
Let $E$ be a two-dimensional étale algebra over a non-Archimedean local field $K$ of characteristic zero. We show that the unitary group of a non-degenerate hermitian lattice over $E$ is generated by symmetries and rescaled Eichler isometries. In the appendix we show that unless $E/K$ is a ramified dyadic field extension and the residue field has two elements, symmetries suffice.