The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello,

Here are some remarks about this.

First of all, if you have a proof that [forall n:nat, P(n)] then A
should always return true, therefore A = [fun x => true] should behave
as you wish. :)

I suspect however that this is not exactly what you are thinking about...

The standard way of dealing with decision procedure is to prove a
property like [forall n:nat, P(n) \/ ~P(n)]. This proof is indeed a
decision procedure if your did not use any axiom in its proof. Note it
is preferable to prove the variant [forall n:nat, { P(n) } + { ~P(n)
}], for technical reasons.

Best regards,
Pierre Courtieu





2014-09-29 17:31 GMT+02:00 Zhoulai.FU@Gmail 
<zhoulai.fu AT gmail.com>:
> Hello,
>
> I have little background in proof theory.  Here is a naive question that I
> am thinking about:
>
>  Let P denote a predicate over natural numbers. Suppose that I have a coq
> proof for  "forall n:nat, P(n)”. Then, can I establish a mapping A from
> natural numbers to {true, false},  so that for any natural number n,  A(n)
> is true if and only if P(n) can be proved?
>
> Otherwise, does some weaker guarantee holds for this mapping A, such as
> "for any natural number n,  A(n) is true implies  P(n) can be proved” ?
>
> Thank you for your ideas.
>
> Zhoulai Fu