Re: reductio ad falsum versus reductio ad absurdum


Torkel Franzen wrote:
> "futurist" <adamgolding@xxxxxxxxxxxxxxx> writes:
>
> > Conditional Proof
> > ???? |- A->Q
> >
> > i don't see a way to fill in the ???? without nesting |-.
>
> I don't know of any very convenient way of faithfully representing
> rules and derivations in natural deduction in news postings.
>
> We can use instead the closely related sequent calculus with a
> single formula in the consequent. The rule of conditional proof is then
>
> G,A => B
> --------
> G => A->B

i'm not well versed in the sequent calculus--let me see if i
understand:

the => means |-, here?

and it reads: "if B is derivable from G and A, then A->B is derivable
from G??

if so, then this rule does not capture the inference in ND at all,
since the conclusion is a statment in the metalanguage. the 'rule' i
want to formalize concludes a simple wff in the object language.

>
> > what are the sequents describing rules of ND which permit the following
> > two (distinct) inference patterns?
> >
> > 1. (what i'm inclined to call reductio ad falsum)
> >
> > P
> > ---
> > ...
> > Q
> > A (assumption)
> > ...
> > ~Q
> > ~A
> >
> >
> > (which yields P |- ~A)
>
> In the above notation, we write this (disregarding any other formulas
> involved) as
>
> P => Q A => ~Q
> _______
> P => ~A
>
> In Gentzen's system of natural deduction, this is a derived rule.

again, this seems perfectly true, but does not seem to be a formulation
of a rule in ND, although it may map well onto one...

in Allen & Hand's logic primer (i'm working from several books here),
they list most rules with sequents, as i did with modus ponens above:

P->Q,P |- Q is the rule,

and

P->Q
P
---
.: Q is the corresponding inference.

they handle CP and RAA etc. by having a separate rule called
'assumption', but this bothers me about the system, since then
additional rules have to be heaped on about when the statements written
below the line are actually valid conclusions (i.e. when all
assumptions are discharged)... so i figured nesting |- captures the
structure right--when you have:

P
----

and when you then 'assume A'--you're essentially begining a subproof, a
proof within the proof, a proof that (A & P => ~Q) or whatever result
you need. so, by this line of thinking, saying that CP is

(P |- Q) |- (P -> Q)

makes a lot of sense to me--although i gather from the responses that
there is something wrong with this--although i don't quite gather
what--is there something formally/techincally wrong? is it false? is
it just non-standard? i'm not sure why this wouldn't be a sensible
metalinguistic convention for talking about ND proofs, and the way the
proofs nest.


>
> > 2. (what i'm inclined to call reductio ad absurdum)
> >
> > ---
> > A (assumption)
> > ...
> > Q
> > ...
> > ~Q
> > ~A
> >
> > (which yields |- ~A)
> >
>
> Similarly,
>
> A => Q A => ~Q
> ------
> => ~A
>
>
> Note, however, that this is not reductio ad absurdum in the
> sense of the link you gave earlier. That link is about "classical
> reductio" or "the rule of indirect proof":
>
> ~A => Q ~A => ~Q
> -------
> => A

Allen & Hand call the above rule "Impossible Antecedent", and they lump
all the rest under RAA...

>
> What you call reductio ad absurdum (and which is often so called) is
> the "constructive reductio", which is also valid in constructive
> logic.

ok, so with RAA often being used as an umbrella term, 'constructive
reductio' makes it clear that one means the one with no premises. is
there another specifying term in somewhat common parlance to specify
the other kind, i.e. not constructive reduction, not impossible
antecedent, but the one i called 'reductio ad falsum' ??

.

Relevant Pages

  • Re: reductio ad falsum versus reductio ad absurdum
    ... The rule of conditional proof is then ... (what i'm inclined to call reductio ad absurdum) ... Note, however, that this is not reductio ad absurdum in the ... the "constructive reductio", which is also valid in constructive ...
    (sci.logic)
  • Re: reductio ad falsum versus reductio ad absurdum
    ... > Conditional Proof: ... You can use any notation you like as long as you define a precise ... There can be any number of premises in both constructive reductio ...
    (sci.logic)
  • reductio ad falsum versus reductio ad absurdum
    ... stonger in a special case--below i've attempted to tease this ... apart--please tell me if this makes sense (i chose the terms based on ... CONDITIONAL PROOF: ... REDUCTIO AD ABSURDUM: ...
    (sci.logic)