Re: [isabelle] propositional calculi equivalence

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

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


Hector Villafuerte schrieb:
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
I hope I'm making myself clear. Any pointers would be appreciated.
Thanks in advance,

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