Re: [isabelle] p-adic numbers and model theory in Isabelle
You could also define the p-adic numbers as the completion of the rational numbers with respect to the topology of a non-Archimedean absolute value (Ostrowski's theorem). The p-adic integers are just the ball of radius 1. This definition is independent of p. Indeed, for your project in model theory the number p is just a distraction: the non-Archimedean property of the norm is the essential feature. In this way, the analogy with real numbers is stronger.
In my own research I am formalizing a functional analysis over the complex numbers, but it would be nice to generalize my results to a algebraic structures over an arbitrary topological field, in order to include the p-adic numbers, e.g., Hilbert snd Banach spaces over the p-adic numbers.
It would be nice to develop a software in order to automatically generalize proofs in Isabelle in cases where the generalization is trivial: the user should only take care when the generalization is non-trivial.
Sent from my iPhone
This archive was generated by a fusion of
Pipermail (Mailman edition) and