2
$\begingroup$

I will divide my question in two parts. The first part I am sure that there is a objective answer, but I am not sure about the second part.

First part: Is it all (decisions) problems trivial to prove decidable after assuming the Law of Excluded Middle (LEM)? e.g. There is no problem hard to prove decidable after assuming LEM.

Second part: Does make any sense to agree with a non-constructive proof that a problem is decidable?

Edit:

I will give an example of what I meant in the first part.

Consider the problem of deciding the eveness of a number. If I assume LEM, this problem can be easily proved decidable. There was no need to do the "hard" proof of building the decider.

Here is the demonstration in Coq of that:

Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_SS : forall n, even n -> even (S (S n)).

Axiom LEM : forall P : Prop, P \/ ~ P.

Lemma even_dec : forall (n : nat), even n \/ ~ even n.
  intros.
  apply LEM.
Qed.

The first part of my question was basically asking if this is always the case.

$\endgroup$
  • 1
    $\begingroup$ This seem to be more about the philosophy of mathematics than computer science. $\endgroup$ – Yuval Filmus Jul 4 at 7:25
  • $\begingroup$ I don't understand your first part. What do you mean by "hard to prove"? We certainly can't prove that all decision problems are decidable using LEM because, with the exception of people studying the nature of proof itself, everybody assumes LEM all the time, including in the many proofs that uncountably many languages are not decidable. So your first part seems to be "is it trivial to prove something false using LEM", to which the answer is presumably either "No" or "You didn't mean that." $\endgroup$ – David Richerby Jul 4 at 10:28
  • $\begingroup$ @DavidRicherby I added an example to my question. Does it help understand it? $\endgroup$ – Rafael Castro Jul 4 at 12:56
8
$\begingroup$

You are conflating computationally decidable with logically decidable.

A (closed) formula, $\varphi$, is logically decidable iff $\vdash\varphi$ or $\vdash\neg\varphi$, i.e. if $\varphi$ is derivable or $\neg\varphi$ is derivable (with respect to some given logical system). This is the sense we mean when we say something like the Continuum Hypothesis is undecidable.

A unary predicate on naturals, $P$, is computationally decidable iff there is a Turing machine $M$ which terminates on all inputs with output either $1$ or $0$, and $P(n)$ holds if and only if $M$ terminates with output $1$ on input $n$. This is the sense we mean when we say something like the Halting Problem is undecidable.

(There are other ways we use the term "decidable" such as when we say a(n entire) logic or theory is decidable which, more or less, means something like $\vdash\varphi_n$ is computationally decidable where $\varphi_n$ is a formula encoded by $n$ via some suitable surjective encoding.)

Assuming the Law of the Excluded Middle (LEM) doesn't automatically make every unary predicate on the naturals computationally decidable. Indeed, usually computational decidability is formulated within a classical logic where LEM holds.

Intuitionistic logic connects logical decidability to LEM because it satisfies the disjunction property which states $\vdash\varphi\lor\psi$ if and only if $\vdash\varphi$ or $\vdash\psi$. This means $\varphi$ being logically decidable is equivalent to $\vdash\varphi\lor\neg\varphi$.

Now, there's a model of intuitionistic first-order logic such that $\forall n:\mathbb N.P(n)\lor\neg P(n)$ is modeled by a computable function taking a natural and producing a witness of (the interpretation of) either $P(n)$ or $\neg P(n)$. This means (the interpretation of) $\forall n:\mathbb N.P(n)\lor\neg P(n)$ is true in this model if and only if $P$ is computationally decidable. LEM, in this context, would imply the statement that all decision problems are computationally decidable. LEM is, of course, false in this model. Therefore, if you assume LEM, this interpretation ceases to be a model.

The fact that certain formulas are derivable in intuitionistic first-order logic implies that corresponding predicates are computationally decidable. This implication itself, though, is demonstrated in the meta-logic where the definition of "computationally decidable" resides, and this is usually a classical logic.

For an informal (meta-)logic in which you define "computationally decidable", it's up to you whether you want to accept non-constructive proofs or not. However, there is a big difference between proving a formula in constructive logic which can be interpreted as a witness to the computational decidability of a predicate, and proving a formula which states in the constructive logic that a predicate is computationally decidable which would involve constructive definitions of Turing machine and so forth. As an analogy, the circle as a (higher inductive) type in Homotopy Type Theory is very different from the construction of cirles, e.g. $\mathbb R/\mathbb Z$ within Homotopy Type Theory. As a more contrived example, let's say I interpret the theory of abelian groups into $3\mathbb Z$, i.e. $1$ is interpreted as $3$. Then it is still the case that the "internal" notion of $3$, i.e. $1+1+1$, is different from $1$.

$\endgroup$
  • $\begingroup$ I added an example to my question. My example is about "logically decidability", right? $\endgroup$ – Rafael Castro Jul 4 at 13:08

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.