Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default



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.



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