*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default*From*: Josh Tilles <merelyapseudonym at gmail.com>*Date*: Sun, 21 Dec 2014 17:51:33 -0500*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Markus Wenzel <makarius at sketis.net>*In-reply-to*: <517D4E09-7AA6-4725-A1C4-E03627EC8959@cam.ac.uk>*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> <517D4E09-7AA6-4725-A1C4-E03627EC8959@cam.ac.uk>

I've responded inline. And as always, I'm grateful for your replies. --Josh On Sun, Dec 21, 2014 at 5:51 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > You should consider adopting Isabelle's built-in development of > non-standard analysis, which is constructed definitionally using > ultrafilters. (See …/src/HOL/NSA.) The non-standard real numbers do indeed > form a field; the whole point of non-standard analysis is that the > first-order theories of the standard and non-standard entities are > identical. Here, the only nil square infinitesimal is zero. > Thank you for pointing that out. (There's so much of Isabelle that's worthy of study!) > > A moment with Google found another work by John L. Bell: > > http://publish.uwo.ca/~jbell/New%20lecture%20on%20infinitesimals.pdf That lecture appears to be *very* similar to the introduction to the book of his that I'm using. > > > and this does indeed require intuitionistic logic. If you really want to > create a constructive theory of higher-order logic, you will need to start > from scratch. *sigh* I knew that that it might come to that. > A suitable axiom system can be found in the book Logic and Structure by > Lambek and Scott. Thanks for the tip! > But this would be a substantial project. > Understood. But for a moment, let's say I took it on: a constructive theory of higher-order logic *could* be built using Isabelle/Pure, right? Or are there certain kinds of object-logics that won't fit into Pure's paradigm? > > Does Bell explain why smooth infinitesimal analysis is a better choice > than Robinson’s NSA? > I'm not sure that Bell claims anywhere that SIA is *better* than Robinson's NSA, but he does compare the two: > …[N]onstandard analysis shares with smooth infinitesimal analysis a > concept of infinitesimal in which the idea of continuity is represented by > the idea of ‘preservation of infinitesimal closeness’. Nevertheless, there > are many differences between the two approaches. We conclude by stating > some of them. > > 1. In models of smooth infinitesimal analysis, only smooth maps > between objects are present. In models of nonstandard analysis, all > set-theoretically definable maps (including discontinuous ones) appear. > 2. The logic of smooth infinitesimal analysis is intuitionistic, > making possible the nondegeneracy of the microneighbourhoods and > *M_**i *, *i *= 1, 2, 3. The logic of nonstandard analysis is > classical, causing all these microneighbourhoods to collapse to zero. > 3. In smooth infinitesimal analysis, the Principle of Microaffineness > entails that all curves are ‘locally straight’. Nothing resembling this is > possible in nonstandard analysis. > 4. The property of nilpotency of the microquantities of smooth > infinitesimal analysis enables the differential calculus to be reduced to > simple algebra. In nonstandard analysis the use of infinitesimals is a > disguised form of the classical limit method. > 5. In any model of nonstandard analysis *R has exactly the same > set-theoretically expressible properties as R does: in the sense of > that model, therefore, *R is in particular an Archimedean ordered > field. This means that the ‘infinitesimals’ and ‘infinite numbers’ of > nonstandard analysis are so not in the sense of the model in which they > ‘live’, but only relative to the ‘standard’ model with which the > construction began. That is, speaking figuratively, a ‘denizen’ of a model > of nonstandard analysis would be unable to detect the presence of > infinitesimals or infinite elements in *R. This contrasts with smooth > infinitesimal analysis in two ways. First, in models of smooth > infinitesimal analysis containing invertible infinitesimals, the smooth > line is non-Archimedean in the sense of that model. In other words, > the presence of infinite elements and (invertible) infinitesimals would be > perfectly detectable by a ‘denizen’ of that model. And secondly, the > characteristic property of nilpotency possessed by the microquantities of > any model of smooth infinitesimal analysis (even those in which invertible > infinitesimals are not present) is an intrinsic property, perfectly > identifiable within that model. > > The differences between nonstandard analysis and smooth infinitesimal > analysis may be said to arise because the former is essentially a theory of > infinitesimal numbers designed to provide a succinct formulation of the > limit concept, while the latter is, by contrast, a theory of infinitesimal > geometric objects, designed to provide an intrinsic formulation of the > concept of differentiability.

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

**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:*Lawrence Paulson

- 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