Re: where do people check for the MML library?

On Fri, 30 Nov 2018, Freek Wiedijk wrote:

> Hi Brando,
>
>> I was hoping to learn the syntax by proving trial stuff, like in Coq, 
>> its helpful to even define natural numbers myself and define and prove 
>> properties about them, like n+m = m + n and other simple facts using 
>> even induction.
>
> _That_ will be very difficult in Mizar.  The Mizar library is
> based on set theory in ZFC style, so defining the natural
> numbers is a major undertaking.  They are the finite
> ordinals, I think, so you wold need to define ordinals
> and finiteness.
> Also Mizar is based on first order logic, so induction is a
> "scheme" which is somewhat involved in the first place.
>
>> is that possible in Mizar? Or is that a bad way to go about it?
>
> Possible certainly, but not a good way to start playing
> with the system.
>

Freek is absolutely right that usually we recommend the users to work on 
top of the existing library with all the basic staff already defined the 
ZFC way. But on the other hand, Mizar also allows building your own 
environment with extra axioms and I actually _do_ exactly this kind of 
exercises which Brando mentioned with my undergraduate students, so it is 
not _very difficult_. They just use a specially prepared local environment 
with all the needed notions in place, so they can prove by induction and 
axioms of the Peano arithmetic various elementary facts about arithmetic 
operations, Fibonacci numbers, factorial etc.

Brando: if you're interested, I can send you this student environment with 
a number of exercises to look at.

Adam

===========================================================================
Dept. of Programming and Formal Methods      Fax: +48(85)738-83-33
Institute of Informatics                     Tel: +48(85)738-83-06 (office)
University of Bialystok                      E-mail: [email protected]
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================