The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Hello,

Vincent Aravantinos wrote:
>
> Le 14 févr. 08 à 11:26, Robin Green a écrit :
>
>> On Thu, 14 Feb 2008 10:54:17 +0100
>> Vincent Aravantinos 
>>Â <vincent.aravantinos AT gmail.com>
>>  wrote:
>>
>>> Assume you are given two functions (f:Prop -> nat) and (g:nat ->
>>> Prop), and then define a F like this:
>>>
>>> Definition F (P:Prop) : Prop -> Prop := g (1 + f P).
>>>
>>> I don't see any reason why such a function would respect your
>>> conjecture.
>>
>> But how can you define a function f : Prop -> nat which yields
>> different numbers for different propositions, in Coq? You can't do case
>> analysis on Props.
>
> I think we don't matter if we can't define it in Coq: as soon as we
> can define it mathematically, the property is false (and thus should
> not be provable in Coq).
>
> I was actually thinking of a kind of godelisation to define f, if we
> restrict to first order formulas.
>
Yes, but this cannot be done in Coq without axiom.

In fact, Gang Chen's property (GC) is equivalent to propositional
extensionality
PE : forall A B: Prop,(A<->B)->A=B.

Obviously PE -> GC.
GC->PE is also provable:
Axiom equiv : forall (F : Prop->Prop) (A B : Prop), (A<->B)->((F A)<->(F
B)).
Goal forall A B, (A<->B) -> A=B.
intros.
elim (equiv (fun P => P=B) _ _ H); intros.
auto.
Qed.

PE is (believed) consistent with Coq since there is (but this is not
formally established yet) a boolean model of Coq (i.e. where Prop is
interpreted by booleans), and PE is valid in this model.
(And this shows that the godelisation above cannot be effective without
axiom.)

However PE is (believed) not provable, because there is also an
intuitionistic model of Coq (but this is not formally established yet).
You could think of it as assuming that Prop and Set are indeed the same
sort. In that case, GC(Prop:=Set) does not hold:
take F X := { x:X| forall y:X, x=y}  (X has exacly one inhabitant).
unit <-> bool since they are both inhabited.
(F unit) holds but (F bool) does not (true<>false).

Bruno Barras.