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

Question

Is there any mechanism or algorithm where one can generate mathematical statements/problems that are undecidable, i.e their proof is independent, from a certain set of axioms?

Answer 1

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).

Answer 2

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