# 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
syntax).
The following declaration introduces a prop predicate with proper concrete
syntax:
consts
is_subst :: "[o,o,o,o] => prop" ("(1IS'_SUBST/(1'(_,/ _,/ _,/ _')))")
axioms
ax_sub1: "IS_SUBST(P,Q,P,Q)"
ax_sub2: "IS_SUBST(P,Q,R,R)"
Makarius

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