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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and