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



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?





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