Brandon Moore writes: (snip)

The term I've heard is "skolem constant", which is a freshly invented thing distinct from everything else. (snip)

There's a nice easy-going example in chapter 8 of http://www.cl.cam.ac.uk/Teaching/2000/LogicProof/notes.pdf where quantifiers are removed from first-order formulae. (this aside moved from haskell to haskell-cafe) -- Mark