If A contains no disjunction (∨) or existential quantifier (∃), then ¬¬A → A is provable in intuitionistic logic

This is important because Brouwer’s intuitionistic analysis is inconsistent with LEM. However, if \(A\) is any negative formula (without \(\vee\) or \(\exists\)) then \(\neg \neg A \rightarrow A\) is provable using intuitionistic logic. A reconciliation of intuitionistic and classical analysis along these lines, inspired by Troelstra [1977] and Kripke[2019], is suggested in Moschovakis [2017].