A function is decidable if there is a Turing Machine that computes the function in a finite amount of time (i.e., the Turing Machine halts). Instead of talking about Turing Machines, though, let's use functions instead, because to me they're a little easier to think about, but otherwise exactly the same. I'll use ML syntax here.

In particular, we would like to find a function

```fun H f x = true iff f:int->int halts on input x:int
```
But consider a function
```fun diag x = if (H diag x) then loop() else true
```
where
```fun loop () = loop ()
```
So then
```(H diag x = true) only if ((diag x) halts)
```
But (diag x) halts exactly when (H diag x) evaluates to false, which is a contradiction. Thus no such function H can exist.

This is the halting problem, from which most of the theory of decidability branches out. So what can we do with the fact that H does not exist? Well, if we can show that given a "black box" function B, if we can use B to write H, then B must not exist. Here's an example:

Let's define

```fun Z f = true iff f(0) halts, f:int->int
```
But then
```fun H f x = Z (fn 0 => f x)
```
Here, if Z can decide whether (fn 0 => f x) halts on input 0, then that's really deciding whether f x halts, which is the halting function. So Z cannot exist. Here are a few more examples:
```fun Hsome f = true iff f x halts for some input x:int
but
fun Z f = Hsome (fn 0 => 0 | fn _ => loop ())
```
Here we've reduced Z to Hsome. Since Z can't exist, neither can Hsome.
```fun Hevery f = true iff f:int->int halts on every input x:int
but
fun Z f = Hevery(fn _ => f 0)

fun E (f, g) = true iff f(x) = g(x) for all x:int
but
fun H f x = E ((fn y => f x; y), (fn y => y))

and finally
fun Hsame (f, g) = true iff f and g halt on the same input
but
fun Hevery f = Hsame (f, fn _ => 0)
```
Please note that these functions Z, Hsame, etc., do exist for certain cases (i.e., for certain f's) and sometimes not insignificant cases; all we've shown here is that they do not work in the general case (for every f).

There are many more functions that are not decidable and many more classes of decidability (i.e., recognizability), but that is beyond the scope of this node.