Re: [isabelle] formalization of non-classical logic in hilbert style
> 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.
> 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
> Tomas Beranek
This archive was generated by a fusion of
Pipermail (Mailman edition) and