*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?*From*: Matthew Wampler-Doty <negacthulhu at gmail.com>*Date*: Thu, 14 Jan 2010 14:06:00 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <3E85E862-20F0-4ABA-92F1-3BE44D36676F@cam.ac.uk>*References*: <afdf13fb1001131716xfeeba0ehc41b6cb0a3387ae2@mail.gmail.com> <3E85E862-20F0-4ABA-92F1-3BE44D36676F@cam.ac.uk>

Thanks Larry! Well, I am personally interested in the axioms and rules of Isabelle/Pure, since I would like to know how they compare to HOL-Light, the other system which I am familiar. Am I mistaken, or does Isabelle/Pure and all of its extensions ultimately construct objects with a theorem type in SML in a similar fashion to the HOLs? I know this is how HOL-Light functions - the constructor rules are all given in a file thm.ml. If this is how Isabelle functions, I'd be curious to know all the primitive constructors for theorems. Anyway, since my thesis will be given to logicians, I'm sure they'd have other logics they'd be familiar with that they might want to compare Isabelle/Pure's logic to. ~Matthew P. Wampler-Doty On Thu, Jan 14, 2010 at 11:38 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > Isabelle/Pure sets up the logical framework on which logics themselves are defined, so its axioms are no relevance to you unless you were comparing Isabelle/Pure with another logical framework. > > The axioms of Isabelle/HOL can be found by searching for "axioms" and "axiomatization" declarations. Nearly all of them are in the file HOL.thy, and they specify the logical connectives and quantifiers. The axiom of infinity is introduced later, in Nat.thy, and the axiom of choice later still, in Hilbert_Choice.thy. All these will be visible if you work in the theory Main. > Larry Paulson > > > On 14 Jan 2010, at 01:16, Matthew Wampler-Doty wrote: > >> Dear all, >> >> I'm formalizing a completeness theorem for a modal logic my MSc thesis >> in Isabelle/HOL, and I would like to have a section outlining the >> axioms and basic rules Isabelle/HOL (since it's an LCF system after >> all, so there shouldn't be too many of these). I can't seem to figure >> out how to find these out; they appear to be scattered across >> Isabelle/Pure and Isabelle/HOL. Can someone direct me to a listing of >> all the rules and axioms? >> >> Thanks! >> >> ~Matthew P. Wampler-Doty >> > >

**Follow-Ups**:**Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?***From:*Lawrence Paulson

**Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?***From:*Makarius

**References**:**[isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?***From:*Matthew Wampler-Doty

**Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?
- Next by Date: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?
- Previous by Thread: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?
- Next by Thread: Re: [isabelle] What are the Rules and Axioms of Isabelle/HOL Exactly?
- Cl-isabelle-users January 2010 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