How are OWL defined datatypes intended to be used?

Why would a:SSN have an empty lexical space here?

Datatypes and literal values are notoriously difficult to handle in symbolic reasoning. When you have a symbolic logic, such as first order logic or description logics, symbols denote things that are arbitrary elements in arbitrary sets. You don't need to know what the symbols denote in order to perform correct and complete reasoning (for instance, http://dbpedia.org/resource/France may denote anything, as far as a reasoner is concerned, and it is impossible to constrain this IRI to denote a specific thing in FOL or DL).

For literals, it is a completely different story because they are quantified. They denote specific values in specific sets. For instance "10"^^xsd:integer denotes the number “ten” and nothing else. This matters for the reasoner, because it has to understand that this is different from what "10"^^xsd:string denotes, but the same as what "10.0"^^xsd:decimal denotes. This means that however you implement your reasoner, there must a part of the code specifically dedicated to processing the literals with datatype IRI xsd:integer. Thanks to this dedicated code, an OWL reasoner is able to infer:

<s> <o> "10"^^xsd:int .

from:

<s> <o> "10.0"^^xsd:decimal .

If an ontology can introduce new datatype IRIs that can be used on literals, then you don't have the specifically dedicated code for literals with these types. Now, consider the following:

ex:one  a  rdfs:Datatype;
  owl:equivalentClass  [
    a  rdfs:Datatype ;
    owl:onDatatype  xsd:positiveInteger ;
    owl:withRestrictions ( [ xsd:maxInclusive 1 ] )
  ] .

Then, should the following be a well formed literal, given this datatype definition?

"1.0"^^ex:one

You see, "1.0" is in the lexical space of xsd:decimal and maps to the numeric value “one” in this datatype. The value “one” is also part of the value space of xsd:positiveInteger, but "1.0" is not a valid lexical form for an xsd:positiveInteger. You could argue that ex:one must only use the lexical forms of xsd:positiveInteger because it is defined as a restriction of it. But the problem is that you then have a semantic description (a piece of ontology) that defines a syntactic constraint (the way you are allowed to write a literal with a specific datatype IRI). Logicians know that logics that allow one to constrain the syntax with their semantics are devilish.

Because of the OWL 2 specification where the lexical space of ex:one is empty, it is then possible to say that ex:one is the same datatype as ex:oneD defined as follows:

ex:oneD  a  rdfs:Datatype;
  owl:equivalentClass  [
    a  rdfs:Datatype ;
    owl:onDatatype  xsd:decimal ;
    owl:withRestrictions ( [ xsd:minInclusive 1 ] [ xsd:maxInclusive 1 ] )
  ] .

One more remark, though: what I'm saying here is only valid when you consider the OWL 2 Direct Semantics. If you consider the OWL 2 RDF-based semantics, then there are other things to consider. Especially, in the RDF-based semantics, it is not necessarily the case that ex:one is the same as ex:oneD. They may be distinct datatypes that happen to have the same value space.

Regarding your other questions:

So why does the OWL spec say that the lexical space of a:SSN is empty, rather than the the set of finite-length sequences of zero or more characters (as defined in XML) that match the regular expression [0-9]{3}-[0-9]{2}-[0-9]{4}?

Here, you are considering the xsd:string datatype, where the value space and the lexical space are the same. The lexical-to-value mapping is identity. So it looks like there would be a trivial way to allow the datatype IRI to be used on literals. But consider the broader problem as I showed you before.

So does that mean that a:SSN cannot be used as follows?

Exactly.

If so, how is one supposed to use the a:SSN datatype?

You can use datatypes defined in this way as the range of a property, for instance, or in allValuesFrom or someValuesFrom restrictions. However, when it comes to concrete values attached to instances, you have to use the datatypes that are natively supported by OWL 2 reasoners, as you suggest in your last code snippet.

It seems to me that a:SSN has an empty lexical space in the example because it isn't itself "the set of finite-length sequences of zero or more characters that match the regular expression [0-9]{3}-[0-9]{2}-[0-9]{4}." Rather, that is the definition of a:SSN. The definition itself was made by constraining a datatype (xsd:string) that does not have an empty lexical space, which is why the section on patterns that you cited applies. That is, the example uses a pattern to constrain a datatype with a non-empty lexical space to define a datatype with an empty lexical space. Accordingly, since "there can be no literals of datatype a:SSN," you would have to either infer that "123-45-6789"^^xsd:string is an SSN by the usage of a:hasSSN or by asserting that "123-45-6789"^^xsd:string is an instance of a:SSN.

However, when it comes to concrete values attached to instances, you have to use the datatypes that are natively supported by OWL 2 reasoners, as you suggest in your last code snippet.

Else augment the capabilities of the reasoner, for your application. But don't expect these capabilities to be available when data is processed by a 'generic' OWL reasoner.