Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)
It sort of escaped my notice that although I have
"(!C.!D.(C | D --> C)) --> (A | B --> A)"
I also have anything else I want to prove, for the simple fact that the
hypothesis is always false.
"(!C.!D.(C | D --> C)) --> P a"
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
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