weak counterexamples and the law of trichotomy in intuitionism I've been reading a reaserch in Stanford's website about Intuitionism and I can't really understand what is a weak counter example and how does the intuitionistic continuum lookes like and it's realtaion to the reals.
Basiclly I think I just can't understand  the example in the article.
The article's link: https://plato.stanford.edu/entries/intuitionism/#TwoActInt
I am talking directly on the Weak counterexample paragraph and speciffly this function: 
r_n = 
  \begin{cases}
    2^{-n} \text{ if } \forall m \leq n A(m) \\
    2^{-m} \text{ if } \neg A(m) \wedge m \leq n \wedge \forall k \lt m A(k). 
  \end{cases}
What I am basiclly trying to understand is why does thr law of trichotomy is not true on the intuitionistic continuum. 
 A: The property $A(n)$ is decidable, i.e. for evry natural number $n$ we can decide (calculate) if $A(n)$ holds or not.
But we cannot know if $\forall x A(x)$ holds or not.
We can start calculating the values of the sequence $\langle r_m \rangle$ "testing" $A(m)$ for $m=0,1,\ldots, n$.
If for all $m \le n$ we have that $A(m)$ holds, then we have that:

$r_0=2^{0}, r_1=2^{-1},\ldots, r_n=2^{-n}$. 

The question is : let $r$ the limit of the sequence $\langle r_m \rangle$; does the limit equal $0$ or not ?
If $A(m)$ hold for every $m$, then the sequence converges to $0$, but if instead there is $m_0$ such that $A(m_0)$ does not hold, then the sequence will be :

$r_0=2^{0}, r_1=2^{-1},\ldots, r_{m_0}=2^{-m_0}, r_{m_0+1}=2^{-m_0},\ldots$

and thus the sequence converges to $2^{-m_0}$.
Conclusion: due to the fact that we cannot know if $\forall n A(m)$ is true or not, we cannot know if :

$r=0 \lor r=2^{-m_0}$

i.e. we cannot know if :

$r=0 \lor r \ne 0$.

For details and discussion, see :


*

*Anne Troelstra & Dirk van Dalen, Constructivism in mathematics : An Introduction. Volume I (1988), page 5-on

A: For simplicity, let $A(m)$ refer to a specific statement -- in the article, they use "$m = 1$ or $2m$ is the sum of two prime numbers". That is, Goldbach's conjecture is the statement $\forall m(A(m))$. Then, classically, the sequence has either of two forms. If Goldbach's conjecture is true, then the sequence is given by $r_n = 2^{-n}$, and thus converges to 0. If Goldbach's conjecture is false, there is a least counterexample -- call this counterexample $m$. Then, $r_n = 2^{-n}$ for all $n \leq m$, and $r_n = 2^{-m}$ for all $n > m$.
Now, in either case, $r_n$ is a sequence of rational numbers, which is Cauchy. Hence, it represents a real number $r$, under the usual construction of the reals as the quotient of all Cauchy sequences of rationals under an equivalence relation.
Classically, we either have $r = 0$ (if Goldbach's conjecture is true) or we have $r > 0$ (if Goldbach's conjecture is false). And thus, $r = 0 \lor r > 0 \lor r < 0$ is true about $r$. However, an intuistionist would (might) say that this is meaningless; that the interpretation of $r = 0 \lor r > 0 \lor r < 0$ should mean that one of them is true, and that in order to have trichotomy for $r$, we should either have to be able to say $r = 0$, or that $r > 0$. At present, Goldbach's conjecture has not been proven or disproved; so we can say neither. Hence, trichotomy does not hold for the real number $r$.
Note that $r$ is itself essentially defined in terms of a dichotomy: we let $r_n = 2^{-n}$ if there is no counterexample to the Goldbach conjecture below $n$, and we let it equal $2^{-m}$ otherwise (where $m$ is the least counterexample). However, this dichotomy is fine to intuistionists, since it says something about a finite set we can check: it is possible to check this "bounded" Goldbach conjecture, at least in theory.
A: Assume that we know that either $r>0$, $r=0$ or $r<0$, where $r$ is a real number defined by $\langle r_n\rangle$. We can see that $r<0$ is impossible. If $r>0$, then $r_n$ stops to decrease at some point, that is, there is some $N$ such that $r_n = 2^{-N}$ for any $n\ge N$. Thus we have $\lnot P(N)$, which implies $\exists n \lnot P(n)$. Moreover $\exists n \lnot P(n)$ implies $\lnot\forall n P(n)$ in intuitionistic logic.
If $r=0$, then the sequence $\langle r_n\rangle$ goes to 0 as $n$ increases. Therefore we have $r_n= 2^{-n}$ so $\forall m<n P(m)$ holds for any $m$, hence $\forall n P(n)$. 
Therefore $(\forall n P(n)) \lor (\lnot \forall n P(n))$. That is, we know  whether $\forall n P(n)$ or $\lnot\forall n P(n)$ holds, which violates the assumption.
To note, the disjunction in the classical logic and an intuitionistic logic has quite different meaning. In the classical logic, $A\lor B$ just means either $A$ or $B$ is true. In an intuitionistic logic, however, $A\lor B$ means we know that one of $A$ or $B$ holds! For example, an intuitionistic logic satisfies following (meta-)property:
$$\vdash A\lor B \iff \vdash A\text{ or } \vdash B.$$
That is, we have a proof of $A\lor B$ only if we can prove one of $A$ or $B$ explicitly.
You may refer the BHK interpretation to get an intuition of an intuitionistic logic :)
