Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
I've responded inline.
And as always, I'm grateful for your replies.
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
> A moment with Google found another work by John L. Bell:
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