*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Fwd: p-adic numbers and model theory in Isabelle*From*: AARON CRIGHTON <crightoa at mcmaster.ca>*Date*: Thu, 30 May 2019 19:20:56 -0400*In-reply-to*: <CAFUz6AhOKTE8MBXvZsbW7pE_s5V=u768rziS18wzfbS81DwV9w@mail.gmail.com>*References*: <CAFUz6AhOKTE8MBXvZsbW7pE_s5V=u768rziS18wzfbS81DwV9w@mail.gmail.com>

---------- 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

- Previous by Date: Re: [isabelle] Isabelle2019-RC2: Cannot get exception trace
- Next by Date: Re: [isabelle] Isabelle2019-RC2: Cannot get exception trace
- Previous by Thread: [isabelle] Call for Participation - Workshop on Large Mathematical Libraries (LML 2019)
- Next by Thread: Re: [isabelle] p-adic numbers and model theory in Isabelle
- Cl-isabelle-users May 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list