coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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/
- [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 ?,
Gyesik Lee
- 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
Archive powered by MhonArc 2.6.16.