[ceh123]

You could state (2) as a contrapositive where your re-phrasing of (2) is:

If A is the set of all primes, then A is an infinite set.

Contrapositive proof: Suppose A is a finite set containing only primes. By (1) we know there exists some p not in A and therefore A is not the set of all primes.

I don't believe contrapositive needs law of excluded middle but I'm honestly not sure. Logic is not my area

[quietbritishjim]

Oops, perhaps I meant proof by contradiction is equivalent to contrapositive (rather than equivalent to law of excluded middle). If you write out a classic high school proof by contradiction formally, then you find yourself basically writing out the contrapositive.

Let's say you know A and ~B=>~A, then you can deduce B. Proof by contradiction: assume otherwise, i.e. ~B, then by ~B=>~A you have ~A, but that contradicts A.

So if you have ~B=>~A then you have A=>B.

[ceh123]

Okay yup, turns out this is correct and it's slightly upsetting to me honestly haha. Just for someone else if they're interested where contrapositive and contradiction both use law of excluded middle (the ==* step requires it):

Contrapositive:

A-> B == A or ~B == ~B or A ==* ~B or ~(~A) == ~B -> ~A

Contradiction:

~(~A and B) == ~~A or ~B ==* A or ~B == A -> B

[housecarpenter]

You might be interested to know that in intuitionistic logic, you still have a one-sided contrapositive law, i.e. (A > B) > (~B > ~A):

  [1] A > B(assumption)
  [2] ~B (assumption)
  [3] A (assumption)
  [4] B (modus ponens on 1 and 3)
  [5] ~A (proof of negation on 3, 4 and 2)

It's only the converse that no longer holds. In general familiar equivalences from classical logic are still valid in intuitionistic logic but only in one direction.