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

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

```

• References:

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