The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

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/