Re: [isabelle] Proving equivalence



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





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