Re: reductio ad falsum versus reductio ad absurdum

On Sun, 28 Aug 2005, futurist wrote:
To whom are you repling? Removal of immediate references can lead to your
reply not being noticed by the person to whom you are repling. (I read by
new arrivals, not by threaded format, as the former is easier for seeing
what's up.)

> ok, i guess that's the part i don't understand--why doesn't |- nest
> when -> can??
>
Becuase -> combines two formal statements into another.
P |- Q is a statement about a sequence of formal statements.
(P |- Q) |- R, is a statment about a sequence of formal statements
because P |- Q isn't a formal statement.

> basically this arose because i was making myself a list of various
> rules and theorems in ND systems, and realized that CP, to take the
> simplest example, wasn't presented in the same way as the others:
>
> Modus ponens
> P, P->Q |- Q
>
> Conditional Proof
> ???? |- A->Q
>
> i don't see a way to fill in the ???? without nesting |-. to be
> clearer, i have no thesis, i have two questions:
>
> 1. why is what i put for the ???? wrong, and what SHOULD go there?

A set of formal statements only.

> 2. (further below) why are two very different inferences both called
> RAA?

Then ask it further below.

> > What you described can formally be expressed as
> > Given P,A |- Q, conclude P |- A -> Q
> > which is called the Deduction Theorem, tho actually it's a metatheorem.
>
> in which case it can't be a description of a rule of ND...
>
ND has somewhat different syntax than PC, propositional calculus.

> when i write:
>
> P
> ----
> A (assumption)
> ...
> Q
> A->Q (conditional proof)
>
> i'm not using any metatheorems--i'm just using some rule (CP) of the
> object language--but i don't know how to precisely formalize that rule
> as a sequent... (see above)
>
You are mixing ND with PC. Here's ND

assume P
assume A
...
Q
A -> Q
P -> (A -> Q)

> 1. (what i'm inclined to call reductio ad falsum)
>
> P
> ---
> ...
> Q
> A (assumption)
> ...
> ~Q
> ~A
>

assume P
...
Q
assume A
...
~Q
Q -> F (ND definition ~Q)
Q
F
A -> F
~A
P -> ~A

> (which yields P |- ~A)
>
It does not. You assumed P |- Q.

> 2. (what i'm inclined to call reductio ad absurdum)
>
> ---
> A (assumption)
> ...
> Q
> ...
> ~Q
> ~A
>
> (which yields |- ~A)
>
It does not. You assumed A |- Q.

> how do i describe the rules applied here in sequents, as all the other
> rules are described?
>
You are hopelessly confusing ND with PC.
Be content with what I think you've stated
P -> Q, Q -> (A -> ~Q) |- ~A
P -> Q, Q -> ~Q |- ~P

As for a distinction
P -> ~P |- ~P
P -> Q, P -> ~Q |- ~P

.