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



Thank you for your reply, Elsa!

Your questions made me pursue some previous research a little further, and
I discovered an excerpt from Bell's "An Invitation to Smooth Infinitesimal
Analysis" <http://publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf> that
addresses your points.
(The excerpt essentially says that R does indeed form a field and the law
of the excluded middle is indeed problematic in infinitesimal analysis.)



> …we deduce the important principle of infinitesimal cancellation, viz.

IF εa = εb FOR ALL ε, THEN a = b.

…

We observe that the postulates of smooth infinitesimal analysis are

incompatible with the law of excluded middle of classical logic. This
> incompatibility can be demonstrated in two ways, one informal and the other
> rigorous. First the informal argument. Consider the function f defined for
> real
> numbers x by f(x) = 1 if x = 0 and f(x) = 0 whenever x ≠ 0. If the law of
> excluded
> middle held, each real number would then be either equal or unequal to 0,
> so
> that the function f would be defined on the whole of R. But, considered as
> a
> function with domain R, f is clearly discontinuous. Since, as we know, in
> smooth infinitesimal analysis every function on R is continuous, f cannot
> have
> domain R there. So the law of excluded middle fails in smooth infinitesimal
> analysis. To put it succinctly, universal continuity implies the failure
> of the law
> of excluded middle.
>  Here now is the rigorous argument. We show that the failure of the law of
> excluded middle can be derived from the principle of infinitesimal
> cancellation.
> To begin with, if x ≠ 0, then x^2 ≠ 0, so that, if x^2 = 0, then
> necessarily not x ≠ 0.
> This means that
>  for all infinitesimal ε, not ε ≠ 0. (*)
> Now suppose that the law of excluded middle were to hold. Then we would
> have, for any ε, either ε = 0 or ε ≠ 0. But (*) allows us to eliminate the
> second
> alternative, and we infer that, for all ε, ε = 0. This may be written
> for all ε, ε.1 = ε.0,
> from which we derive by infinitesimal cancellation the falsehood 1 = 0. So
> again
> the law of excluded middle must fail.

…
> What are the algebraic and order structures on R in SIA? As far as the
> former is concerned, there is little difference from the classical
> situation: in SIA
> R is equipped with the usual addition and multiplication operations under
> which it is a field. In particular, R satisfies the condition that each x
> ≠ 0 has a
> multiplicative inverse. Notice, however, that since in SIA no microquantity
> (apart from 0 itself) is provably ≠ 0, microquantities are not required to
> have
> multiplicative inverses (a requirement which would lead to inconsistency).
> From a strictly algebraic standpoint, R in SIA differs from its classical
> counterpart only in being required to satisfy the principle of
> infinitesimal
> cancellation.
> The situation is different, however, as regards the order structure of R in
> SIA. Because of the failure of the law of excluded middle, the order
> relation <
> on R in SIA cannot satisfy the trichotomy law
> x < y ∨ y < x ∨ x = y,
> and accordingly < must be a partial, rather than a total ordering.


I still really appreciate your questions though!

On Sat, Dec 20, 2014 at 10:12 PM, Elsa L. Gunter <egunter at illinois.edu>
wrote:

> Dear John,
>
> On 12/20/14 8:06 PM, Josh Tilles wrote:
>
>> 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.
>>
>>  Do you have reason to believe that the set of reals + infinitesimals
> forms a field?  I haven't done the exercise recently, but I don't believe
> that the fact "{0} = {x::'a::field. x * x = 0}" in fields requires
> classical reasoning, at least if stated roughly (F,0,1,+,*) a filed ==> 0 *
> 0 = 0 \<and>  (\<forall> x \<in> F. x * x = 0 --> x = 0).  In fact, you
> don't even need F to be a field, just an integral domain.  In fact, the
> very fact you wish to prove proves that the reals plus infinitesimals do
> not form an integral domain and hence they don't form a field (assuming I
> am right that showing fields are integral domains does not require
> classical reasoning).  I don't think classical reasoning is your problem
> here.  I think you want to start by constructing a type of reals plus
> infinitesimals having the appropriate algebraic and order theoretic
> properties.  It has been a very long time since I've played with such
> things, but I do not believe you need intuitionistic logic to reason about
> infinitesimals at all.
> ---Elsa
>



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