Re: Natural deduction?

On 27 Nov 2005 09:29:16 -0800, "George Dance" <georgedance04@xxxxxxxx>
wrote:

>
> So here is a major difference between the systems: Gentzen gives a
> crisp, clear list of primitive rules, ordered into int-elim pairs [...]
>
Right. And there's a deep idea behind that:

"The claim that the essential deductive operations have been isolated
[in Gentzen's calculi] is not to be understood as the claim that these
operations mirror all informal deductive practices, which would be an
unreasonable demand in view of the fact that informal practices may
sometimes contain logically insignificant irregularities. What is
claimed is that the essential logical content of intuitive logical
operations that can be formulated in the language considered can be
understood as composed of the atomic inferences isolated by Gentzen.
It is in this sense that we may understand the terminology _natural_
deduction."

(D. Prawitz)

>
> OTC, Copi offers a mixed bag of [more than] twice as many primitive rules,
> with no discernible order between them, no reason (except that they're
> known to be valid) for them being in there, and no clear distinction
> between primitive and non-primitive rules - with the consequence that
> his set of rules doesn't even stay the same from time to time. (So,
> again just to have a name, I'd call that a 'mixed-bag' type of system.)
>
"mixed-bag", very good. (Some logician called it a "melange".)

>
> The question is which type of system "comes as close as possible to
> actual reasoning" and thus best means Gentzen's criterion. [...]
>

"Gentzen's systems are also natural in the more
superficial sense of corresponding rather well to informal practices;
in other words, the structures of informal proofs are often preserved
rather well when formalized within the systems of natural deduction."

(D. Prawitz)

>
> ...it is quite clear that, by 'reasoning,' Gentzen did mean 'mathe-
> matical reasoning.'
>
Right:

"The formalization of logical deduction, especially as it has been
developed by Frege, Russell, and Hilbert, is rather far removed from the
forms of deduction used in practice in mathematical proofs. ... In
contrast I intended first to set up a formal system which comes as close
as possible to actual reasoning. The result was a calculus of natural
deduction (NJ for intuitionist, NK for classical predicate logic)."

(Gentzen, Investigations into logical deduction)

>
> However, if the 'reasoning' one is interested in is the normal,
> day-to-day, mostly informal reasoning that all of us (even
> mathematicians) do in the course of our daily lives, then a
> 'mixed bag' type of system is the better approximation.
>
See Dan Prawitz' comment above. I agree with him.


F.

--
"I do tend to feel Hughes & Cresswell is a more authoritative
source than you." (D. Ullrich)
.

Relevant Pages

  • Re: Natural deduction?
    ... > "The formalization of logical deduction, ... > developed by Frege, Russell, and Hilbert, is rather far removed from the ... > as possible to actual reasoning. ... mathematicians) do in the course of our daily lives, ...
    (sci.logic)
  • Re: No Mid Term Reasoning
    ... a so called natural style deduction ... calculus, because it is lacking ... As we know the two clauses that is no mid term could not be reasoned ... according to the classic logic reasoning. ...
    (sci.logic)
  • Re: Luskin: Judge Wrong To Rule Against IDs Theology
    ... "validity" identifies a line of reasoning such that if the initial ... validity means the same thing in induction and deduction. ...
    (talk.origins)
  • Re: Justifying transfinite induction in ZF
    ... vastly different from saying that such people take deduction as the ... only method of mathematical REASONING. ... an axiom has to be proved (from the axioms and definitions). ... Deduction as the queen of logical reasoning is part of the ...
    (sci.logic)
  • Re: Justifying transfinite induction in ZF
    ... Deduction as the queen of logical reasoning is part of the ... preminence to calculation vs. reasoning, ... philosophy of mathematics - you know, find out what many other people ...
    (sci.logic)
Quantcast