Email Gateway (Aug 18 2022 at 11:38): Email Gateway (Aug 18 2022 at 11:38):From: Hector Villafuerte <hectorvd@gmail.com>
Hi,
I just came to Isabelle after having learnt some functional
programming through SML. Now I'm teaching myself some mathematical
logic (back to the foundations!). My question is: how to use Isabelle
to establish the equivalence of different propositional calculi, say
Hilbert-style vs. LK sequent calculus (restricted to propositional
logic)?
I hope I'm making myself clear. Any pointers would be appreciated.
Thanks in advance,
Email Gateway (Aug 18 2022 at 11:38):From: Tobias Nipkow <nipkow@in.tum.de>
You can find a simple example of a formalized logic with completeness
theorem in HOL/Induct/PropLog (in the distribution) and a larger one in
http://afp.sourceforge.net/entries/FOL-Fitting.shtml
This is not quite what you asked for, but the same techniques can be
used to relate different calculi. Just make sure that you formalize your
logics inside a logic that has induction, eg HOL. Do NOT formalize them
as Isabelle object logics, because Isabelle's meta logic does not have
induction (and is not meant to formalize the relationship between
different calculi).
Tobias
Hector Villafuerte schrieb:
Last updated: May 03 2024 at 04:19 UTC