Editing Law of excluded middle (section)

=== Intuitionist definitions of the law (principle) of excluded middle ===
The following highlights the deep mathematical and philosophic problem behind what it means to "know", and also helps elucidate what the "law" implies (i.e. what the law really means). Their difficulties with the law emerge: that they do not want to accept as true implications drawn from that which is unverifiable (untestable, unknowable) or from the impossible or the false. (All quotes are from van Heijenoort, italics added).

''Brouwer'' offers his definition of "principle of excluded middle"; we see here also the issue of "testability":

::On the basis of the testability just mentioned, there hold, for properties conceived within a specific finite main system, the "principle of excluded middle", that is, ''the principle that for every system every property is either correct [richtig] or impossible'', and in particular the principle of the reciprocity of the complementary species, that is, the principle that for every system the correctness of a property follows from the impossibility of the impossibility of this property. (335){{cn|reason=The "335" appears to be a page number? The source however is unclear.|date=January 2022}}

''Kolmogorov'''s definition cites Hilbert's two axioms of negation
<ol start="5"><li>''A'' → (~''A'' → ''B'')</li>
<li>(''A'' → ''B'') → { (~''A'' → ''B'') → ''B''}</li></ol>

::Hilbert's first axiom of negation, "anything follows from the false", made its appearance only with the rise of symbolic logic, as did the first axiom of implication … while … the axiom under consideration [axiom 5] asserts something about the consequences of something impossible: we have to accept ''B'' if the true judgment ''A'' is regarded as false …
::Hilbert's second axiom of negation expresses the principle of excluded middle. The principle is expressed here in the form in which is it used for derivations: if ''B'' follows from ''A'' as well as from ~''A'', then ''B'' is true. Its usual form, "every judgment is either true or false" is equivalent to that given above".
::From the first interpretation of negation, that is, the interdiction from regarding the judgment as true, it is impossible to obtain the certitude that the principle of excluded middle is true … Brouwer showed that in the case of such transfinite judgments the principle of excluded middle cannot be considered obvious
::footnote 9: "This is Leibniz's very simple formulation (see ''Nouveaux Essais'', IV,2). The formulation "''A'' is either ''B'' or not-''B''" has nothing to do with the logic of judgments.
::footnote 10: "Symbolically the second form is expressed thus
:''A'' ∨ ~''A''
where ∨ means "or". The equivalence of the two forms is easily proved (p.&nbsp;421)