Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)

It sort of escaped my notice that although I have

theorem --"(4)"
  "(!C.!D.(C | D --> C)) --> (A | B --> A)"
by auto

I also have anything else I want to prove, for the simple fact that the hypothesis is always false.

theorem --"(4a)"
  "(!C.!D.(C | D --> C)) --> P a"
by auto

This could be material for my book, "How to Learn Basic Logic with Isabelle", or with the type of title I always hate, "Logic for Dummies with Isabelle2012".

It still appears that free variables aren't quantified, although my reasoning might be warped. It may not be warped. If I just know what's true, then I can sometimes straighten out my reasoning.

This is my first use of Isabelle as a tool to confirm some basic logic. No one else is going to take any substantial time to clarify and remind me of the basics that I mostly understand. There's nothing wrong with that.


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