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.

Tjark,

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))"
oops

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 an inconsistency.

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))"
oops

even though Makarius has talked about quantifiers getting stripped away.

Thanks for the help,
GB







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