*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] formalization of non-classical logic in hilbert style*From*: Tomáš Beránek <tom at logici.cz>*Date*: Thu, 10 Feb 2011 19:28:08 +0100

Hi, my task is to explore possibility of formalisation of a logic in Isabelle/Isar, which is weaker than logics that are already formalised in Isabelle. For now I only need a first-order variant (higher orders will be needed later) of an alternative to MTL<http://en.wikipedia.org/wiki/Monoidal_t-norm_logic>. This formalisation should be in Hilbert style (some axioms and one MP rule). I already tried to create the theory by taking the IFOL.thy and editing the connectives definitions and axioms according to my needs. Then I was able to prove some basic theorems but it came out it is quite difficult to write and hard to read these proofs since Isabelle's Pure is based on natural deduction and these proofs are in Hilbert calculus. 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). 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.). [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. 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

**Attachment:
MTL_Delta.thy**

**Follow-Ups**:**Re: [isabelle] formalization of non-classical logic in hilbert style***From:*Tobias Nipkow

- Previous by Date: [isabelle] Babel-17 v0.21.1 now available
- Next by Date: Re: [isabelle] String.explode in generated code
- Previous by Thread: [isabelle] Babel-17 v0.21.1 now available
- 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