I was going to add this from the docs of D[]:

D returns generic results that may not account for discontinuities, cusps or other special points

This is the case for Kronecker[x]. However, the following seems wrong (should be Pi*x, not 2*Pi*x, right?):

D[SawtoothWave[x], x]
(*  Piecewise[{{1, Sin[2*Pi*x] != 0}}, Indeterminate]  *)

Otherwise, we could use SawtoothWave[x] + SawtoothWave[1 - x] for Ceiling[x] - Floor[x].

Further, @Daniel may like this integral better:

Integrate[KroneckerDelta[Sin[Pi x]], {x, 0, x}]
(*  ConditionalExpression[0, x \[Element] Reals]  *)

I cannot say that I like the integrals. But the derivatives make good sense to me. The Kronecker delta, unlike its Dirac analog, is not a functional. There are no plausible alternatives for the derivatives that I'm aware of.

Sorry, I didn't notice your reply, so I'm replying late.

So, if it were to "solve" the problem with variables but a user wanted to use the solution with values (in particular the values I used as examples), well then they'd get very incorrect results.

And what incorrect results they will get if Wolfram computes it?

In:  FullSimplify[Ceiling[x] - Floor[x] == 1  
 x \[Element] Reals]
Out: x \[NotElement] Integers

Let's be specific!

You're gorgeous as always!

There isn't such a function presently

I realize that. I put it that way for brevity. You can leave Ceiling[x] - Floor[x] -1 as the definition of a function on the set of real numbers. The important thing is for Wolfram to prove that this function is -1 if x is an integer and 0 if x is a non-integer.

Okay, maybe my response was irrelevant, but I'm not convinced, so let me try again. I see your point about my example using concrete values while you're only interested in the abstraction provided by variables. But Mathematica doesn't want to give an untrue answer (as much as reasonable, there are in fact weird edge cases that one could consider untrue, but I don't think we need to go into that). So, if it were to "solve" the problem with variables but a user wanted to use the solution with values (in particular the values I used as examples), well then they'd get very incorrect results.

As for your questions...

I would like Wolfram to be able to convert an expression Ceiling[x] - Floor[x] - 1 into a function that has zero everywhere except the set of integers, where it has -1.

That's easy. We can just use your expression directly:

myFunc[x_] := Ceiling[x] - Floor[x] - 1;
Table[myFunc[x], {x, -2, 2, 1/4}]
(* {-1, 0, 0, 0, -1, 0, 0, 0, -1, 0, 0, 0, -1, 0, 0, 0, -1} *)

There are probably many ways to define such a function, there may even be a built in function for that.

to what extent can Wolfram help in theoretical mathematics?

I'm not the right person to answer that, but as far as I can tell there are many people doing sophisticated mathematics with Wolfram.

Okay, let me first emphasize that I sympathize with you. I'm not arguing with you. It's perfectly reasonable for you to expect there to be a natural expression that gets you to where you want. But what you've got to remember is that Mathematica is not a logic system. We can quibble about things around the edges, but in the main, all Mathematica is doing is evaluating expressions. So, when you are trying to assert something like x \[NotElement] Integers that is first an foremost just an expression, it's not an assertion. You're not registering an assertion into a logic framework.

If I understand you, you want Mathematica to "solve" Ceiling[x] - Floor[x] == 1 by telling you the domain in which it holds true. Logically, that domain should be x \[Element] Reals && x \[NotElement] Integers. Unfortunately, that expression simply doesn't resolve for all x. I don't have any knowledge about the inner workings of Mathematica's code, but I believe that the reason this is failing is because this expression isn't guaranteed to resolve for all of the relevant numeric values. For example,

With[
 {x = 2.0},
 x \[Element] Reals && x \[NotElement] Integers]
(* 2. \[NotElement] Integers *)

So, Mathematica was not able to determine the truth/falsity of that second term. Now, you may be thinking, "yes, but that value isn't in the domain of the solution", and I totally sympathize, but I still think that the underlying ambiguity of that expression is interfering. I could be totally wrong--we'd probably need someone more familiar with the underlying code to confirm.

I am sure that FullSimplify has a bunch of ad hoc rules that it knows how to apply, and maybe this particular case should be added to those rules, but for now it appears that it simply isn't. Maybe there's a very good reason for this, I don't know. But you're just beating your head against a wall here. Which leads me to ask what your real objective is. This looks more like some sort of test case for Mathematica itself than a computational problem that you need help with. What is it that you're actually trying to achieve? If this is just for curiosity's sake, then I think we've gone as far as we can. If this particular computation is interfering with some actual computational goal you're working toward, then maybe we can explore workarounds.

I think Hans Milton provided a good example, and your reply to that doesn't seem relevant. Here's another way to look at it:

FullSimplify[Ceiling[x] == Floor[x], x \[Element] Integers]
(* True *)

FullSimplify[Ceiling[x] == Floor[x], x \[Element] Reals]
(* Ceiling[x] == Floor[x] *)

So, you can interpret that as meaning, "when x is real, Mathematica cannot find a simplification that resolves the equality to true or false". And of course, like Hans showed, one example is 2.0. Indeed, we have

2 \[Element] Reals
(* True *)

So, we don't even need an expression with Real as its Head. Furthermore, consider this

2. \[Element] Integers
(* 2. \[Element] Integers *)

2. \[NotElement] Integers
(* 2. \[NotElement] Integers *)

meaning that Mathematica withholds commitment about the integer-valued-ness for a value that you expect to satisfy your assumptions. I think the answer to your original question depends upon the reason for that.

What do you mean? Here's another example:

In:  1 \[Element] Rationals
Out: True

In:  Ceiling[x] == 1 + Floor[x] /. x -> 12/5
Out: True

In:  FullSimplify[Ceiling[x] == 1 + Floor[x], x \[Element] Rationals]
Out: Ceiling[x] == 1 + Floor[x]