I find the difference really really confusing, I know that less assumptions lead to stronger results so:
Goal A -> B) is weaker form of
but what about things like
Goal B -> C and
Goal (A-> B) -> C I find it very confusing when trying to rename the lemmas is the second one a stronger version or weaker version ?
I think most people agree on that if you can derive lemma 1 from lemma 2 (but not the opposite), then lemma 2 is stronger than lemma 1. Then there are usually a bunch of "custom" meanings of logical strength floating around, but popularity seems limited for most.
Last updated: Dec 06 2023 at 15:01 UTC