Re: [isabelle] I need a meta-or

On 7/31/2013 3:29 PM, Makarius wrote:

Trueprop priority is 5, so dealing with the syntax of functions of type "prop => prop" and "prop => prop => prop" is tricky:

  Trueprop :: "bool => prop"   ("(_)" 5)

If you want to play with syntax, you can always use 'notation' and 'no_notation' to specify things in any way you like, but don't ask me about suitable priorities -- this is a black art and better not changed fundamentally.

Reminder to self. Add the following to the official GB list of HOL cardinal rules: "Never change the default settings of Trueprop priority. Live within the limits of Trueprop priority being at 5, lest you cause yourself or others great logical harm in the future."

Generally, Isabelle/Pure is not really a meta-logic, i.e. a logic to reason about other logics. It is just a logical framework, for higher-order natural deduction based on !! and ==>.

If you really want to reason about some other logic, better do it in Isabelle/HOL, and define you syntax as datatype, semantics as function, inference system as inductive predicate in the usual way. AFP has examples for that.

In these technical matters, I'm a practical purist. I'm only interested in logics other than HOL to the extent they help me understand isar-ref.pdf, and other Isabelle documentation. I also want there to be the possibility that I can use anything I do as part of HOL. I'm just a user who delves into foundations because I never found the book "Set Theory, Real Analysis, Algebra, Combinatorics, and Number Theory for Maple, Mathematica, and Even Isabelle2013".

I decided to take a step back and finally study natural deduction. However, natural deduction inevitably leads to sequents, so I have wanted to create a psuedo-sequent to use with exercises and, in some manner, really be using a metalanguage.

With the pseudo-sequent I have now, there is the possibility that it will all end up being academic, where I end up only using the standard natural deduction rules. There is also the possibility that I will eventually find a use for the pseudo-sequent, or at least for the notation.

I have no idea at this point why the RHS of a sequent needs to behave as a disjunction, or why a person needs more than what the natural deduction rules provide. But, it could be that I find a practical use for stating a theorem using a meta-or along with !! and ==>. Sometimes, we do that kind of thing as a preliminary step, because it helps us sort out foggy concepts.

Thanks for the help, and thanks to Lars for the info about PROP.

I got my meta-False down to "(!!P. P::bool)". If I could roam the halls of CMU, I'd stop by Avigad's office, make sure I called him professor, and ask him if I can get a meta-False without using !!.


notation ==> (infixr "|-" 4) (* ==> and |-, they're close relatives. *)
notation ==> (infixr ",," 4) (* Fake sequent comma. It's all ==> on the LHS. *)

(*Warning!! What's below could all be bogus.*)

(*Meta False. Trying to use "PROP P" instead of "P::bool" causes some looping below. It's no loss. If automatic Trueprop coercion is used, there's no extra
  purity obtained from using "PROP P".

It looks like I'm only tied into the object-logic because of these statements:
    typedecl bool
    judgment Trueprop :: "bool => prop",
  though probably also to the arities statements right above them.*)

abbreviation MFalse :: "prop" ("MFalse") where
  "MFalse == (!!P. P::bool)"

theorem meta_False:
  "MFalse == (Trueprop False)"
by(rule equal_intr_rule, auto simp only:)

(*Meta not.*)
abbreviation (input) meta_not_abbr :: "prop => prop" ("([~]_)" 40) where
  "meta_not_abbr P == (PROP P ==> MFalse)"

theorem meta_not:
  "([~]P) == Trueprop (~P)"
by(rule equal_intr_rule, auto simp only:)

(*Meta or.*)
abbreviation (input) meta_or_abbr :: "prop => prop => prop" (infixr "([|])" 4) where
  "meta_or_abbr P Q == ((PROP P ==> MFalse) ==> PROP Q)"

theorem meta_or:
  "(P [|] Q) == Trueprop (P | Q)"
by(rule equal_intr_rule, auto simp only:)

(*Meta and.*)
abbreviation (input) meta_and_abbr :: "prop => prop => prop" (infixr "([&])" 4) where
  "meta_and_abbr P Q == ((PROP P ==> (PROP Q ==> MFalse)) ==> MFalse)"

theorem meta_and:
  "(P [&] Q) == Trueprop (P & Q)"
by(rule equal_intr_rule, auto simp only:)

(*Meta exists. I don't feel like looking up how to do the binder notation right now. The presence of implicit meta-quantification always leaves one paranoid.
  You do the pencil and paper scratch work 15 times, but because you cannot
stop by Avigad's office to get confirmation of the obvious, and because you have used up your bi-monthly mailing list quota for asking questions, you never
  rest easy.*)
theorem meta_exists:
  "((!!x. P x ==> MFalse) ==> MFalse) == Trueprop (? x. P x)"
by(rule equal_intr_rule, auto simp only:)

(*Finally, the pseudo-sequent. The order of the arguments on both the LHS and RHS don't matter, and there's actually a meta-language operator being used
  that's not HOL disjunction.

The priorities of the commas, |-, and [|] are all at 4, so they nest to the right, which means I don't have to use parentheses for the turnstile statement.
  The ==> is at priority 1 so the parentheses have to be used as shown.*)

  "  (P,, Q |- (~E ==> ~C ==> ~D ==> B))
  == (Q,, P |- E [|] B [|] C [|] D)"
by(rule equal_intr_rule, auto simp only:)

  "  (P,, Q |- (~E ==> ~C ==> ~D ==> B))
  == (Q,, P |- D [|] E [|] B [|] C)"
by(rule equal_intr_rule, auto simp only:)

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