>The axioms for geometry and real numbers are not >built into the DC Proof system. The numbers of >axioms alone would overwhelm the beginner. For >the axioms of geometry, see the work of Tarski >or Hilbert. You can find a version of the axioms >for the real numbers in the DC Proof/Samples directory. > >Beware, though. In my experience, even >elementary results in the Euclidean plane can >quickly explode into proofs of several hundred, >even thousands of lines. So, I really can't >recommend geometry for the beginner just >learning how to write mathematical proofs. >Better to stick to logic, set theory, and >elementary number theory, the axioms of which >ARE built into DC Proof. (See "To the Educator" at my homepage.)
All true but I come to exactly the opposite conclusion about beginners just learning how to write mathematical proofs. I continue to believe (as with far better mathematicians than either of us over the last couple millennia) that Euclidean plane geometry remains a wonderful place to introduce mathematical proof to beginners. Moreover, I am absolutely convinced that much of the reason that US students pursuing degrees in mathematics have so much difficulty with mathematical proof is the loss of a good (in spite of its logical problems) introduction to proof in the context of the traditional high school (usually sophomore) course in Euclidean plane geometry. So-called "modern" introductions to geometry that have replaced it are so awful as to be useless if not outright counterproductive. I have been teaching our upper division university course entitled "Modern Geometry" for the past 40 years and the performance has gotten steadily worse over the decades. With very few exceptions, students who have had their precollege education abroad - Mideast, Far East, Russia, Ethiopia, etc. - are the best students of the class and that did not used to be the situation, say, back in the 70s when we had lots of students from Iran. A nice example was my first student assistant after I was left quadriplegic and in need of competent classroom assistance. She was from Lebanon, a beginning high school mathematics teacher there who had lost all of her school records when she left Lebanon at the height of the conflict there years before. With her children now in middle school, she decided to return to the university and do whatever she needed to get US credit for a bachelor's degree in mathematics. At the time, I had not yet figured out how I could write so she needed to score my neighbors as well as write stuff on the board that I had not been able to anticipate and use Geometer's Sketchpad or Cinderella (wonderful for examples in the Poincaré disk model for hyperbolic geometry).
I have always felt the need to start the course with a quick review of stuff learned in the traditional high school course but over the years it has become less and less "review" than initial introduction and, although they have earned a C or better in a course entitled "Math Notation and Proof", they have little idea of what mathematical proof is really all about. On the first quiz, she came back from scoring absolutely amazed, better said, appalled at some students inability to even regurgitate easy stuff that was both in the printed material I had distributed and discussed in class. Her assessment, "We learned that stuff in 7th grade!".
Beginning as you propose strikes me as being perceived by most students as an exercise in abstract nonsense, not in providing some level of understanding of the solid foundation for mathematics that proof provides. Beyond that, except for mathematical logic itself, no professional mathematician appeals to axiomatic set theory or formalistic logic in their thinking nor in their publications. More than a few have no idea what you're even talking about once you get beyond, say, discussions about the Axiom of Choice.