Re: [isabelle] Wanting only ==>, prop, and schematic variables; but not so



It's not exactly all there, but starting on page 27 of isar-ref.pdf, there is section "2.1 The Pure Framework", in which a brief explanation of the four meta-logic symbols is given, where the four symbols are =>, \<And>, \<equiv>, and ==>. It pays to look at things 4 or 5 times, at least.

In particular, on page 28, it says, "Logical statements are composed via \<And>x::alpha. B(x) and A ==> B." It then goes on to define some rules for \<And> and ==> using sequents.

That's important because there is the section "Simulating sequents by natural deduction" on page 203 which talks about expressing a form of sequents using the ==> symbol.

You put those sections together, and you might be able to figure how to use ==> to have a form of sequents in Isabelle/HOL where ==> is considered the fundamental symbol for the sequents, and figure out how to do it without abusing conventional standards too much.

You might call them isa-sequents. If you abuse things unintentionally, an isa-sequent is whatever you define it be anyway.

Regards,
GB




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