Re: [isabelle] formalization of non-classical logic in hilbert style

Thank you for your help, Tobias.

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.
> 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.
 I will maybe ask more questions about this subject, because although I have
some basic understanding of ML, I still cannot understand the code
completely (even the simpdata.ML). For now I will continue proving the
necessary rules.

> 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.
This topic I will have to discuss with my supervisor, but I think, the
proving about provability will also be necessary in the theory FCT which
will be based on the MTL logic. Now I take a deeper look in the HOL tutorial
on inductively defined sets to see if I can figure out how to define the
notion of provability inductively.

Thanks again.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.