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