Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
On 9/11/2012 4:17 PM, Tjark Weber wrote:
I believe a more helpful insight here is simply that a formula with
free variables may be contingent (i.e., its truth value may depend on
the interpretation of the free variables, so that neither the formula
nor its negation are theorems), while a formula without free variables
is either true or false.
See http://en.wikipedia.org/wiki/First-order_logic (especially the first
three sections) for further background.
I think I'm straightened out, but the least little difference in what
people say can make me wonder if I'm straightened out.
I think what confused me is that I was assuming that how Nitpick uses a
formula in a theorem, such as,
theorem "~((A --> B --> A) --> (A <-> B))"
is the same way the prover engine uses it. (I still wouldn't know what
the software is doing.)
If you had said before my email, "GB, the truth value of '~((A --> B -->
A) --> (A <-> B))' cannot be determined until you assign truth values to
A and B", then at worst, I would have said, "Tjark, I remember that now.
I used to be so good at thinking in terms of truth tables before
Isabelle started overloading me with information."
Anyway, I always get a little extra out of these exchanges, even if I
don't start them off right.
Whatever is actually happening in Nitpick's engine and the provers
engine, I now know that with free variables, I can consider that Nitpick
is checking a "theorem" like this:
definition false_formula::"bool => bool => bool" where
"false_formula A B == ~((A --> B --> A) --> (A <-> B))"
value "false_formula True True" (*Output panel: "False" :: "bool" *)
That helps a lot, because I was in this mindset that when Nitpick found
counterexamples for both a "theorem" and its negation, that it had found
On the other hand, I now consider that the prover engine has converted
my theorem above to
theorem "!A B. ~((A --> B --> A) --> (A <-> B))"
even though Makarius has talked about quantifiers getting stripped away.
Thanks for the help,
This archive was generated by a fusion of
Pipermail (Mailman edition) and