> > What concerns me is that the present ordinal-based development is very > close to textbooks (most textbooks I think, although I'm not sure), with > detailed references to Takeuti-Zaring in particular that match the textbook > almost exactly. >
This point must be emphasized. For instance by a detailed paragraph in the first theorem of the series and a note saying that a combined use of the formal proofs in set. mm and the explanations in Takeuti-Zaring would be very valuable pedagogical material. Proofs that are very close to a textbook are more suitable for beginners than the others. But attention should be drawn to this pecularity. A table of contents enumerating the proofs in the series and a short description of each one might help too. This kind of material -- close to the book -- might easily be set up for Euclid's books, featuring Euclid's original text, Aitken's handouts and Byrne's intuitive edition with diagrams. It would also constitute a very valuable material. We would have (in an international language) a full collection of texts connecting the original source, an intuitive presentation (Byrne), an accurate, modern and completely rigorous formulation (Aitken) and the final symbolic formalization. If we add a table with references to these texts put side by side, it would be the perfect tool for those who want to read Euclid and understand where the text is great and where it is inadequate. It would not be a repeat of Tarski's system. The treatise describing it is in German and thereby perfectly out of reach for the vast majority of inhabitants of this planet. And anyway Tarski's system is not the original system, it's a modern one. People are more comfortable with Euclid's system. It's the official definition of an euclidean plane, the definition of reference so to speak. And it might be used to show the equivalence of the reference definition with Tarski's system. It would also be a pity not to use Aitken's very interesting work. -- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f0fdfa41-277e-4d2c-b57b-170c5ee9b771n%40googlegroups.com.
