It turns out that for powerful theories of Computer Science,

there must exist infinitely many propositions that are

inferentially undecidable, that is, can be neither proved nor disproved.

However, the propositions cannot be specified constructively

and so are not very interesting.

Currently, there seem to be no propositions interesting to

practical Computer Science that are provably inferentially

undecidable.