Re: [isabelle] How-to define a object logic

On Sat, 23 Dec 2006, Michael Nedzelsky wrote:

> I try to define the system S_1^0 of modal logic

> One thing which bother me is that the axioms are written like the 
> following
> ax_sub1: "PROP is_subst(P,Q,P,Q)"
> instead of simply
> ax_sub1: "is_subst(P,Q,P,Q)"
> Any suggestions and comments are highly welcome.

This is because is_subst yields prop, rather than "o" of the object-logic.  
Isabelle requires explicit syntax to indicate this situation -- by default 
the system inserts an object-logic judgment.  The PROP syntax allows to 
input pure propositions, but this markup is absent in output of 
applications involving a constant (which is assumed to provide its own 

The following declaration introduces a prop predicate with proper concrete 

  is_subst :: "[o,o,o,o] => prop"  ("(1IS'_SUBST/(1'(_,/ _,/ _,/ _')))")

  ax_sub1: "IS_SUBST(P,Q,P,Q)"
  ax_sub2: "IS_SUBST(P,Q,R,R)"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.