I think you have more or less understood the issue. If your formula has free variables, it is an 'open' formula with no specific truth value. Quantifiers let you form 'closed' formulae (called sentences) that have a specific truth value (given any model). Note that if the model has a finite domain, and you are only interested in talking about that single model, then you can easily replace "$\forall$" by an appropriate conjunction, and "$\exists$" by an appropriate disjunction. However, it is impossible to do so when you want to make statements about arbitrary models (even if they are guaranteed to be finite).
In some mathematical writings, people conventionally assume that all free variables are implicitly universally quantified, but that just means that the quantifier is merely hidden, and not that it was actually 'removed'. Also, under that same convention, the existential quantifier cannot be expressed with a quantifier-free formulation. For example, "$\forall x \exists y ( x \ne y )$" is one way of saying that there is more than one object. By the convention "$x \ne y$" would mean that every $x$ is distinct from every $y$, which is obviously different.
Furthermore, you cannot arbitrarily change the convention and stipulate that different variables refer to different objects, otherwise you cannot say "$\exists x \forall y ( x = y )$" to mean that there is exactly one object.
The bottom-line is that no matter what convention you choose, you have to have some mechanism for expressing quantification otherwise you would never be able to handle classical logic.
Please note that any conditional is true as soon as its antecedent (the 'if' part) is false.
So, we can easily make your:
$(\exists x)[[(Sx \wedge Dx) \wedge (\forall y)(Ty \rightarrow \neg By)] \rightarrow Hx]$
true by pointing to any one object that is not a driver, or that is not safe. Put differently: this statement would be true in any domain where there is at least one non-driver, and anything the statement is trying to say about the actual safe drivers has become completely irrelevant. So, this is certainly not what you want.
It is indeed the reason why you almost never see an existential claim being an existentially quantified statement of a conditional: they can almost always be made vacuously true.
OK, so why use a universal in the case of 1? Because the use of 'a' is really reflecintg 'any. That is, it is saying: "for anything at all, if it is a safe driver, then ..."
Consider this sentence: "If a cat whips its tail, the it is mad". Here, we clearly make a universal statement about any cat, and so this should be symbolized as something like:
$\forall x ((C(x) \land W(x)) \to M(x))$
Again, the existential version of this:
$\exists x ((C(x) \land W(x)) \to M(x))$
can be made vacuously true by something that is not a cat, and hence this latter statement does not end up forcing, and thus saying anything, about an actual cat that whips its tail.
OK, but then why in 2 do we use an existential? It is because 2 is really of a different form. Statement 2 is in fact not a quantified statement at all! It is a conditional ... whose antecedent and consequent both happen to be quantified statements. Most importantly, the 'then' part is not making any references to any of the objects referred to in the first statement, so you don't have one quantifier quantifying over a conditional where the 'if'; and 'then' part have the same subject, but rather a conditional relating two quantified statements, each with their own subject.
So, 1 and 2 are quite different statements! But when you express them in English, they sounds very similar. Indeed, statements of type 1 are often referred to as 'donkey sentences', after the famous:
"If a farmer owns a donkey, then he will beat it"
Do you see now why this sentence is a (double) universal rather than a (double) existential?
Best Answer
With respect to the last part of your question, i have tried and answered them here
You can use the $\exists!$ quantifier, which reads as "there exists a unique". You can read more here, which shows how to represent the symbol in the symbols you are "allowed" to use.