Is there an algorithm that when given a set of axioms, will generate a statement independent of those axioms?

Gödel's original proof in effect delivers just such a recipe for a theory $T$ which is recursively axiomatized, contains (or can implement) at least the minimal amount arithmetic of arithmetic for the incompleteness theorem to apply, and is (omega) consistent. Of course there are complete theories to which Gödel's theorem doesn't apply (and some of them are non-trivial) But -- leaving aside the inconsistent cases -- these exceptional theories will have to be either theories which can't be effectively axiomatized or theories which know (almost) nothing about arithmetic or anything equivalent.

But assuming we are dealing with the right sort of theory, the construction of a Gödel sentence goes in two stages. We first choose some sensible way of "arithmetizing" the syntax of $T$ (i.e. coding up wffs, and proofs by numbers). [There's a lot of freedom of choice here, and different choices will lead to different sentences unprovable in $T$: so this phase is not deterministically algorithmic.]

Then Gödel tells us how to actually produce a wff $Gdl_T(x, y)$ of $T$ which represents the relation "$x$ codes up a proof of the wff that results from putting the numeral for $y$ for the free variable in a wff with code number $y$" [the details of this wff will depend on both $T$ and the chosen coding scheme, but we can give a recipe for producing the wff]. Then he shows how to construct, very simply, an undecidable Gödel sentence $G_T$ for theory $T$ out of $Gdl_T(x, y)$.

The procedure "choose a coding scheme, then apply the recipe for forming a Gödel sentence" applies quite generally (as Gödel stresses in his original 1931 paper), to construct an undecidable sentence for a given $T$ of the (very general) right kind. If you want more of the gory details, any standard text will tell you how the trick is done. Or look at Episode 9 of my online notes Gödel Without Tears


It depends on the set of axioms.

Some theories are complete, meaning that every statement (in the given language) can be proved or disproved from them. For example the theory of algebraically closed fields of characteristics $0$.

Some theories are so complicated that such algorithm will have to make appeals to oracles which can access informations we cannot compute on our own. For example the consequences of $\sf PA$ is not a decidable theory, so we don't have an algorithm to compute it.

The incompleteness theorems give us very specific requirements. The theory $T$ must be:

  1. Recursively enumerable.
  2. Strong enough to interpret basic truth about number theory.
  3. Consistent.

In which case the incompleteness theorem[s] give us a mechanism for writing down a statement which is independent of the theory $T$. If the theory does not fulfill these requirement it might be complete, or it might be inconsistent, or we might not have an algorithm (which doesn't make appeals to oracles).


Yes you can construct such a sentence. Godel's theorem shows how to do it, provided the axioms are appropriate for such a construction. It doesn't work for a decidable complete theory.

To do this using Godel's sentence, it needs the axioms of arithmetic or some subset of them that's sufficient to do the Godel construction. Robinson's arithmetic is sufficient for instance

You can even build a set of rules for constructing such sentences.

But if you formalize the process for constructing those sentences into a formal system - then that system itself has a Godel sentence that it can't construct. And again as a human mathematician using the approach of Godel's theorem you can construct a sentence for that too. But in some sense there has to be a possibility for endless creativity in constructing such sentences.

You can't derive an algorithm to derive all and only true Godel sentences from a theory. If you attempt to do so, it could be made into the basis for a set of deduction rules that you can then use Godel's method to find a sentence it can't produce.