Email Gateway (Aug 22 2022 at 19:45): Email Gateway (Aug 22 2022 at 19:45):From: AARON CRIGHTON <crightoa@mcmaster.ca>
---------- Forwarded message ---------
From: AARON CRIGHTON <crightoa@mcmaster.ca>
Date: Thu, May 30, 2019 at 7:15 PM
Subject: p-adic numbers and model theory in Isabelle
To: <cl-isabelle-users@lists.cam.ac.uk>
Hello everyone,
I am working on a project this summer to formalize some basic results of
p-adic model theory in Isabelle, and have some questions about the best way
to go about some aspects of it.
As far as I can tell, it is not possible to define each p-adic field as a
type in Isabelle, because of the dependence on the prime parameter p.
Instead we have opted to construct the p-adic integers using records, as an
inverse limit of finite rings in the HOL algebra library, and the p-adic
field as the fraction field of the p-adic integers.
Our eventual goal is to prove that the first-order theory of the p-adics in
a certain first order language admits quantifier elimination, but before
doing this we need to decide on a formalism for talking about first-order
languages and interpretations. I understand that one approach is to define
a first-order language recursively as a datatype as is done for Presburger
arithmetic here:
http://isabelle.in.tum.de/~nipkow/pubs/lpar05.pdf
As of now, I'm not sure whether this approach, or defining a record and
locale for general first-order languages and semantics in the style of the
HOL algebra library would be the best approach. My intuition is that the
latter approach would make it easier to develop general facts about
first-order model theory, of which the p-adic example would be a special
case, but perhaps this would also be possible when constructing languages
at the type level as well?
I apologize if my questions aren't completely clear, and I'm happy to
provide more information if that would make it easier to understand my
question.
Best wishes,
Aaron Crighton
Email Gateway (Aug 22 2022 at 19:45):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
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.
https://www.pc.ut.ee/en/jose-manuel-rodriguez-caballero
Sent from my iPhone
Email Gateway (Aug 22 2022 at 19:55):From: Manuel Eberl <eberlm@in.tum.de>
That seems like a reasonable thing to do, although you may want to
consider formalising a generalisation of this instead (e.g. formalising
limits in general and maybe going to the more general setting of a
Discrete Valuation Ring).
By the way, Jeremy Sylvestre is also currently working on a
formalisation of p-adics. If I recall correctly, his idea was not to use
HOL-Algebra but to do it with types. He also wanted to construct the
ring of adeles directly using Laurent series and then carve out p-adics
as needed. I didn't quite understand why he wants to do it that way, but
I don't know much about p-adic numbers.
In any case, if one were not to use HOL-Algebra, it should be fairly
straightforward to construct the type of p-adic numbers in Isabelle
using a similar trick that John Harrison uses to encode n-dimensional
vectors (real ^ 'n) or that René Thiemann et al. used to encode finite
fields of prime characteristic p. One could define e.g. a type 'p adic,
where 'p is a finite type with "p" elements. The main issue with that is
that /using/ this type becomes somewhat painful when the type parameter
p is not fixed but depends on some term. It can be done using Isabelle's
Types-to-Sets mechanism, and Thiemann et al. have done it.
It's not entirely clear to me which way is better. I think I have a
slight preference for following the standard mathematical approach,
which is what you are planning to do – but, as I said, some things might
be fairly easy to generalise, in which case I think they should be
generalised.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 20:02):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Aaron,
as Manuel already indicated, we (Jose, Sebastiaan, Akihisa and myself) did some
formalization with algorithms in GF(p), both via types and via records.
If you’re interested, just write me an email and I can give you access to an
upcoming journal paper where several details on the various formalizations of GF(p)
are described in detail.
Cheers,
René
Last updated: Apr 19 2024 at 08:19 UTC