I find the difference really really confusing, I know that less assumptions lead to stronger results so:

(`Goal A -> B`

) is weaker form of `Goal B`

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: Jun 05 2023 at 10:01 UTC