*To*: Josh Tilles <merelyapseudonym at gmail.com>*Subject*: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sun, 21 Dec 2014 10:51:58 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Markus Wenzel <makarius at sketis.net>*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>

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. A moment with Google found another work by John L. Bell: http://publish.uwo.ca/~jbell/New%20lecture%20on%20infinitesimals.pdf 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. A suitable axiom system can be found in the book Logic and Structure by Lambek and Scott. But this would be a substantial project. Does Bell explain why smooth infinitesimal analysis is a better choice than Robinson’s NSA? Larry Paulson > On 21 Dec 2014, at 02:06, Josh Tilles <merelyapseudonym at gmail.com> wrote: > > On Mon, Dec 15, 2014 at 3:13 PM, Makarius <makarius at sketis.net> wrote: >> >> >> As far as I can tell, there is nobody on this planet who is familiar with >> all of Isabelle's internals. In fact the situation is better imagined like >> this: http://toplowridersites.com/you-are-here-milky-way-galaxy/ > > Ha! Interesting. > >> >> >> >> On Fri, 21 Nov 2014, Josh Tilles wrote: >> >> P.S. I'm about a hundred pages into *ML for the Working Programmer*, so I >>> apologize if all of my questions are just a result of my not yet having >>> read the chapter about constructing a tactical theorem prover [?] >>> >> >> There is certainly something to learn from it: how proof assistants were >> implemented in the early 1990-ies. See also the famous Handbook article by >> Larry Paulson "Designing a theorem prover": http://www.cl.cam.ac.uk/ >> techreports/UCAM-CL-TR-192.html > > Are you being tongue-in-cheek? I can't tell. Like, I wouldn't have guessed > that implementation techniques from twenty years ago are relevant now... > >> >> >> The newer "Handbook of Practical Logic and Automated Reasoning" by John >> Harrison also has a chapter on "Interactive theorem proving", see also >> http://www.cl.cam.ac.uk/~jrh13/atp --- it describes HOL-Light, so the >> prover architecture is very minimalistic. >> > Thank you for pointing that out! I might take a closer look at that later. > >> >> >> That won't help in the project to remove the classical principle from >> Isabelle/HOL, which I would consider futile. > > You all would certainly know better than I. That said, shouldn't Isabelle > be *able* to function with the classical axiom (HOL.True_or_False) made > into a locale-assumption? I don't mean that as a criticism of anybody's > work; just that if all that's needed is a bunch of tedious updates to proof > automation tools, I think I'd be up to the task as long as I would still be > welcome to ask questions on the mailing list when I run into difficulties. > >> Why change the logic anyway? > > 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. > >> Better use it (and its many ad-on tools) to model your own language and >> logic inside it. >> > I'm not sure what you mean. Could you elaborate? Or perhaps point me toward > some examples or explanations by other people?

**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