coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?

From: Vincent Aravantinos <vincent.aravantinos AT gmail.com>
To: Robin Green <greenrd AT greenrd.org>
Cc: gang chen <gangchen_sh AT yahoo.com>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?
Date: Thu, 14 Feb 2008 11:36:26 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=in-reply-to:references:mime-version:content-type:message-id:cc:content-transfer-encoding:subject:date:to:x-mailer:from; b=D11yCtYBmQSyJXnGKkzLQiPST41GTmEg0Nl34yFrbaIiPDsoKqpkquWWleYoWh+i2MLjwV9gcQzy2rU9RdrkPE3j1Uz4gz828SHzpp2tefEedVMCk475neXI8Wp7NUV4YvkyLssCXLvDO2xLq732VN+5NTxckoicCpLa+VEGapw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

Vincent

[Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, gang chen
- Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Vincent Aravantinos
  - Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Robin Green
    - Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Vincent Aravantinos
      - Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Gyesik Lee
        
        Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Andreas Abel
      - Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Bruno Barras
        
        Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, Conor McBride
        
        Re: [Coq-Club] is "(A<->B)->((F A)<->(F B))" provable ?, gang chen