The following question assume that the decision problem definition (syntactic) has been written (and could be changed if it isn't able) to catch a concept (meaning, semantic) which has both nice implications and some models. So please don't answer "the definition is the definition".

Let be any usual proof system, let $x$ be an object and let $P_{x}$ be a property. By Gödel incompleteness theorem, there are 3 cases :

  1. $P_x$ is true and there is a proof for this.
  2. $P_x$ is false and there is a proof for this.
  3. $P_x$ is unprovable and there is neither a proof of trueness nor a proof of falseness.

But, regardless those 3 cases, a decision problem is defined by its set of positive instances (which hasn't even to match with 1.). Consequently, we must give truth value (positiveness/negativeness) to statements which don't have any in our proof system, I know that such a completion isn't inconsistent but it doesn't make much sense in my opinion.

Defining a decision problem constructivly, the decision problem would be just the target property, would make more sense. What could be the problems of such an approach ?

  • 2
    $\begingroup$ 1) Gödel's theorem does not apply to all proof systems. 2) How do we have interpret "nice implications" and "some models"? 3) Unprovable != no truth value. Decision problems are defined in a non-constructive fashion; we can define properties for which sometimes no proofs exist, c.f. halting problem (where proof means "the finite computation of an algorithm deciding the problem" here). 4) I have trouble understanding what you are asking. The "standard" definition of decision problems is rather clear. Can you give a formal definition of what you are proposing? $\endgroup$ – Raphael Jul 2 '15 at 14:39
  • 2
    $\begingroup$ I think you misunderstand the meaning of "constructive". You are confusing it with "provable", as far as I can tell. $\endgroup$ – Andrej Bauer Jul 2 '15 at 18:37
  • 1
    $\begingroup$ It is meanigful to ask for a construction if a yes/no algorithm for any property. But it may happen that there is no solution because the property in question is not decidable. According to your philosophy, a question is meaningless if it does not have an answer. $\endgroup$ – Andrej Bauer Jul 2 '15 at 18:39
  • 2
    $\begingroup$ It has an answer! The answer is negative: the problem is not decidable. $\endgroup$ – Andrej Bauer Jul 2 '15 at 19:13
  • 1
    $\begingroup$ Also, witness is not the same thing as proof. A witness can be infinite. It can be non-syntactic in nature, for instance topological. Consider for example sheaf-theoretic models of constructive mathematics. Or topological realizability. $\endgroup$ – Andrej Bauer Jul 2 '15 at 19:14

A decision problem is a question of the form:

Does $x$ have property $P$?

A solution to such a problem is a Turing machine $T$ such that:

  1. For all $x$, $T(x)$ terminates.
  2. If $x$ has property $P$ then $T(x)$ outputs true.
  3. If $x$ does not have property $P$ then $T(x)$ outputs false.

Notice how formal systems play no role in the above. We are asking for a machine to corectly determine whether $P(x)$ is true. (The other possibiity is that $P(x)$ is false, and there is no third options, if you believe in excluded middle.) We did not ask for the machine to find a proof of $P(x)$! You should make sure to understand the difference between truth and provability.

There is an important class of decisions problems which have no solutions because of Gödel's incompleteness theorem. For instance, the decision problem

Does formula $\phi$ have a proof in Peano arithmetic?

has no solution because there is no Turing machine that will correctly answer the question for all formulas $\phi$.

But in general decision problems are not directly linked to provability. For instance, the Halting Problem "does Turing machine $T$ stop on input $x$?" has nothing to do with any formal system. It is a question about machines.

  • $\begingroup$ "Formal systems play no role in the above" but when you said "x has the property" it's regarding a proof system or some axiomatic theory. I don't believe in the excluded middle, I am asking for a constructive decision problem definition. I edit my question. $\endgroup$ – François Jul 2 '15 at 16:37
  • 4
    $\begingroup$ I most definitely did not ask for a proof when I said "$x$ has property $P$"! It is essential that you understand the difference between "is true" and "has a proof". A statement which has a proof is true, but not every true statement has a proof. Proofs are a way of verifying that something is true and they are not the same thing as truth. Even if you do not believe in excluded middle, the definition of decision problems still stands and it has nothing to do with provability. $\endgroup$ – Andrej Bauer Jul 2 '15 at 18:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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