# Re: [isabelle] propositional calculi equivalence

• To: Larry Paulson <Larry.Paulson at cl.cam.ac.uk>
• Subject: Re: [isabelle] propositional calculi equivalence
• From: Tobias Nipkow <nipkow at in.tum.de>
• Date: Tue, 01 Apr 2008 12:50:11 +0200
• References: <350f72300803310747k68fd9d8dw259c12aa17fb43fc@mail.gmail.com>
• Resent-date: Tue, 1 Apr 2008 12:18:50 +0100
• Resent-date: Tue, 01 Apr 2008 12:18:51 +0100
• Resent-from: Lawrence Paulson <lp15 at cam.ac.uk>
• Resent-message-id: <E1JgeVv-0001f4-3K@ppsw-1.csi.cam.ac.uk>
• Resent-to: isabelle-users at cl.cam.ac.uk

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:
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.