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: adamn@mizar.org Ciolkowskiego 1M, 15-245 Bialystok, Poland http://math.uwb.edu.pl/~adamn/ ===========================================================================