The Coq mailing list

[like <12like34xiongmao AT 163.com>]

Hi, Pierre Casteran: 

Because the semantic of the 'prj' temporal operator in our 
logic is really complicated. We just want to embedding the
 pure axiomatic system in Coq, not the model system. 
If I define derviable in Fixpoint,it will invlove semantic.
 Can you give me an example about what kind of
axioms I needed for expressing the
relationship between derivability and the constructors of formulas. 

(ps:I also read a lot of papers about logic embedding in theorem prover.
 Up to now,all the embedding are in model theory invovled semantics.
 None of it like this.)
 Thanks for your help,  I came to see my problem from your answer.