The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

zaman wrote:
> I wish to say that "A component term must be either a client or server of a
> connection; but not both." I have come up with the following as a 
> representation
> of the above in the coq (based on my definition above):
>
>      (forall con:Connector, forall c:Component, In con (MyConnections x) ->
>      (c = (client con) /\ c<>  (server con)) \/ (c<>  (client con) /\ c = 
> (server
> con)))
>    

The form of this theorem is suspicious.  You have a quantified 
implication whose conclusion mentions [c] but whose assumption does 
not.  Thus, in terms of determining the value of [c], the only help the 
assumption [In con (MyConnections x)] may be is if it is contradictory, 
in which case any conclusion follows.

Your question seems to be more about first-order logic than about Coq in 
particular.  Do you believe you can formulate everything on paper in 
traditional first-order logic?  (I expect the theorem statement above is 
not a desirable part of such a formulation.)