The Coq mailing list

["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