The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 2013-05-27 15:19, Floyd Lee wrote:
> Parameter A     : Type.
> Parameter P     : A -> Prop.
> Parameter Q     : A -> Prop.
> Parameter P_dec : forall (x : A), {P x}+{~P x}.
> Parameter Q_dec : forall (x : A), {Q x}+{~Q x}.
> 
> Definition R :=
>   (exists r, P r /\ Q r).
> 
> (* Both P and Q are decidable, so R should be too. *)
> Theorem R_dec : {R}+{~R}.

No, unless the type A is finite.

Example: let TM be an arbitrary Turing machine and take

         A = nat
         P = fun n => TM is halted after n steps
         Q = fun n => True

P x is clearly decidable (just run TM for n steps and check whether it
is halted), but R is equivalent to "TM halts", so deciding R (for an
arbitrary TM) would be solving the halting problem.

- Xavier Leroy