Re: reductio ad falsum versus reductio ad absurdum

"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

> 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.

> 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

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


.

Relevant Pages
Loading