Re: [isabelle] Some corrections and amendments



On 7/7/2016 11:26 AM, Ken Kubota wrote:
Paulson argued that natural deduction is far superior to Hilbert-style systems
for automated proof. This is, of course, correct, since Hilbert-style
metatheorems become symbolically representable in natural deduction as regular
theorems (and not just metatheorems), but this only reflects the engineer's
perspective with the pragmatic aim of quickly obtaining proofs. For the
philosopher it is not proof automation but expressiveness that is the main
criterion, such that the method with the least amount of rules of inferences,
i.e., a Hilbert-style system, is preferred, and all other rules become derived
rules.

In particular, there is this sentence of yours: "...this only reflects the engineer's perspective with the pragmatic aim of quickly obtaining proofs. For the philosopher it is not proof automation but expressiveness that is the main criterion..."

I completely understand the issue of low status vs. high status, and the importance of trying to assert one's status, by bandying about labels, with the hopes that labels will stick.

I myself, at one time, aspired to be a philosopher, and mind you, no mere philosopher, but the mother-of-all-philosophers, as this would give me the ability to bandy about the mother-of-all-condensations, along with, certainly, the mother-of-all-condescensions.

Having aspired, I steeled myself, and struck the philosopher's pose, after which, my arm fell asleep. Surely, if I could have endured even 5 more minutes, the answer would have come, "42", and therefore, the prize. It was not to be.

Reevaluating my aspirations, I lowered them, and aspired to be an engineer, so that I could at least condescend to technicians.

Being a man of action, I went out and bought a little train set, and spent hours and hours painting the little cars, in intricate detail.

But one day, when I was engineering my little train set, saying, "choo, choo, choo" to the little train cars, the little kids next door heard me, because the window was open, and they started laughing at me.

Do you know how bad it hurts to have little kids laugh at you, when you're saying, "choo, choo, choo"?

So in one massive swoop, I destroyed my little train set, to show those little kids what a bad martial artist I was, MMA style.

They just kept laughing.

It was no great loss. I was actually only aspiring to be a bad martial artist, MMA style.

--
GZ
--








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.