I’m reading Poincare’s Science and Method as part of my philosophy of science mini-kick. Poincare is fun to read. I’m not sure what exactly I think of his views on logic, but I appreciate the Kantian line he’s pushing. I hope to write up something on his work, but I think I have a few other posts on the backburner. In the interim, to try to make up for my lack of posting last week, here is a quote from Poincare on Hilbert’s view of math and logic from his “Mathematics and Logic”:
“Thus, [according to Hilbert’s view] it will be readily understood that, in order to demonstrate a theorem, it is not necessary or even useful to know what it means. We might replace geometry by the reasoning piano imagined by Stanley Jevons; or, if we prefer, we might imagine a machine where we should put in axioms at one end and take out theorems at the other, like that legendary machine in Chicago where pigs go in alive and come out transformed into hams and sausages. It is no more necessary for the mathematician than it is for these machines to know what he is doing.”
Axioms in one end, theorems out the other. What would Poincare think of automated theorem proving?