Gecko only supports document.characterSet and that is the one DOM4 will keep. The others will be removed from the standard as they do not seem necessary for legacy compatibility.
Document.defaultCharset is not an alias for charset, so let's not discuss it here. Perhaps you meant inputEncoding? If you'd actually like us to consider removing defaultCharset, please file a separate bug, although my initial answer will be similar to the one below. Both document.charset and document.inputEncoding are well established in standards, and should not be removed from implementations. See <http://www.w3.org/TR/REC-DOM-Level-1/level-one-html.html> and <http://www.w3.org/TR/DOM-Level-3-Core/core.html#Document3-inputEncoding> respectively. I would suggest the following course of action: specify all of charset, characterSet and inputEncoding, the latter two being deprecated. Document.charset is writable, and that trait can also be deprecated as far as I know, but it needs research. Implementations will not remove support for any of these in foreseeable future. The reason why I suggest making charset the non-deprecated one is that it has the longest history in major browsers, and is best known to web developers.
I meant document.charset and document.defaultCharset, neither of which is listed in either of the documents you cite.
My mistake, charset is not in any W3C spec indeed. Still, it's supported in vast majority of browsers, and removing support from WebKit would be counter-productive. If you actually meant defaultCharset, then why did you report both in the same bug? It's a completely different feature.