In My Head

but the voices keep talking anyways

A Country Doctor

as soon as a theory is strong
enough to capture the results of boringly mechanical reasoning about decidable
properties of individual numbers, it must itself cease to be decidable.

—Intro to Godels Theorems

"5.2 More about effectively enumerable sets
We are going to show that the set of truths of a sufficiently expressive language
is not effectively enumerable. To do this, we need three initial theorems about
effectively enumerable sets.
(a) We start with an easy warm-up exercise. Recall: a set of natural numbers W
is effectively enumerable iff it is either empty or there is an effectively computable
function f which enumerates it.2 Then,
Theorem 5.1 If W is an effectively enumerable set of numbers,
then there is some effectively decidable numerical relation R such
that n ∈ W if and only if ∃xRxn.
Proof The theorem hold trivially when W is empty (simply choose a suitable R
that is never satisfied). Suppose, then, that the effectively computable function
f enumerates W. That means the values f (0), f (1), f (2), … give us all and only
the members of W. So n ∈ W iff ∃xf (x) = n. We now just define Rmn to hold
iff f (m) = n. Evidently, we can decide whether Rmn obtains just be evaluating
f (m) and checking whether the result is indeed n – and both steps are, by
hypothesis, algorithmically computable. So we are done.”

—— Excuse me?

—Intro to Godels Theorems