If a proposition is not provable, yet raises no issues if regarded as true, then it can be added as an axiom and used in theorems.
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.
If a proposition is not provable, yet raises no issues if regarded as true, then it can be added as an axiom and used in theorems.