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



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
Description: Binary data



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