Daniel Spiewak's proof that there exist total functions which are not inductive uses the following assumption:
I am going to assume that the problem of determining whether some arbitrary function is inductive [...] is in fact decidable. I actually don't have a reference on this one, but it seems like a fairly reasonable assumption. Formally:
exists D, forall f, f in I <=> (D(f) = TRUE)
I have modified the statement of the assumption slightly. In fact, my modification is not equivalent to the original, since my version says "there is a decider for inductive functions" where the original is "there is a single decider for both inductive and coinductive functions". It is conceivable that there is only a technique that can tell whether a function was either inductive or coinductive but can't tell which it is, in which case the above statement would not be implied. But that is an exotic enough possibility that I'm comfortable with my simplification.
However, the statement of the assumption is a bit vague. A decision procedure is a computable function on naturals (equiv. Turing machine, etc.), and we are trying to hand it a function. In what way is the function represented as a number? For example, the identity on booleans i can be represented in two ways:
i x = x
i True = True
i False = False
These are the same function (they have the same extensional behavior), but they have two different presentations. I will refute the possibility that you can just "pick a representative" to give to D: It is undecidable in general whether two presentations represent the same function. This can be seen by straightforward reduction to the halting problem; consider these two presentations
f x = x
f' x = if L then x else infinite_loop
where L is an arbitrary lambda term. Deciding whether f is equivalent to f' is equivalent to the halting problem for L.
So there is no computable way to get a representative of an equivalence class of presentations, and we do in fact have to think about what presentation we are giving to D.
It is clear that there is a decider for some presentations of inductive functions; e.g. an Agda definition that passes the type checker. But we could present that same function in a way such that its inductive structure is not apparent from the presentation, and the decider would not be able to decide that.
The way this impacts the original proof: how do we know that a function with a general recursive presentation does not have some inductive presentation that we simply have not found? Perhaps every total general recursive function can be written in an inductive way.