Here is a partial answer.
Godel's theorem connects logic and set theory. Syntax is the part of the logic, it's where the formulas and proofs live; set theory is the part of the semantics, where the interpretations and models live. Of course one can have them relocated to other contexts, but classically I think that it's a theorem about logic and set theory.
It is provable without the axiom of choice that if we have an infinite tree whose nodes are the natural numbers, and every level of the tree is finite, then there is a branch in that tree. If we omit the requirement that the nodes of the tree are the natural numbers, it won't be true anymore and counterexamples do exist (by which I mean, consistent with $\sf ZF$, of course).
Similarly, given a countable language we write the proof of the completeness theorem for that language, and all our uses of the axiom of choice will be mitigated by the fact that we have a uniform enumeration of all the objects of interest. Therefore some fragment of the completeness theorem is in fact provable without any appeal to the axiom of choice.
On the other hand, the completeness theorem is not about countable languages. It is about any language of first-order logic. So we can have a lot of function symbols, or constants, or so on. So what about the above proof? Well, it can be shown that if the language is well-orderable, then indeed we can repeat the same arguments and everything is well-orderable uniformly and everything is fine.
But alas, without the axiom of choice, not every set can be well-ordered. And that where the non-constructive nature of the proof sneaks in. Let me give a particular counterexample.
Example:
We say that a set $A$ is amorphous if it is infinite, and cannot be written as a disjoint union of two infinite sets. One can show that if $A$ is an amorphous set, then there is no way to linearly order $A$. That is, there is no $R\subseteq A\times A$ such that $(A,R)$ is a linearly ordered set.
Suppose that $A$ is an amorphous set (and it is consistent that such set exists), and let $\mathcal L$ be the language in which $<$ is a binary relation symbol, and for every $a\in A$ there is a constant symbol $c_a$.
We write the axioms, $\varphi$ is the conjuction of the statements $<$ is a linear order, and for every distinct $a,b\in A$ we write $\varphi_{a,b}:=c_a\neq c_b$. This theory is consistent, because if it were to prove a contradiction there would be a finite number of $a\in A$ whose constants appear in the proof, but then we can construct a finite linear order which will be an interpretation of these axioms. This is impossible of course.
However, the theory as a whole, despite being consistent, does not have a model. Because in any model of the theory, reducing just to the constants will have defined a linear order of $A$, and $A$ itself is an amorphous set, so it cannot be linearly ordered.
So where is the axiom of choice coming into the play? When we construct models we need to make some arbitrary choices along the way. When the language is well-ordered then we can delegate these choices to the well-ordered and uniformly make them all; but when the language is an arbitrary set which may not be well-orderable to begin with, then the axiom of choice is needed.
In fact, one can prove that the completeness theorem (and its equivalent, the compactness theorem) is equivalent to the ultrafilter lemma, stating that every filter can be extended to an ultrafilter. These all are also equivalent to many other weak choice principles such as Tychonoff theorem for Hausdorff spaces, or the Boolean Prime Ideal theorem.
So what is missing from this answer? Well, I don't know about contexts where the WKL is not provable, so I cannot help in that aspect. But hopefully this answer shed some light on where the theorem is using fragments of choice and non-constructiveness.
A formula $A$ is a tautology if it is true with every assignment.
A formula $A$ is satisfiable if there is at least an assignemnt $v$ such that $A$ is true for $v$.
If $A$ is true for the assignment $v$, then its negation, $¬A$, is false for that assignment.
A formula $A$ is a tautology iff its negation, $¬A$, is not satisfiable.
The complement of a decision problem :
is the decision problem resulting from reversing the yes and no answers.
Thus, in a nutshell, if the answer to the problem "is $A$ in TAUT ?" is NO, then $¬A$ is in SAT.
More precisely, the problem of determining if some formula $A$ is not a tautology is thus equivalent to the problem of determining if the negation of the formula, $¬A$, is satisfiable.
It seems to me that it is only a terminological issue. Compare with :
Now we define some additional complexity classes related to $\text {P}$ and $\text {NP}$.
If $L ⊆ \{ 0, 1 \}^∗$ is a language, then we denote by $\overline L$ the complement of $L$.
We make the following definition: $\text {coNP} = \{ L \mid \overline L ∈ \text {NP} \}$.
$\text {coNP}$ is not the complement of the class $\text {NP}$. The following
is an example of a $\text {coNP}$ language: $\overline {\text {SAT} } = \{ \varphi \mid \varphi \text { is not satisfiable} \}$.
The decision problems (or languages) are complementary : not the corresponding classes of formulae.
Best Answer
Yes. If $A$ holds in the context, then you may infer that $A\vee B$ holds (whether $B$ does or does not). After all, $A\vee B$ is the claim that at least one from $A$ or $B$ holds. So when at least one does (eg $A$), then the disjunction holds too.
PS: the rule of Addition is not about adding the whole statement. In logic proof systems, it refers to the rule by which any disjunct can be added to an existing statement. That if $A$ is derivable (or assumed), then $A\vee B$ may be inferred in the same context.
It is possible to raise an assumption (rule P) that contradicts a prior statement. You may open a sub-proof by assuming anything as needed for the sake of argument; just be sure to close the sub-proof by discharging it with a valid rule (such as rule CP, "conditional proof").
This is the Principle of Explosion, otherwise known as ex falso (sequitur) quodlibet (Latin for "from falsehood, anything follows"). If your premises contain a contradiction, you can derive anything via valid rules of derivation. Since it is valid to do so, therefore you may do so.
So you want to prove $\neg A\to(A\to B)$? Well, since that is a conditional statement, you should use a conditional proof: raise $\neg A$ as an assumption with the aim to derive $A\to B$.
So you want to prove $A\to B$, under the assumption of $\neg A$? Well, again you should use a conditional proof: raise $A$ as an assumption with the aim to derive $B$.
So you want to prove $B$ under the assumptions of $\neg A$ and $A$? Well, you have assumed $A$ so you may infer $A\vee B$ (via Addition), but you have also assumed $\neg A$, so you may further infer $B$ (via Disjunctive Syllogism).
Why now, you have successfully derived $B$ in the context of the two assumptions, $\neg A$ and $A$, so you may now discharge those assumptions to close the two conditional proofs.
Thus you have proven $\neg A\to(A\to B)$ using the rules of assumption, conditional proof, addition, and disjunctive syllogism.