My first instinct is to translate this post to logic. Obviously A → B doesn’t imply A, because A → B is true when A is false. So we need to expand the problem: imagine we have A → B and some additional knowledge K, and together they imply A. Then it seems to me that K alone, without A → B, would also imply A.
Proof: by definition, (not (A → B)) = (A and not B). Therefore (not (A → B)) → A. Therefore (K and not (A → B)) → A. But we also have (K and (A → B)) → A by assumption. Therefore K → A by case analysis.
So the only thing we can say about K is that it must imply A, and any such K would suffice. The proof only works in classical logic though. What can we say about K if the logic is intuitionistic?
We can see the difference by setting K = ((A → B) → A). Then in intuitionistic logic, K alone doesn’t imply A because Peirce’s law doesn’t hold, but (K and (A → B)) implies A by modus ponens. Moreover, it’s obvious that any other suitable K must imply this one. That wraps up the intuitionistic case: K must imply (A → B) → A, any such K would suffice, and there’s no shorter answer.
Can we exhibit specific A and B for which (A → B) → A holds intuitionistically, but A doesn’t? Yes we can: this stackexchange answer says A = (((P → Q) → P) → P) and B = (P → Q) work. Of course this A still holds classically due to Peirce’s law, but that’s unavoidable.
My first instinct is to translate this post to logic. Obviously A → B doesn’t imply A, because A → B is true when A is false. So we need to expand the problem: imagine we have A → B and some additional knowledge K, and together they imply A. Then it seems to me that K alone, without A → B, would also imply A.
Proof: by definition, (not (A → B)) = (A and not B). Therefore (not (A → B)) → A. Therefore (K and not (A → B)) → A. But we also have (K and (A → B)) → A by assumption. Therefore K → A by case analysis.
So the only thing we can say about K is that it must imply A, and any such K would suffice. The proof only works in classical logic though. What can we say about K if the logic is intuitionistic?
We can see the difference by setting K = ((A → B) → A). Then in intuitionistic logic, K alone doesn’t imply A because Peirce’s law doesn’t hold, but (K and (A → B)) implies A by modus ponens. Moreover, it’s obvious that any other suitable K must imply this one. That wraps up the intuitionistic case: K must imply (A → B) → A, any such K would suffice, and there’s no shorter answer.
Can we exhibit specific A and B for which (A → B) → A holds intuitionistically, but A doesn’t? Yes we can: this stackexchange answer says A = (((P → Q) → P) → P) and B = (P → Q) work. Of course this A still holds classically due to Peirce’s law, but that’s unavoidable.