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




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