I teoremi di indecidibilità possono essere rilevati da una macchina? [Chiuso

Question

Questa domanda è stata originariamente scritta in Mathoverflow, ma un commento mi ha consigliato di riscriverla come domanda CS.

Questa non è una domanda matematicamente formalizzata. Mi dispiace per questo, ma penso che sia più simile alla matematica che alla filosofia.

Quando abbiamo dimostrato un teorema A che dice "B è indecidibile", non cerchiamo di non dimostrare né b né (non b). Una macchina può fare la stessa cosa? Può rilevare "significato" di un'affermazione, come "qualcosa è indecidibile"?

Ecco un motivo per cui non la penso così.

Supponiamo una frase

universal_Turing_machine(program, input, output)

è vero se e solo se risultante output di "programma" con dato "input" è "output". Naturalmente, se il programma non si ferma, sarebbe falso per qualsiasi "input" e "output".

Ora, lascia che X sia un numero di Godel di una frase. Considera la seguente frase:

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)

Se il programma funge da "Programma decisionale che accetta prove valide", questa frase ovviamente significa "una frase codificata come X non è dimostrabile". In caso contrario, questa frase non significa alcuna indecidibilità. Quindi se una macchina è in grado di rilevare teoremi di indecidibilità, deve rilevare programmi che agiscono come "programmi decisionali che accettano prove valide"

Ma secondo il teorema di Rice, rilevare programmi che ha una proprietà specifica non è possibile.

Pensi che questa "ragione" abbia senso? Dal momento che questa non è una domanda matematica pura, spero di ascoltare le tue opinioni. Grazie.