> > > For me the usual treatise of logic is mostly artificial and this is > probably the only universally available tool to make it more concrete. >
I don't fundamentally disagree with that. Simply I think that if you want to teach logic with software you have to use natural deduction with a system where the context stack is very apparent at each step and where the problem of provisos is simplified as much as possible. I feel that there are systems where when you delete a quantifier, the variable is replaced by a constant. It seems to me to be the clearest system for a beginner. And then the teacher must analyze on the blackboard a textual demonstration to clearly show the relationship between textual demonstration and formal demonstration and that juggling between the two forms is acquired. Finally, I find that a system where the human-machine interface is very visual is better. In short, that's why I think Metamath is not the best educational tool. -- 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/044baf33-ab31-4cf0-bc5c-9c28e0f33932%40googlegroups.com.
