Let's say that we know that $A$ is false. We disallow the use of law of excluded middle. Then is it true that $\neg A$ is true?
Add: How would "false" be (usually) defined in intuitionisitc logic and classical logic? I think this can be a starting point for the question..
The law of excluded middle is normally written as $A\vee\neg A$. In three-valued logic that would typically come out either true or "neither true nor false" but never false. If only always-true sentences count as theses, then excluded middle would not be a thesis--and yet $\neg A$ would be true if $A$ is false. This all assumes the most natural negation operator, namely one that flips true to false and false to true, and leaves "neither" as "neither."
The "usual" way to define the negation : $\lnot$ is to introduce a propositional constant (or $0$-connective) : $\bot$.
See Dirk van Dalen, Logic and Structure (5th ed - 2013), page 30 :
As usual “$\lnot \varphi$” is used here as an abbreviation for “$\varphi \rightarrow \bot$”.
In this way, in classical logic, the semantics for $\lnot$ is "reduced to" that for $\rightarrow$ :
when $\varphi$ is true $\varphi \rightarrow \bot$ is $T \rightarrow F$, which is false,
and
when $\varphi$ is false $\varphi \rightarrow \bot$ is $F \rightarrow F$, which is true.
In intuitionistic logic the definition still holds.
What differ are the rules. In classical logic we have [see page 30] :
(RAA) $$\frac {\frac {[\lnot \varphi]} \bot } \varphi$$
which does not hold in the intuitionistic one.
The difference is due to the different semantics [see page 156] :
The primitive notion is here “$a$ proves $\varphi$”, where we understand by a proof a construction. [...] :
$(→)$ : $a$ proves $\varphi → \psi$ iff $a$ is a construction that converts any proof $p$ of $\varphi$ into a proof $a(p)$ of $\psi$.
$(⊥)$ : no $a$ proves $\bot$.
Thus [page 157] :
The only rule that lacks constructive content is that of reductio ad absurdum (RAA). As we have seen [see page 36], an application of RAA yields $\lnot \lnot \varphi → \varphi$, but for $\lnot \lnot \varphi → \varphi$ to hold [in intuitionistic logic] informally we need a construction that transforms a proof of $\lnot \lnot \varphi$ into a proof of $\varphi$.
Now $a$ proves $\lnot \lnot \varphi$ if $a$ transforms each proof $b$ of $\lnot \varphi$ into a proof of $\bot$, i.e. there cannot be a proof $b$ of $\lnot \varphi$. $b$ itself should be a construction that transforms each proof $c$ of $\varphi$ into a proof of $\bot$.
So we know that there cannot be a construction that turns a proof of $\varphi$ into a proof of $\bot$, but that is a long way from the required proof of $\varphi$ !
If A is false, the law of the excluded middle has no bearing on the status of ¬A. The law of the excluded middle consists of a disjunction... as rather clearly seen when it gets written in Polish notation: ApNp. The truth value of ¬A only depends on the unary operator ¬ (or N) here, as the following three-valued truth tables make clear:
A 0 1 2 N
0 0 1 2 1
1* 1 1 1 0
2 2 1 2 2
Here ApNp is not a tautology, since A2N2=A22=2. However, if p=0 (p is false), then Np=1, in other words p is true.
