The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 08/29/2012 09:09 PM, like wrote:
> 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.
>    

This is certainly a fairly unusual choice in Coq formalization.  
However, I'd be careful about thinking of this as meaning that you have 
an unusual problem domain that demands unusual encoding.  I would 
recommend thinking hard about how to formalize your logic without axioms.