Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
On Tue, 2012-09-11 at 15:07 -0500, Gottfried Barrow wrote:
> "~((A --> B --> A) --> (A <-> B))"
> "(A --> B --> A) --> (A <-> B)"
> "~(!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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and