Can undecidability theorems be detected by a machine? [closed]

Question

this question was originally written in mathoverflow, but a comment recommended me to rewrite it as a CS question.

This is not a mathematically formalized question. I'm sorry for that but think it's more like mathematics than philosophy.

When we proved a theorem A which says "B is undecidable", we don't try to prove neither B nor (not B). Can a machine do the same thing? Can it detect "meaning" of a statement, like "something is undecidable"?

Here's a reason why I don't think so.

Suppose a sentence

universal_Turing_machine(program, input, output)

is true if and only if resulting output of "program" with given "input" is "output". Of course, if the program doesn't halt, it would be false for any "input" and "output".

Now, let x be a Godel number of a sentence. Consider the following sentence:

there is no y such that:
y is a Godel number of a string which ends with a sentence encoded as x, 
and universal_Turing_machine(program, y, true)

If the program acts as a "decision program accepting valid proofs", this sentence obviously means "a sentence encoded as x is not provable". If not, this sentence doesn't mean any undecidability. Hence if a machine can detect undecidability theorems, it has to detect programs which act as "decision programs accepting valid proofs"

But according to Rice's theorem, detecting programs which has a specific property is not possible.

Do you think this "reason" makes sense? Since this is not a pure mathematical question, I hope to listen to your opinions. Thank you.