Re: [isabelle] Thanks Nitpick for actually answering a former, simple question



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







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