*To*: s.wong.731 at gmail.com*Subject*: Re: [isabelle] Proving equivalence*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 25 Jan 2011 14:15:30 -0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Tjark Weber <webertj at in.tum.de>*In-reply-to*: <001636458a36921009049ab2c895@google.com>*References*: <0016e6dbe2b3231679049ab23ee9@google.com> <001636458a36921009049ab2c895@google.com>*Sender*: huffman.brian.c at gmail.com

On Tue, Jan 25, 2011 at 1:56 PM, <s.wong.731 at gmail.com> wrote: > Actually, proving "(0::real) = 1" using that as a fact doesn't make it > inconsistent, right? It just means that it has at least one unsatisfying > model. If "False" can be derived as a theorem from some set of axioms, then any proposition can be derived as a theorem, and so by definition that set of axioms is inconsistent. Note that my proof of "(0::real) = 1" from ax1 did not rely on any extra assumptions about the constants "foo", "bar", etc. so the proof applies to *all* potential models. - Brian

**References**:**Re: [isabelle] Proving equivalence***From:*s . wong . 731

**Re: [isabelle] Proving equivalence***From:*s . wong . 731

- Previous by Date: Re: [isabelle] Proving equivalence
- Next by Date: [isabelle] Inconsistent axioms?
- Previous by Thread: Re: [isabelle] Proving equivalence
- Next by Thread: Re: [isabelle] Proving equivalence
- Cl-isabelle-users January 2011 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