Email Gateway (Aug 18 2022 at 10:02): Email Gateway (Aug 18 2022 at 10:02):From: Michael Nedzelsky <MichaelNedzelsky@yandex.ru>
Hi all.
I try to define the system S_1^0 of modal logic (according to "Modal Logics"
by Robert Feys) in order to learn the process of adding a new object logic.
Current version is at:
http://www.myjavaserver.com/~nedzelsky/isabelle/ModalS1_0.html
One of the rules of S_1^0 is EQS (substitution of strict equivalents).
I feel my attempt to formalize it is not very satisfactory. 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.
Regards,
Michael Nedzelsky
Email Gateway (Aug 18 2022 at 10:02):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 04:19 UTC