In FOL, can we say that if from a set of assumptions gamma we have no proof of A, then we have a proof of not-A ($\Gamma \vdash \neg A$)?
Additionally, are these rules admissible as part of a first order proof system:
a) $\frac {\Gamma \vdash \forall x(Ax \rightarrow Bx)}{\Gamma, \{ \neg B\} \vdash \forall x \neg A}$
b) $\frac {\Gamma \vdash \forall x(Ax \rightarrow Bx)}{\Gamma, \{ \neg B\} \vdash \exists x \neg A}$
My intuition is that (a) is clearly inadmissible and (b) is admissible, but I don't know whether my reasoning is clear enough.
As I see it, (a) is inadmissible because it would go against the normal interpretation of material implication. If we have $A \rightarrow B$ = True and B = False, it would mean A is false. But I don't know whether this type of semantic reasoning can be applied to proving the inadmissibility of a syntactical proof or not. I'm having difficulty not appealing to the meanings of the logical constants and trying to be fully syntactical.
For the first part of your question, the answer is no: a sentence in FOL can hold in some models but not in all models. E.g., $\forall x, y(x = y)$ holds iff the universe has exactly one element and is therefore neither provable nor disprovable. There are first-order axiom systems $\Gamma$ such that for every formula $A$ either $\Gamma \vdash A$ either $\Gamma \vdash \lnot A$, but such systems (which are called complete) are quite special: one example would be to take $\Gamma$ to be $\{\forall x, y(x = y)\}$ (under which assumption, FOL essentially reduces to propositional logic - do you see why?).
For the second part of your question, to prove a proposed rule is not admissible, the simplest approach is to look for a counterexample, i.e., an interpretation in which the antecedent of the rule holds, but the succedent does not. Consider your first proposed rule (a): $$ \frac{\Gamma \vdash \forall x(A(x) \to B(x))}{\Gamma, \lnot B(x)\vdash \forall x \lnot A(x)} $$ (I have tidied up your notation a bit and hope that the above is what you meant.) To get a counter-example, we can just take $\Gamma$ to be empty and interpret $A(x)$ and $B(x)$ in the natural numbers as follows \begin{align*} A(x) &\equiv x = 2 \\ B(x) &\equiv x > 1 \end{align*} Then the antecedent $\vdash \forall x (x = 2 \to x > 1)$ certainly holds, but the succedent $\lnot x > 1 \vdash \forall x(\lnot x = 2)$ does not (if we interpret the free $x$ in $\lnot x > 1$ as $1$).
For your second proposed rule (b):
$$ \frac{\Gamma \vdash \forall x(A(x) \to B(x))}{\Gamma, \lnot B(x)\vdash \exists x \lnot A(x)} $$ we can show that the rule is actually derivable (i.e., there is a fixed proof schema that shows how to derive any instance of the rule - this is a stronger property than admissibility). The details of the proof schema depend on the formulation of first-order logic you are using: the natural deduction proof schema would go something like:
\begin{align*} 1) \quad &\forall x(A(x) \to B(x)) \quad &\mbox{Conclusion of the antecedent} \\ 2) \quad &A(x) \to B(x) \quad\quad&\mbox{$\forall$-elim 1}\\ 3) \quad & A(x) &\mbox{Assume}\\ 4) \quad& B(x) &\mbox{$\to$-elim with 2 and 3}\\ 5) \quad& \lnot B(x) &\mbox{Assumption of the succedent}\\ 6) \quad& \bot &\mbox{$\bot$-intro with 4 and 5}\\ 7) \quad& \lnot A(x) &\mbox{$\lnot$-intro with 6 discharging 3}\\ 8) \quad& \exists x\lnot A(x) &\mbox{$\exists$-intro with 7} \end{align*}