Re: [isabelle] p-adic numbers and model theory in Isabelle

Dear Aaron,
   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.

Kind Regards,
José M.

Sent from my iPhone

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.