Re: [isabelle] Announcement: Isabelle/HOLF


I also like this work, in particular the unifying approach towards the notions of "True" and "False". Up to now, the community has been quite dogmatic in this respect.

2) For some really nasty Isabelle-Hacking, that I do not dare to
reproduce on this list, a lemma of the following form would be nice:
   lemma: "PROP P"

However, my attempt to prove that "by exfalso" failed. Any chance to
extend the proof method such that it also proves this lemma?

The new axiom can only prove valid statements of HOLF. However, your lemma is a statement of Pure, but not HOLF. Embedding a powerful logic in Pure does not make Pure itself more powerful. In fact, the statement above is the single axiom of the even stronger system PureF, which can prove all theorems of HOLF and many more...


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