Yes, this is what constructivism is all about! In intuitionistic logic, the law of excluded middle doesn't generally hold, so it is not always possible to derive $A$ (i.e. $A$ is true) from $\lnot\lnot A$ (i.e. $A$ is not false).

The particular case you're considering is a form of Markov's Principle, which can be worded as if it is not the case that there is no example, then an example does exist. Symbolically, the rule is $$\lnot\forall x\lnot A(x) \to \exists x A(x),$$ where $A(x)$ is required to be decidable: $\forall x(A(x) \lor \lnot A(x))$. In constructive mathematics, existence is very strong — it is not acceptable to merely show that there must be an example, one needs to actually produce an example in some way or another. Markov's principle says that showing that there must be an example is enough to prove existence. Thus this principle is not generally accepted by most schools of constructivism, except in limited instances.

Yes, this is what constructivism is all about! In intuitionistic logic, the law of excluded middle doesn't generally hold, so it is not always possible to derive $A$ (i.e. $A$ is true) from $\lnot\lnot A$ (i.e. $A$ is not false).

The particular case you're considering is a form of Markov's Principle, which can be worded as if it is not the case that there is no example, then an example does exist. Symbolically, the rule is $$\lnot\forall x\lnot A(x) \to \exists x A(x),$$ where $A(x)$ is required to be decidable: $\forall x(A(x) \lor \lnot A(x))$. In constructive mathematics, existence is very strong — it is not acceptable to merely show that there must be an example, one needs to actually produce an example in some way or another. Markov's principle says that showing that there must be an example is enough to prove existence. Thus this principle is not generally accepted by most schools of constructivism, except in limited instances.

Yes, this is what constructivism is all about! In intuitionistic logic, the law of excluded middle doesn't generally hold, so it is not always possible to derive $A$ (i.e. $A$ is true) from $\lnot\lnot A$ (i.e. $A$ is not false).

The particular case you're considering is a form of Markov's Rule, which can be worded as if it is not the case that there is no example, then an example does exist. Symbolically, the rule is $$\lnot\forall x\lnot A(x) \to \exists x A(x),$$ where $A(x)$ is required to be decidable: $\forall x(A(x) \lor \lnot A(x))$. In constructive mathematics, existence is very strong — it is not acceptable to merely show that there must be an example, one needs to actually produce an example in some way or another. Markov's rule says that showing that there must be an example is enough to prove existence. Thus the rule is not generally accepted by most schools of constructivism, except in limited instances.

Yes, this is what constructivism is all about! In intuitionistic logic, the law of excluded middle doesn't generally hold, so it is not always possible to derive $A$ (i.e. $A$ is true) from $\lnot\lnot A$ (i.e. $A$ is not false).

The particular case you're considering is a form of Markov's Principle, which can be worded as if it is not the case that there is no example, then an example does exist. Symbolically, the rule is $$\lnot\forall x\lnot A(x) \to \exists x A(x),$$ where $A(x)$ is required to be decidable: $\forall x(A(x) \lor \lnot A(x))$. In constructive mathematics, existence is very strong — it is not acceptable to merely show that there must be an example, one needs to actually produce an example in some way or another. Markov's principle says that showing that there must be an example is enough to prove existence. Thus this principle is not generally accepted by most schools of constructivism, except in limited instances.