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.

  • $\begingroup$ What does "detect" mean here? Are you asking: is there an algorithm for deciding whether a sentence is decidable, i.e., a machine $T$ such that $T(x)$ rejects if $x$ encodes a decidable sentence, and accepts if $x$ encodes an undecidable sentence? $\endgroup$ – Andrej Bauer Jul 14 '19 at 9:16
  • $\begingroup$ @Andrej Bauer I mean a machine T such that T(x) accepts x if x encodes a sentence which "means" an undecidability of another sentence, and rejects otherwise. $\endgroup$ – user9730905 Jul 14 '19 at 9:20
  • 1
    $\begingroup$ Now you have to explain "means" :-) $\endgroup$ – Andrej Bauer Jul 14 '19 at 9:22
  • $\begingroup$ Let me try: a machine $T$ such that $T(x)$ decides whether $x$ encodes a statement $\phi$ such that there exists a sentence $\psi$ such that $\phi$ is logically equivalent to the sentence $\forall n . \lnot \mathrm{Prf}(\ulcorner \psi \urcorner, n) \land \lnot\mathrm{Prf}(\ulcorner \lnot\psi \urcorner, n)$ (read as "$\psi$ is undecidable"). $\endgroup$ – Andrej Bauer Jul 14 '19 at 9:25
  • 1
    $\begingroup$ I think I've given sufficient comments and advice to point out that the question is unclear because it is insufficiently formal, as well as that there is absolutely no problem with making it formal. But as long as you do not settle with one formal version, there is nothing to answer here. Yes, in logical equivalence is hard, but that has nothing to do with posing the question. It may be important for the answer. So, what is the question? $\endgroup$ – Andrej Bauer Jul 14 '19 at 14:22

The question is unclear with respect to how exactly it is supposed to be formalized. But formalized must it be because it is asking about the ability of Turing machines to perform certain tasks. So I am going to go ahead and formalize is as best as I can.

Let ZFC be the first-order theory of Zermelo-Fraenkel set theory. We are going to use it as the meta-theory, which is an overkill as a much weaker theory would do. The important thing is that ZFC is powerful enough to be able to talk about first-order languages.

We fix an acceptable numbering of formulas and proofs using natural numbers. Note that the acceptable encodings are all computably isomorphic and nothing changes if we use a different one. So, given a syntactic object $\phi$ (such as a formula), let $\ulcorner \phi \urcorner$ be its code for the given fixed encoding.

The OP speaks about "decidability theorems" and wonders whether there is a formal way of writing down what they are, so let us deal with this first. It is routine to produce first-order formulas in the language of ZFC that express the following:

  • $\mathrm{Signature}(x)$ expresses: $x$ encodes a signature for a first-order language.
  • $\mathrm{Theory}(x, y)$ expresses $\mathrm{Signature}(x)$ and $y$ encodes a first-order theory (with a decidable set of axioms) in the language over the signature encoded by $x$
  • $\mathrm{Prf}(x,y,z,p)$ expresses the fact that $\mathrm{Theory}(x,y)$ and that $p$ encodes a first-order proof in the theory encoded by $y$ of the statement encoded by $z$.

We now have any number of possibilities to formally define what a "decidability theorem" is, and the OP may entertain themselves by exploring the possibilities. To my mind the foloowing is a reasonable definition:

Definition: Let $\mathrm{UndecThm}(x, y, z)$ be the formula which expresses the fact that $\mathrm{Theory}(x, y)$ and that $z$ encodes a formula in the language encoded by $x$ of the form $$\forall p \,.\, \lnot \mathrm{Prf}(x, y, \ulcorner \phi \urcorner, p) \land \lnot \mathrm{Prf}(x, y, \ulcorner \lnot\phi \urcorner, p)$$ for some sentence $\phi$ (in the language encoded by $x$).

Note: one might be tempted to say that if $A$ is an "undecidability theorem" and $A \iff B$ then $B$ is an undecidability theorem as well, but this is not the case. Logical equivalence does not preserve meaning! For example, $A$ might be a undecidability theorem which is true (or provable, if you care about the difference), therefore equivalent to $2 + 2 = 4$, but nobody would claim that $2 + 2 = 4$ is an undecidability theorem.

We may now observe that $\mathrm{UndecThm}(x, y, z)$ is decidable in $x$, $y$ and $z$, quite obviously, as we only need to check that $x$ correctly encodes a signature, that $y$ correctly encodes a first-order theory, and that $z$ indeed encodes a sentence of the form, as given given in the above definition.

The question was whether "machines can detect undecidability theorems". The answer is positive, since $\mathrm{UndecThm}(x, y, z)$ is decidable. Any number of variations on the theme will have a positive answer as well, because one simply has to check that a given code encodes a certain syntactic form. For example, if you slightly vary your notion of "undecidability theorem" nothing will change.

  • $\begingroup$ Very nice! Thank you so much. $\endgroup$ – user9730905 Jul 14 '19 at 14:52
  • $\begingroup$ I am glad I understood the question correctly. $\endgroup$ – Andrej Bauer Jul 14 '19 at 14:55

Humans have found undecidability theorems. There is no reason known why an artificial intelligence cannot be built that matches what humans can do intelligence wise (although what is currently fashionable seems to be just pattern matching on a massive scale, which is not going to get you very far), therefore there is no reason known why an artificial intelligence, that is a machine, cannot find undecidability theorems.

  • $\begingroup$ Well, of course, if a machine mimic our brains, it can. But it would be a cluster of neural network, which says "it seems to be undecidability theorem, with probability xx.xx%", not a deterministic algorithm. Think of a Turing machine. Do you think it's possible? $\endgroup$ – user9730905 Jul 14 '19 at 12:08
  • $\begingroup$ Can humans do it? $\endgroup$ – gnasher729 Jul 14 '19 at 12:41
  • $\begingroup$ I don't know, but I've never heard about exact criterion for "undecidability theorem". If we can make an exact criterion, maybe there is a Turing machine doing the same thing. But because of the reason I wrote above, it seems not to be a case. The question is, whether my reasoning makes sense. $\endgroup$ – user9730905 Jul 14 '19 at 12:49
  • $\begingroup$ The exact criteorion for an undecidability theorem is: it is a theorem which states that a sentence is neither provable nor refutable relative to some formal system. This can be previsely formulated in great generality, and formalized. Stop insisting that there is a mystery and instead try to understand our reasons when we explain that there is no mystery. $\endgroup$ – Andrej Bauer Jul 14 '19 at 13:29

I'm not sure I completely understand what you mean. But it looks like just a common misconception.

When we say X is undecidable, it means it isn't possible to find an algorithm that could always generate the correct output for every valid input. But it's possible for an algorithm to generate the correct output only for some inputs, while giving a third result in case it doesn't know the answer.

Likewise, in Rice's theorem, it isn't possible to find an algorithm that could correctly decide whether a program has a specific property for every program. But it's perfectly possible to find an algorithm that could only decide whether each one in a carefully chosen subset of the programs has a specific property.

There are undecidable problems that we could never prove it's undecidable using a certain axiom set. (Say, accept if either the input program halts on empty input, or ZFC is inconsistent.) We could only know some of the undecidable problems are undecidable. So could an algorithm. An algorithm could not "decide" whether a problem is undecidable, or whether a program accepts iff the input is a valid proof, in the sense that such an algorithm cannot always work for any input problem or program. Neither could us.

  • $\begingroup$ As you mentioned, an algorithm can't decide whether a problem accepts iff the input is a valid proof. But if there is a machine accepts undecidability theorems only, it should do that. Hence I think it's impossible. Does it sound? $\endgroup$ – user9730905 Jul 14 '19 at 21:07
  • $\begingroup$ @user9730905 It's impossible for a machine to accept every true statement about undecidability. But it's possible for a machine to accept some true statements about undecidability, and gives a third result that is neither accept or reject for some statements. And this is also exactly what humans could do. $\endgroup$ – user23013 Jul 15 '19 at 1:55
  • $\begingroup$ Now I got it. Thank you. $\endgroup$ – user9730905 Jul 15 '19 at 9:29

Not the answer you're looking for? Browse other questions tagged or ask your own question.