Definition of undecidability
Closed this issue · 3 comments
Dominik has brought up that the definition of undecidability we use is too strong, since some problems cannot be proved undecidable constructively. In particular, we can currently not prove synthetically that the complement of the halting problem is undecidable, but since some proofs of undecidability (like satisfiability of FOL) are by reduction from the complement of the halting problem. This is unsatisfying, because one can constructively show that the complement of the halting problem is non-synthetically undecidable if one uses a model of computation.
The easy way out is to define undec p := decidable p -> enumerable (compl Halt). This is also in line with the CPP '19 on synthetic undecidability (with the Entscheidungsproblem as example), where the undecidability axiom UA is introduced as ~ enumerable (compl PCP) (and we of course have enumerable (compl Halt) <-> enumerable (compl PCP). We would have undec_old p ->undec p, where undec_old is our current definition, so all current proofs are still valid.
As mentioned by Andrej, we could also use semi-decidability instead of enumerability in the definition. Since they are equivalent I'd advocate for choosing enumerability because I find synthetic enumerability easier to explain than synthetic semi-decidability.
I'm opening this issue so we can discuss this centrally and everybody can share their thoughts.
I am fine with alternate (ie lesser) definitions of undec. In retrospect, a great strength of the approach followed in the library, based on constructive (axiom free) reductions, is that it is mostly insensitive to changes in the definition of undec.
It is indeed annoying not being able to show undec P <-> undec ~P, but we also do not have dec P <-> dec ~P. I am not sure the proposed alternative allows that but it seem to be able to show more undec, typically undec ~Halt. Notice that under XM, the two definitions, undec_old and undec collapse to one (Halt being a predicate over a datatype).
The newly proposed undec is also stable under (many-one) reductions. What about the other reductions (truth table, Turing ...)?
The only drawback I find to the new undec is that changing the seed P := Halt in enumerable (~P) by another many-one equivalent one Q could affect the undec predicate. Apparently not in the case of switching Halt with PCP, but the reason does not seem to be many-one equivalence between Halt and PCP. Or may be I did not think enough about it...
After discussion with @dominik-kirst, he made me realized that P ⪯ Q entails ~P ⪯ ~Q (using the same many-one reduction function) and since enumerability is transported by reduction, this means enumerable (~P) <-> enumerable (~Q) as soon as P and Q are many-one equivalent. So I indeed did not think enough about it...
As the definition of undec proposed by @dominik-kirst is insensitive to the choice of a seed in the many-one class of Halt, I do not see any reason not to switch to this weaker characterization, but we should document this move and the reasons for it, may be in the README.md.
For the record, I am also in favor of undecidable p := decidable p -> enumerable (complement (HaltTM 1)) because of the previously initially mentioned reasons.
Though a weaker statement than undec_old, it is in spirit our goal, while still reasoning constructively.
Of course, the stronger statements are about the individual many-one reductions and are still around.
So I see no reason to keep undec_old at all, given the new definition.