The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Yes. Because P hold of all natural numbers, this mapping A is just the
constant function true:

Section Foo.

Variable P : nat -> Prop.
Hypothesis P_is_true : forall n, P n.

Definition A : nat -> bool := fun _ => true.

Lemma l : forall n, A n = true <-> P n.
Proof.
  intros n.
  split.
  - intros _. apply P_is_true.
  - reflexivity.
Qed.

End Foo.

2014-09-29 11:31 GMT-04: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



-- 
Arthur Azevedo de Amorim