Email Gateway (Aug 18 2022 at 17:15): Email Gateway (Aug 18 2022 at 17:15):From: Tomáš Beránek <tom@logici.cz>
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
MTL_Delta.thy
Email Gateway (Aug 18 2022 at 17:15):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 18 2022 at 17:16):From: Tomáš Beránek <tom@logici.cz>
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.
Tomas
Email Gateway (Aug 18 2022 at 17:16):From: Makarius <makarius@sketis.net>
There are some (outdated) explanations in
http://isabelle.in.tum.de/dist/Isabelle2011/doc/ref.pdf
section 9.7 "Setting up the Simplifier".
In src/Pure/simplifier.ML there is also an easy_setup function that should
give an idea how the minimal setup works.
Makarius
Last updated: Apr 26 2024 at 01:06 UTC