Re: [isabelle] Some corrections and amendments





On 09.07.2016 05:05, Gottfried Barrow wrote:
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 [ ... ]


The difference seems that between "What" and "How" rather.






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