*To*: Josh Tilles <merelyapseudonym at gmail.com>*Subject*: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default*From*: "Elsa L. Gunter" <egunter at illinois.edu>*Date*: Sat, 20 Dec 2014 21:12:13 -0600*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CAGTcTFygtwufnmF7_0dD3hbViLXubfh5Tp0twYkHQPcJOdADSA@mail.gmail.com>*References*: <CAGTcTFw5QbLPQ_YaSzmT5uXLgVjuyo6vnKNrmEJcGrzfEYCh=A@mail.gmail.com> <425E3845-D343-40DD-ADCA-81E49E4C6375@cam.ac.uk> <CAGTcTFzPk4XsjKFcQenDqPR5xE84VO9ihb8uEEQSKSzU1vkT=A@mail.gmail.com> <alpine.LNX.2.00.1412152100540.30515@lxbroy10.informatik.tu-muenchen.de> <CAGTcTFygtwufnmF7_0dD3hbViLXubfh5Tp0twYkHQPcJOdADSA@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.3.0

Dear John, On 12/20/14 8:06 PM, Josh Tilles wrote:

The primary reason is actually a sequence of ideas: - I try to prove things in Isabelle (versus proving them on paper) as much as possible; - I'm reading John L. Bell's *A Primer of Infinitesimal Analysis *and would like to do the exercises (in Isabelle); - and (apparently) Infinitesimal Analysis is *incompatible* with classical logic. - For example, a fundamental principle is that "The set of magnitudes 𝜀 for which 𝜀^2 = 0 —the *nilsquare infinitesimals*— does not reduce to {0}." And yet the following lemma is easily provable in Isabelle/HOL (having imported only Fields and Set): lemma "{0} = {x::'a::field. x * x = 0}" by simp So, to *my* understanding, there's no way to do the exercises in Isabelle without introducing inconsistency.

---Elsa

**Follow-Ups**:**Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default***From:*Josh Tilles

**References**:

- Previous by Date: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
- Next by Date: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
- Previous by Thread: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
- Next by Thread: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
- Cl-isabelle-users December 2014 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