[auggierose]

Thanks for the link, looks like an interesting paper!

The thing is, formal rules can only model what you already understand. A formal rule can tell you exactly WHAT and HOW, but not WHY. But especially with basic proof rules like modus ponens, that is essential. So intuitive understanding is prior to formal rules. Of course, lots can be gained from the interplay of intuition and formality, I am the last one to deny that.

For me, that is an important issue, because I am a big proponent of doing logic on the computer, which necessarily is formal. Nevertheless, the goal here is to make logic on the computer as intuitiv as possible, something many people in the field don't seem to have a desire for. I also don't want the next generation to think exclusively in formal systems, in terms of, oh, if my formal system doesn't allow that, what I want to do must be wrong, or at least stupid. There is already enough of that going around with type theorists.