*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question*From*: Tjark Weber <webertj at in.tum.de>*Date*: Tue, 11 Sep 2012 23:17:47 +0200*In-reply-to*: <504F99E9.8060608@gmx.com>*References*: <504F99E9.8060608@gmx.com>

On Tue, 2012-09-11 at 15:07 -0500, Gottfried Barrow wrote: > theorem > "~((A --> B --> A) --> (A <-> B))" > oops > > theorem > "(A --> B --> A) --> (A <-> B)" > oops > > theorem > "~(!A. !B.(A --> B --> A) --> (A <-> B))" > by auto 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. Best regards, Tjark

**Follow-Ups**:**Re: [isabelle] Thanks Nitpick for actually answering a former, simple question***From:*Gottfried Barrow

**References**:**[isabelle] Thanks Nitpick for actually answering a former, simple question***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Next by Date: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Previous by Thread: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Next by Thread: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Cl-isabelle-users September 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list