In predicate logic, can the form of a translation of an existentially quantified sentence be used with a universally quantified sentence? In predicate logic, can the form of a translation of an existentially quantified sentence be used with a universally quantified sentence? 
That's a lot of words for a simple question. 
But here's what I'm wondering. 
Say we have the sentence
"There is at least one brown horse"
With an unrestricted domain of discourse that would translate to
∃x[Bx & Hx]
If we have the sentence
"All horses are brown"
∀x[Hx → Bx]
That translation seems to say 
"(∀x[) What I say next will apply to every instance of the thing I'll talk about"
"The thing I'm talking about (x) is a horse (H)"(Hx). 
"Whenever the thing you're talking about is a horse, it's also the case that (→) the thing you're talking about is a thing that's brown(Bx)" (→ Bx)
That said. 


*

*Doesn't '∀x' seem redundant. Doesn't it follow from H → B that all horses are brown?
Like R → W  (if you have rain, then you have water). If that weren't the case, you wouldn't be able to write H → B. 

*Even if we wanted to say something about x, whatever it is, couldn't we write:
(x → H) → B
or
(x → H) & (x → B)

*Couldn't you also write ∀x[Hx → Bx] as ∀x[Hx & Bx]?

*And isn't ∀x[Hx & Bx]  written just the same as  ∃x[Bx & Hx], but with a universal quantifier?

*So why is my text saying I should write ∀x[Hx → Bx]?
Thank you.
 A: *

*It seems redundant but it isn't. Whenever you have a free variable $x$ in a predicate (like $Hx\to Bx$), you can introduce a universal quantifier for it ($\forall x(Hx\to Bx)$). And on the converse, if you have a variable bound in a universal, you can elimiate the universal. But you can't do that when the variable is not free.

*The $(x\to H)\to B$ and other syntax you use here does not make any sense. $x$ is a variable, not a predicate.

*$\forall x (Hx \wedge Bx)$ means that both $H$ and $B$ are satisfied, and that's a completely different thing. In your case, it says that everything is a horse and everything is brown.

*No. existentials and universals mean completely different things. For instance, you can introduce an existential from a concrete case $P(c) \implies \exists x P(x)$, but you can only introduce a universal on an already existing free variable: $P(x) \implies \forall xP(x)$
A: (1) Doesn't $\forall x$ seem redundant ?
In standard first order logic we have that $A(x)$ is true iff $\forall x A(x)$ is true. So, it is correct to say that the two formulae $A(x)$ and $\forall xA(x)$ have the same meaning. 
But you cannot, in general, avoid the quantifiers, because otherwise you are not able to express the different meaning in other interesting contexts.
Working with an example by S.C.Kleene, Introduction to metamathematics [1952], the formula:

(a) $\forall x(x \neq 0) \rightarrow 0 \neq 0$ is (silly but) true in the natural numbers.

Instead, the formula :

(b) $\forall x(x \neq 0 \rightarrow 0 \neq 0)$ is false.

Why they have different meanings ? We will exploit the fact that $P \rightarrow Q$ is equivalent to $\lnot P \lor Q$.
(a) translates into : $\lnot \forall x (x \neq 0) \lor 0 \neq 0$.Using the properties of quantifiers, this is the same as : $\exists x \lnot (x \neq 0) \lor 0 \neq 0$, i.e.$\exists x (x = 0) \lor 0 \neq 0$ (simplifying the double negation). 
Now we have translated (a) into an equivalent form, i.e. the disjunction $\exists x (x = 0) \lor 0 \neq 0$ that is true because the first disjunct is : into the domain of natural numbers there are numbers equal to $0$ (of course, $0$ itself).
(b) instead, translates into : $\forall x (\lnot x \neq 0 \lor 0 \neq 0)$. Simplifying the double negation, we have : $\forall x (x = 0 \lor 0 \neq 0)$ and this is not true because if we instantiate the universal quantifier to $1$ (i.e. $x := 1$) we would have :
$1 = 0 \lor 0 \neq 0$ --- FALSE!
A: We need to introduce a concept of type. $x$ is a variable. $H(x)$ is a Boolean value. $H$ is a function from variables to Boolean values. Then $H \to B$ or $x \to H$ makes no sense because $\to$ is an operation on two Booleans.
(3). $\forall x (Hx \to Bx)$ reads "If it's a horse, then it's brown". $\forall x (Hx \wedge Bx)$ reads "Everything is a brown horse". That's fine if you know that $x$ comes from the set of horses, but you don't. Also, it would make $Hx$ redundant.
