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



---------- Forwarded message ---------
From: AARON CRIGHTON <crightoa at mcmaster.ca>
Date: Thu, May 30, 2019 at 7:15 PM
Subject: p-adic numbers and model theory in Isabelle
To: <cl-isabelle-users at 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



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