Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Andreas Abel <andreas.abel AT ifi.lmu.de>
  • To: Gyesik Lee <gyesik.lee AT aist.go.jp>
  • Cc: Vincent Aravantinos <vincent.aravantinos AT gmail.com>, Robin Green <greenrd AT greenrd.org>, 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 12:56:46 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

The formula in the subject line is the rule of replacement

  http://www.philosophypages.com/lg/e11b.htm

therefore it should be valid in sensible interpretations of propositions. It is not provable in Coq as such.

But one can define a small universe of propositions, like formulas in propositional logic.

  Inductive prop (A : Set) : Set

where A ranges over propositional variables.
Then one can define interpretation

  Fixpoint eval (A : Set) (p : prop) (rho : A -> Prop) : Prop

of formulas into true propositions and prove

  Theorem replace :
    forall rho rho', (forall a, rho a <-> rho' a) ->
    forall p, eval A p rho <-> eval A p rho'.

by induction on "small" propositions (p : prop).


Wrt. to Goedelization: The replacement rule is not affected by Goedelization. What you can disprove is

  A <-> B -> (F 'A' <-> F 'B')

where 'A' means the Goedel code (= "syntax") of A.

I think there are good reasons in Coq why you cannot eliminate on Prop.

Cheers,
Andreas


Gyesik Lee wrote:
On Thu, Feb 14, 2008 at 7:36 PM, Vincent Aravantinos
<vincent.aravantinos AT gmail.com>
 wrote:
 > 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, I think Vincent is right.

Assume we have given a syntactic definition of the syntax of a
first-order language.
Then the set of formulas has the decidability of syntactic equality
among formulas.

And then one can use the idea given by Vincent in order to construct a
counter example as the following: (assuming Prop = the set of
formulas)

Given  A B : Prop, define f : Prop -> nat by

f (A) = 0 and f (P) = 1 for P <> A  (the equality means syntactical equality).

i.e. f (B) = 1,

and g : nat -> Prop by

g (n)  :=    n < 2

Then

F (A) = g ( 1+ 0) = 1 < 2

but

F (B) = g( 1+1) = 2 < 2.

Hence we don't have F (A) -> F(B) independent of A and B.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club



--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/





Archive powered by MhonArc 2.6.16.

Top of Page