andrejbauer
Section 4.8
Proposition 4.8.7 characterises the decidable predicates p : Pred(S) as those for which there is a decision procedure d : ∥S∥ → bool that takes a realiser for x to true if p(x) is realised and false otherwise.
Is this actually true? I think this only characterises the "weakly decidable" predicates, i.e. those for which ¬ p(x) ∨ ¬¬ p(x).
The proof does not convince me because of the phrase "Because a decidable predicate is stable". We are in the process of proving that p is decidable, so we can't use this fact yet. We know that the underlying set-predicate on |S| is stable, but this doesn't help us come up with a realiser for p(x) given ¬¬ p(x).
What I think this should say instead is that p : Pred(S) is decidable if and only if there is a d : ∥S∥ → ∥p∥ + unit that takes a realiser for x to a realiser for p(x) if there is one, and ⋆ otherwise.
