[isabelle-dev] construction of the real numbers

[Walther Neuper]

Brian Huffman wrote:
> On Mon, May 10, 2010 at 12:41 AM, Walther Neuper <neuper at ist.tugraz.at> wrote:
>> A comment you ask for: Your assumption, that "users should not need to know
>> or care which construction of reals we use", does not apply in education.
>>
>> There are several attempts to design educational software for ("pure" and
>> "applied") mathematics, which is _transparent_ in the sense, that the
>> learner can access any knowledge underlying a particular calculation.
> 
> Hi Walther,
> 
> I completely agree with your comments. I guess I really meant to
> distinguish the "users" of Isabelle theories from "readers" or
> "students" of those theories. It is for the benefit of this second
> group that the theory of Dedekind real numbers should be kept
> available. 

Right !
A variety of models for reals is a definite advantage for learning.
Now it is the duty for developers of educational math software to 
provide smooth access to these models ;-)

> I have personally learned a lot of new mathematics by
> studying formalizations in Isabelle, and I hope that later students
> will benefit by having two alternative constructions of the real
> numbers to study.
> 
> - Brian

Walther