Was thinking a bit about 's post over here. She quotes Klaus as saying that proofs in logic are "something that humans don't like to do", but I think it would only be fair to say it's something that many people don't like to do. But that just puts it in the category of a million other things that not everybody likes.

The events of the last couple days definitely have convinced me that simply doing math, doing logic, doing proofs --- can be really fun and exciting. I mean, I always sort of knew this, because I'm a dork and I've liked that sort of thing. But I want to claim something: that saying that proofs (even very highly formal syntactic ones) are "merely" exercises in symbol-shoveling is misguided. Not false exactly, but misguided; for it gives a limited picture of what's going on. Sure, there is some spectrum on which some proofs are very formal and abstract and syntactic and others are less so, but I don't think any are wholly without an intuitive component. It's just as apt to say that every use of language at all is "merely" symbol manipulation as well, which is to say not appropriate at all. By going through a lot experience with how some particular symbolic system works, we as human beings --- as things that learn --- get a feel for it, whether it's English or ZFC or the lambda calculus. We make predictions about what symbol-shoveling strategies will get us the result we want, and we test them, and we develop gut instincts, and so on.

The thing about very abstract proofs that can be very good (and it's this thought that has been reinforced so strongly lately for me) is that you can strip away all the intuitions that aren't essential to the problem at hand. By making it (suitably) more abstract and more formal, the prover clears the air of the informal ideas that pertain to everything else about the problem that isn't making it problematic. The goal isn't so much to eliminate all intuitions so that a machine (or person acting like a machine) can do the proof, but to get the problem into such a state where the right intuitions can clearly guide the proof without interference.
Tags:
• #### (no subject)

A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf

• #### (no subject)

Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…

• #### (no subject)

Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…

• #### Error

Anonymous comments are disabled in this journal

default userpic