How does one prove inadmissibility of inference rules in First Order Logic? 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.
 A: 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*}
