What does $ \forall \alpha_1, \dots , \alpha_n . \tau $ mean formally as a type?
The notation is explained in your course material, e.g. here starting on slide 47.
In the notation $$T = \forall \alpha_1, \dots, \alpha_n.\tau$$ $\alpha_i$ are type variables, the $\tau$ is a monomorphic type, and $T$ is a universally quantified, polymorphic type. While free type variables may occur in $\tau$, the quantified variables $\alpha_i$ do not occur free in $\tau$.


  
  Why is there a dot separating the quantifier and the type
  


This is a just a syntactic convention used in type theory. The dot separates the quantifier part from the type it applies to.


  
  How does this relate to normal FOL? e.g. if I had $ \forall x \phi(x) $ that would mean that for all values x can take in the universe at hand, the proposition $\phi(x)$ is true
  


There's a strong relationship between logical formulas and types in programming languages, called Curry-Howard isomorphism.


  
  Is $\tau$ a function of the (meta?) variables $ \forall \alpha_1, \dots , \alpha_n $?
  


$\tau$ is not a function, it's a monomorphic type. You can think of the quantification as adding more context to this monomorphic type thus making it polymorphic. The quantification basically "hides" the variables from the context the whole expression appears in.


  
  What do $ \forall \alpha_1, \dots , \alpha_n $ stand for?
  Are $ \forall \alpha_1, \dots , \alpha_n $ meta-variables? What is their domain?
  


$\alpha_i$ are type variables that (typically) occur free in $\tau$, but are bound by the quantification and do not occur free in $\forall\alpha_i.\tau$ anymore. Like variables in a mathematical expression represent placeholders for concrete values, type variables represent placeholders for more concrete types.


  
  Could I have a couple of concrete examples of what they are
  


The most common example of a polymorphic type is the list type $\forall \alpha . \alpha\;\mathsf{list}$ (this is the notation for Ocaml, in Haskell the notation would be $\forall \alpha.[\alpha]$). In your real code this polymorphic type might be used as a monomorphic type when $\alpha$ is replaced by a concrete type like $\mathsf{int\;list}$, $\mathsf{bool\;list}$ or even $\mathsf{(int\;list)\;list}$.

Sometimes you may still deal with polymorphic types, for example the empty list literal $[\,]$ has the polymorphic type $\forall\alpha.\alpha\;\mathsf{list}$. Note that this is different from when you use $[\,]$ in your real code when it usually will be specialized to $\mathsf{int\;list}$ (or whatever concrete lists you are dealing with) when type inference happens. So $[\,]$ may have one polymorphic type or one of many monomorphic types, where the latter are all very different.

The above linked PDF gives more examples on slide 55.