*To*: Tomás( Beránek <tom at logici.cz>*Subject*: Re: [isabelle] formalization of non-classical logic in hilbert style*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 11 Feb 2011 08:06:04 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTimZYxpF5P=NGoo3RnJf=ti+7gSNYqfb5=+TmnGU@mail.gmail.com>*References*: <AANLkTimZYxpF5P=NGoo3RnJf=ti+7gSNYqfb5=+TmnGU@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

> My first decision was to prove many natural deduction rules which I then > would provide to Isabelle's simplifier, but I think the simplifier is also > ment for natural deduction style proofs and thus it would be useles in this > case (?) (without some coding on the ML level). If you can prove the necessary rules to set up the simplifier, it will certainly be useful. The only bit of ML code involved is in simpdata.ML, and you can modify the existing one. > Then I got the idea to formalize the whole logic inside HOL since the > meta-level of this logic is classical and HOL has many tools already set > up). But here I am not sure if the HOL's tools (like the simplifier) > wouldn't affect proving in my logic somehow unintentionally (turning some > unprovable goals into provable ones etc.). Neither the simplifier nor any other proof tool can prove unprovable thms. Any theorem is proved by the rules that you provide. That is, if you state "(P<->Q) ==> (P==Q)" to get the simplifier going for <->, you must make sure that this is an admissible rule. > [Actual question] > Now I am not sure if it is wise to continue writing completely new logic > based on Pure and setting the simplifier to fit this logic or if it would be > better (or at least possible) to make this formalization inside HOL. If you want to make deductions merely in the logic, it is fine to set it up separately. If you do it inside HOL, it should be done as an inductive definition of provability, and then you can also prove theorems about provability. That is the more powerful approach. Tobias > I add that this logic should later serve to formalization of Fuzzy Class > Theory <http://www.mathfuzzlog.org/index.php/Fuzzy_Class_Theory>. > > The first attempt of the formalization is in the attached file. I am aware > that the proofs are very bad, I am still learning how proving in Isabelle > really works... > > Thanks for any advice, I will gladly provide more precise information if > needed. > > Regards > > Tomas Beranek

**Follow-Ups**:**Re: [isabelle] formalization of non-classical logic in hilbert style***From:*Tomáš Beránek

**References**:**[isabelle] formalization of non-classical logic in hilbert style***From:*Tomáš Beránek

- Previous by Date: Re: [isabelle] Presenting theories without running a session
- Next by Date: Re: [isabelle] String.explode in generated code
- Previous by Thread: [isabelle] formalization of non-classical logic in hilbert style
- Next by Thread: Re: [isabelle] formalization of non-classical logic in hilbert style
- Cl-isabelle-users February 2011 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