Re: reductio ad falsum versus reductio ad absurdum

> What thesis? |- doesn't nest.

ok, i guess that's the part i don't understand--why doesn't |- nest
when -> can??

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?
2. (further below) why are two very different inferences both called
RAA?
wouldn't it make more sense to distinguish them as i have? after
all,
deducing a self-contradiciton from an assumption is more
problematic than
deducing something which simply contradicts the facts


>
> > > Given |- P and P,A |- Q, conclude |- A -> Q
> >
> > ok that's true too, but if you don't have (|- P) but only have (P) (i.e
> > P is not a theorem of your system, but is a premise of your argument)
> > can't you conclude the weaker (A -> Q) ?
> >
> 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...


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)




>
> No. Given
> P |- Q
> P,A |- ~Q
> conclude
> P |- ~A
>
> Have you've notice how natural language is more fluid, ambiguous and
> imprecise than formal languages and translating from one to the other,
> like any translation, has gaps and mishaps?

again what you said metatheoretically is true--but could not be a rule
of ND.

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)



2. (what i'm inclined to call reductio ad absurdum)

---
A (assumption)
...
Q
...
~Q
~A

(which yields |- ~A)


how do i describe the rules applied here in sequents, as all the other
rules are described?

.