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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and