*To*: "Elsa L. Gunter" <egunter at illinois.edu>*Subject*: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default*From*: Josh Tilles <merelyapseudonym at gmail.com>*Date*: Sat, 20 Dec 2014 23:53:51 -0500*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <54963A8D.2090707@illinois.edu>*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> <54963A8D.2090707@illinois.edu>

Thank you for your reply, Elsa! Your questions made me pursue some previous research a little further, and I discovered an excerpt from Bell's "An Invitation to Smooth Infinitesimal Analysis" <http://publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf> that addresses your points. (The excerpt essentially says that R does indeed form a field and the law of the excluded middle is indeed problematic in infinitesimal analysis.) > …we deduce the important principle of infinitesimal cancellation, viz. IF εa = εb FOR ALL ε, THEN a = b. … We observe that the postulates of smooth infinitesimal analysis are incompatible with the law of excluded middle of classical logic. This > incompatibility can be demonstrated in two ways, one informal and the other > rigorous. First the informal argument. Consider the function f defined for > real > numbers x by f(x) = 1 if x = 0 and f(x) = 0 whenever x ≠ 0. If the law of > excluded > middle held, each real number would then be either equal or unequal to 0, > so > that the function f would be defined on the whole of R. But, considered as > a > function with domain R, f is clearly discontinuous. Since, as we know, in > smooth infinitesimal analysis every function on R is continuous, f cannot > have > domain R there. So the law of excluded middle fails in smooth infinitesimal > analysis. To put it succinctly, universal continuity implies the failure > of the law > of excluded middle. > Here now is the rigorous argument. We show that the failure of the law of > excluded middle can be derived from the principle of infinitesimal > cancellation. > To begin with, if x ≠ 0, then x^2 ≠ 0, so that, if x^2 = 0, then > necessarily not x ≠ 0. > This means that > for all infinitesimal ε, not ε ≠ 0. (*) > Now suppose that the law of excluded middle were to hold. Then we would > have, for any ε, either ε = 0 or ε ≠ 0. But (*) allows us to eliminate the > second > alternative, and we infer that, for all ε, ε = 0. This may be written > for all ε, ε.1 = ε.0, > from which we derive by infinitesimal cancellation the falsehood 1 = 0. So > again > the law of excluded middle must fail. … > What are the algebraic and order structures on R in SIA? As far as the > former is concerned, there is little difference from the classical > situation: in SIA > R is equipped with the usual addition and multiplication operations under > which it is a field. In particular, R satisfies the condition that each x > ≠ 0 has a > multiplicative inverse. Notice, however, that since in SIA no microquantity > (apart from 0 itself) is provably ≠ 0, microquantities are not required to > have > multiplicative inverses (a requirement which would lead to inconsistency). > From a strictly algebraic standpoint, R in SIA differs from its classical > counterpart only in being required to satisfy the principle of > infinitesimal > cancellation. > The situation is different, however, as regards the order structure of R in > SIA. Because of the failure of the law of excluded middle, the order > relation < > on R in SIA cannot satisfy the trichotomy law > x < y ∨ y < x ∨ x = y, > and accordingly < must be a partial, rather than a total ordering. I still really appreciate your questions though! On Sat, Dec 20, 2014 at 10:12 PM, Elsa L. Gunter <egunter at illinois.edu> wrote: > 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. >> >> Do you have reason to believe that the set of reals + infinitesimals > forms a field? I haven't done the exercise recently, but I don't believe > that the fact "{0} = {x::'a::field. x * x = 0}" in fields requires > classical reasoning, at least if stated roughly (F,0,1,+,*) a filed ==> 0 * > 0 = 0 \<and> (\<forall> x \<in> F. x * x = 0 --> x = 0). In fact, you > don't even need F to be a field, just an integral domain. In fact, the > very fact you wish to prove proves that the reals plus infinitesimals do > not form an integral domain and hence they don't form a field (assuming I > am right that showing fields are integral domains does not require > classical reasoning). I don't think classical reasoning is your problem > here. I think you want to start by constructing a type of reals plus > infinitesimals having the appropriate algebraic and order theoretic > properties. It has been a very long time since I've played with such > things, but I do not believe you need intuitionistic logic to reason about > infinitesimals at all. > ---Elsa >

**References**:**Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default***From:*Makarius

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

**Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default***From:*Elsa L. Gunter

- 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