Which of the following statements is true regarding the relationship between the Law of Excluded Middle (EM) and Reductio ad Absurdo (RAA)?

Question

Accepted Answer

They are logically equivalent and EM can be used to derive RAA.

Answer

Lean's standard library includes RAA as a primitive tactic, but EM must be imported.

Answer

EM is used for constructive proofs, while RAA is used for non-constructive proofs.

Answer

RAA is a part of intuitionistic logic, while EM is only found in classical logic.

Crowdly