reductio ad falsum versus reductio ad absurdum
futurist
quite understand them--especially as RAA seems able to prove something
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
http://www.iep.utm.edu/r/reductio.htm):
CONDITIONAL PROOF:
P
P, A |- Q
|-
A -> Q
REDUCTIO AD FALSUM:
P
P |- Q
P, A |- ~Q
|-
~A
REDUCTIO AD ABSURDUM:
A |- F (where F is any self-contradiction)
|-
|- ~A
William Elliot
> although i know how to do RAA and CP--it's occured to me that i don't
> quite understand them--especially as RAA seems able to prove something
> 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
> http://www.iep.utm.edu/r/reductio.htm):
>
RAA? CP?
What's your thesis? CP implies other rules of inference?
> CONDITIONAL PROOF:
> P
> P, A |- Q
> |-
> A -> Q
>
You are not making good sense.
Given |- P and P,A |- Q, conclude |- A -> Q
> REDUCTIO AD FALSUM:
> P
> P |- Q
> P, A |- ~Q
> |-
> ~A
>
Given |- P
P |- Q
P,A |- ~Q
conclude
|- ~A
> REDUCTIO AD ABSURDUM:
> A |- F (where F is any self-contradiction)
> |-
> |- ~A
>
Given A |- F, conclude |- ~A
adamg...@gmail.com
William Elliot wrote:
> On Sat, 27 Aug 2005, futurist wrote:
>
> > although i know how to do RAA and CP--it's occured to me that i don't
> > quite understand them--especially as RAA seems able to prove something
> > 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
> > http://www.iep.utm.edu/r/reductio.htm):
> >
> RAA? CP?
sorry, i thought those were standard abbreviations for the headers in
bold below. (they're in two different logic texts of mine)
>
> What's your thesis? CP implies other rules of inference?
well, i agree with that thesis as well, but actually i just wanted to
see if i was anaylsing these three rules correctly--in my texts they
aren't spelled out in metatheoretic symbolism--they're just explained
in english in terms of making and discharging assumptions. what i'm
trying to do is to show the nesting involved in these 'rules' but
nesting the |- symbol.
also, i haven't seen any text distinguish the two reductios, yet i'm
pretty sure there's a difference--do others here agree? is this
difference treated explicitly in some texts?
>
> > CONDITIONAL PROOF:
> > P
> > P, A |- Q
> > |-
> > A -> Q
> >
> You are not making good sense.
> 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) ?
>
> > REDUCTIO AD FALSUM:
> > P
> > P |- Q
> > P, A |- ~Q
> > |-
> > ~A
> >
> Given |- P
> P |- Q
> P,A |- ~Q
> conclude
> |- ~A
again, if we replace |-P with P, can't we conclude merely ~A, as i
wrote?
>
> > REDUCTIO AD ABSURDUM:
> > A |- F (where F is any self-contradiction)
> > |-
> > |- ~A
> >
> Given A |- F, conclude |- ~A
yes, that's exactly what i said in thise case
William Elliot
> William Elliot wrote:
> > On Sat, 27 Aug 2005, futurist wrote:
>
> > What's your thesis? CP implies other rules of inference?
>
> well, i agree with that thesis as well, but actually i just wanted to
> see if i was anaylsing these three rules correctly--in my texts they
> aren't spelled out in metatheoretic symbolism--they're just explained
> in english in terms of making and discharging assumptions. what i'm
> trying to do is to show the nesting involved in these 'rules' but
> nesting the |- symbol.
>
> > 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.
> > > REDUCTIO AD FALSUM:
> > > P
> > > P |- Q
> > > P, A |- ~Q
> > > |-
> > > ~A
> > >
> > Given |- P
> > P |- Q
> > P,A |- ~Q
> > conclude
> > |- ~A
>
> again, if we replace |-P with P, can't we conclude merely ~A, as i
> wrote?
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?
futurist
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?
Torkel Franzen
> 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.
Chris Menzel
>> What thesis? |- doesn't nest.
>
> ok, i guess that's the part i don't understand--why doesn't |- nest
> when -> can??
Because, unlike ->, |- is not a boolean logical connective. Rather,
"S |- Q" is an abbreviation in the *metalanguage* that we are using to
talk *about* the logical system in question for "There is a proof in the
system of Q from S", where Q is a sentence of the language of the system
and S is a set of sentences of the language. In the case where S is
only a singleton {P}, it is conventional to write "P |- Q" instead of
"{P} |- Q".
That said, there is in fact a *sense* in which |- can nest in certain
systems that are powerful enough to represent their own proof relations.
But that's another discussion.
William Elliot
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
adamg...@gmail.com
Torkel Franzen wrote:
> "futurist" <adamg...@adamgolding.com> 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' ??
adamg...@gmail.com
Chris Menzel wrote:
> On 28 Aug 2005 20:30:44 -0700, futurist <adamg...@adamgolding.com> said:
> >> What thesis? |- doesn't nest.
> >
> > ok, i guess that's the part i don't understand--why doesn't |- nest
> > when -> can??
>
> Because, unlike ->, |- is not a boolean logical connective. Rather,
> "S |- Q" is an abbreviation in the *metalanguage* that we are using to
> talk *about* the logical system in question for "There is a proof in the
> system of Q from S", where Q is a sentence of the language of the system
> and S is a set of sentences of the language. In the case where S is
> only a singleton {P}, it is conventional to write "P |- Q" instead of
> "{P} |- Q".
ah, so nothing with a turnstile in it is a wff for sentential logic,
thus any nesting of |- would yield false statements (it's false that
you can prove something from a non-wff)... so then how do you write out
the rule for CP or RAA etc. in a formal way rather than just showing an
example of it?
adamg...@gmail.com
William Elliot wrote:
> 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.)
sorry about that, didn't mean to delete any name headers...
> 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.
replace the last is with 'isn't' and i think i understand..
> >
> > 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.
ok, but which set of formal statements to express the rule of CP?
>
> > 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.
i just want a way to express, precisely and formally, the ND rules of
CP, and RAA, and possibly a way to distinguish various forms of RAA.
although at this point i can't see how to do that since |- doesn't
nest...
>
> > 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)
i don't know about that--i was taught ND in two separate classes where
we had lists of premises, AND we could introduce assumptions for CP,
which is what i've done here. at any rate, what you gave me was an
example of a proof using a rule, not a formalization of that rule...
>
> > 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.
???? P was my premise. A was my assumption A was discharged when i
concluded ~A. thus using only the truth of P i concluded ~A--in other
words i proved that P |- ~A.
P is not atomic here--i'm assuming it has an inner structure that lets
me conclude Q. (i'm not writing out a specific proof, i'm showing a
schematic application of the rule (which is still not really a
*formalization* of the rule))
>
> > 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.
again, A is not atomic, this is the sort of outline they give in many
books of these sorts of proof.. i.e. imagine that A was "Q&~Q" for the
simplest case. then this would definitely yield a proof of |- ~A .
at any rate these are just examples of these rules and not precise
formulations of them.
>
> > how do i describe the rules applied here in sequents, as all the other
> > rules are described?
> >
> You are hopelessly confusing ND with PC.
my understanding is that PC uses several axioms and one rule (MP),
wheras ND uses many rules and no axioms. i'm not thinking of PC at
all, although i understand that they both begin with a list of
premises.
> 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
this one doesn't seem sufficiently general-- couldn't you have P->Q&~Q
withought P->~P? or at the very least, you could get the former in
fewer steps... so we can say:
P -> Q&~Q |- ~P
> P -> Q, P -> ~Q |- ~P
yes i know this one as 'impossible antecent'
so, the formulations immediately above are examples of rules that could
work *in conjunction* with CP to yield the proofs in my example--this
places the burden of describing the rule on CP--how do we precisely
describe the rule of Conditional Proof?
Torkel Franzen
> the => means |-, here?
We don't need to take => to refer to provability in any formal calculus.
Just read G=>A as "A follows from G". The rule
G,A => B
--------
G => A->B
then allows us to conclude, given that B follows from G together with
A, that A->B follows from G.
> 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?
To make good sense of the above, you need to specify the language
you use and how |- is to be understood.
> >
> > ~A => Q ~A => ~Q
> > -------
> > => A
>
> Allen & Hand call the above rule "Impossible Antecedent", and they lump
> all the rest under RAA...
"Impossible Antecedent" is not standard terminology. But the
important thing is that indirect proof is not constructively
valid, but constructive reductio is.
> ok, so with RAA often being used as an umbrella term, 'constructive
> reductio' makes it clear that one means the one with no premises.
Here I don't see what you have in mind.
> 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' ??
Not that I know of.
Chris Menzel
<adamg...@gmail.com> said:
>
> Chris Menzel wrote:
>> On 28 Aug 2005 20:30:44 -0700, futurist <adamg...@adamgolding.com> said:
>> >> What thesis? |- doesn't nest.
>> >
>> > ok, i guess that's the part i don't understand--why doesn't |- nest
>> > when -> can??
>>
>> Because, unlike ->, |- is not a boolean logical connective. Rather,
>> "S |- Q" is an abbreviation in the *metalanguage* that we are using to
>> talk *about* the logical system in question for "There is a proof in the
>> system of Q from S", where Q is a sentence of the language of the system
>> and S is a set of sentences of the language. In the case where S is
>> only a singleton {P}, it is conventional to write "P |- Q" instead of
>> "{P} |- Q".
>
> ah, so nothing with a turnstile in it is a wff for sentential logic,
Correct.
> thus any nesting of |- would yield false statements
Well, no, such nesting is grammatically ill-formed, hence simply
meaningless.
> so then how do you write out the rule for CP or RAA etc. in a formal
> way rather than just showing an example of it?
I don't understand the question. Do you think one needs to nest |-
to state these rules?
Daryl McCullough
I think what he means is this: In sequent-style proof systems,
CP has this form:
A |- B
----------
|- A -> B
He's thinking of this as a kind of "higher-level" sequent
(A |- B) ==> (|- A -> B)
where ==> acts sort of like |-, except that the hypotheses
and conclusion are sequents, instead of statements.
--
Daryl McCullough
Ithaca, NY
Chris Menzel
I see. Well, he should stop thinking that. :-)
-chris
William Elliot
> William Elliot wrote:
> > On Sun, 28 Aug 2005, futurist wrote:
>
> > Becuase -> combines two formal statements into another.
> > P |- Q is a statement about a sequence of formal statements.
> > because P |- Q isn't a formal statement.
>
> replace the last is with 'isn't' and i think i understand..
>
formula of the object language. It is a statement of the metalanguage
and can't be expressed with -> & v <-> (Ex) (Ax) of the object language.
> > > 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.
>
> ok, but which set of formal statements to express the rule of CP?
>
Given
|- P
|- P -> Q
infer
|- Q
You must use meta language "infer" and not object language "->" because
|-P is not a statement of the object language.
> i just want a way to express, precisely and formally, the ND rules of
> CP, and RAA, and possibly a way to distinguish various forms of RAA.
> although at this point i can't see how to do that since |- doesn't
> nest...
>
Then do so as I have show with MP without confusing the object language
with the metalanguage.
> > > 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)
>
> i don't know about that--i was taught ND in two separate classes where
> we had lists of premises, AND we could introduce assumptions for CP,
> which is what i've done here. at any rate, what you gave me was an
> example of a proof using a rule, not a formalization of that rule...
>
The rule doesn't formalize within the propositional calculus.
Which you are insisting upon doing. You have to express the rule in the
metalanguage. Are you taking logic thru the philosophy dept?
> > > 1. (what i'm inclined to call reductio ad falsum)
>
<snip>
I'll let you revise reductio ad falsum
> ???? P was my premise. A was my assumption A was discharged when i
> concluded ~A. thus using only the truth of P i concluded ~A--in other
> words i proved that P |- ~A.
>
You haven't explained what ???? P is.
> P is not atomic here--i'm assuming it has an inner structure that lets
> me conclude Q. (i'm not writing out a specific proof, i'm showing a
> schematic application of the rule (which is still not really a
> *formalization* of the rule))
>
It's too vague. You'll have to formalize this, description of internal
structure et. all with the metalanguage. Use "infer" or other
metalanguage expressions. Don't use the symbol "->" to mean infer, it
is causing you confusion.
> > > 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.
>
> again, A is not atomic, this is the sort of outline they give in many
> books of these sorts of proof.. i.e. imagine that A was "Q&~Q" for the
> simplest case. then this would definitely yield a proof of |- ~A .
> at any rate these are just examples of these rules and not precise
> formulations of them.
>
Yes |- A&~A -> ~A. So you're done.
All the outline is saying is
|- (A -> Q&~Q) -> ~A
Or to use words
If you assume A and can derive Q and ~Q, then you can infer ~A
To restate the outline. From
A |- Q, ie assuming A and deriving Q
A |- ~Q, ie assuming A and deriving ~Q
conclude
|- ~A
> my understanding is that PC uses several axioms and one rule (MP),
> whereas ND uses many rules and no axioms. i'm not thinking of PC at
> all, although i understand that they both begin with a list of
> premises.
>
Yes, ND is an inference or rule logic.
I suggest PC as it's clearer, able to easily express theorem schemata in a
single line while ND has to labor with ... sort of stuff to express the
same theorem or rule schemata. Does your text prove the equivalence of PC
and ND? That is a essential methatheorm for any logic text that
considers both PC and ND.
> > 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
>
> this one doesn't seem sufficiently general-- couldn't you have P->Q&~Q
> withought P->~P? or at the very least, you could get the former in
> fewer steps... so we can say:
>
Mathformlaswithnospacesaren'teasytoread!
> P -> Q&~Q |- ~P
>
> > P -> Q, P -> ~Q |- ~P
>
> yes i know this one as 'impossible antecent'
>
Note: (P -> Q&~Q) <-> (P -> Q) & (P -> ~Q)
So they are the same and all these distincitions of narrow interest.
> so, the formulations immediately above are examples of rules that could
> work *in conjunction* with CP to yield the proofs in my example--this
> places the burden of describing the rule on CP--how do we precisely
> describe the rule of Conditional Proof?
>
I'm not recalling what that is. I'd first express it as theorem
P,Q,R... |- A
in PC and then transcribe it to the cumbersome ND.
ND, tho easy to teach and philosophize about, lacks the expressive
power of PC and in philosophical logic, the essential precision of
mathematical logic is likely neglected.
Torkel Franzen
> I suggest PC as it's clearer, able to easily express theorem schemata in a
> single line while ND has to labor with ... sort of stuff to express the
> same theorem or rule schemata.
Suggest PC for what?
> ND, tho easy to teach and philosophize about, lacks the expressive
> power of PC and in philosophical logic, the essential precision of
> mathematical logic is likely neglected.
I take it you're not all that well acquainted with the literature on
natural deduction.
William Elliot
> William Elliot <ma...@hevanet.remove.com> writes:
>
> > I suggest PC as it's clearer, able to easily express theorem schemata in a
> > single line while ND has to labor with ... sort of stuff to express the
> > same theorem or rule schemata.
>
> Suggest PC for what?
>
For the stuff you clipped.
> > ND, tho easy to teach and philosophize about, lacks the expressive
> > power of PC and in philosophical logic, the essential precision of
> > mathematical logic is likely neglected.
>
> I take it you're not all that well acquainted with the literature on
> natural deduction.
>
I'm acquinted with the various forms of ND, their equivalent PC
forms and the metatheorems showing their equivalence.
ND is useful for outlining various schools of logic, intuitionist,
classical, positive and natural. What do you know about ND that I don't?
Torkel Franzen
> I'm acquinted with the various forms of ND, their equivalent PC
> forms and the metatheorems showing their equivalence.
Then I'm puzzled by your statement that natural deduction "lacks
the expressive power of PC". What are you referring to? Further,
what do you have in mind in speaking of a Hilbert-style formalization
(which, I assume, is what you mean by PC) as "clearer"? What "loss
of precision" in connection with ND (if you think there is such)
do you see?
William Elliot
> William Elliot <ma...@hevanet.remove.com> writes:
>
> > I'm acquainted with the various forms of ND, their equivalent PC
> > forms and the metatheorems showing their equivalence.
>
> Then I'm puzzled by your statement that natural deduction "lacks
> the expressive power of PC". What are you referring to? Further,
I don't recall as apropos context has been removed.
> what do you have in mind in speaking of a Hilbert-style formalization
I don't recall having invoked Hilbert.
> (which, I assume, is what you mean by PC) as "clearer"? What "loss
> of precision" in connection with ND (if you think there is such)
> do you see?
>
That question is out of context (ie context not included). Here's some
random thoughts generated from the accumulated recollection of the
gibbering gibberish of this thread.
Three versions of
p & (p -> q) -> q
p -> q, p |- q
from |- p
|- p -> q
conclude
|- q
p
assume p
...
q
q
Torkel Franzen
> I don't recall as apropos context has been removed.
So you don't remember saying these things? Well, then I can't expect
you to explain what you meant by them.
William Elliot
I remember you didn't like some things I said.
What they are, days later, I've little recollection.
As no reminders are included, there's nothing to explain.
Torkel Franzen
> I remember you didn't like some things I said.
> What they are, days later, I've little recollection.
Actually I quoted your statements. Since, apparently, they don't
seem at all familiar to you, I must congratulate you on being able
to write anything at all in the group.
William Elliot
that's in need of my extraordinarily drool eloquence. ;-)
Torkel Franzen
> Quite simple, this thread has contracted a Jabberwokie
> that's in need of my extraordinarily drool eloquence. ;-)
By all means drool along. If at some point you recognize the statements
quoted, you might want to explain what you meant by them.
William Elliot
For you, I'll do you a favor.
I'll give you the last word,
unless you prove me wrong.
Torkel Franzen
> I'll give you the last word,
> unless you prove me wrong.
Wrong about what, since you don't recognize your quoted statements
as your own?
futurist
Torkel Franzen wrote:
> adamg...@gmail.com writes:
>
> > the => means |-, here?
>
> We don't need to take => to refer to provability in any formal calculus.
> Just read G=>A as "A follows from G". The rule
>
> G,A => B
> --------
> G => A->B
>
> then allows us to conclude, given that B follows from G together with
> A, that A->B follows from G.
>
> > 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?
>
> To make good sense of the above, you need to specify the language
> you use and how |- is to be understood.
ok, and since |- seems to have a rather precise meaning attatched to
it, which prohibits such nesting, perhaps i should use the more
versatile "=>" (which i have seen used with nothing sort of five
different meanings) like so:
Conditional Proof:
P|-Q => P->Q
perhaps?
>
> > >
> > > ~A => Q ~A => ~Q
> > > -------
> > > => A
> >
> > Allen & Hand call the above rule "Impossible Antecedent", and they lump
> > all the rest under RAA...
>
> "Impossible Antecedent" is not standard terminology. But the
> important thing is that indirect proof is not constructively
> valid, but constructive reductio is.
hrm, i'm guessing you're referring to intuitionistic logic, which i'm
not exactly familiar with
> > ok, so with RAA often being used as an umbrella term, 'constructive
> > reductio' makes it clear that one means the one with no premises.
>
> Here I don't see what you have in mind.
just the form you told me was called constructive reductio:
---
> A (assumption)
> ...
> Q
> ...
> ~Q
> ~A
is one with no premises, and is presumably construed as a 'variety' of
RAA.
>
> > 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' ??
>
> Not that I know of.
i suppose we could simply call it the 'nonconstructive reductio' but
'reductio ad falsum' seems a rather good term to me--relating it to the
link i gave before
futurist
>
> Correct.
so does that mean i can't even use metavariables in turnstile
expressions? i.e.
⊢ ∀xΦx ↔ ∀yΦy (in unicode) or:
|- \-/x,Phi(x) <-> \-/y,Phi(y)
>
> > thus any nesting of |- would yield false statements
>
> Well, no, such nesting is grammatically ill-formed, hence simply
> meaningless.
i guess you're saying that only wffs are in the domain of the |-
function. i was thinking that |- was already at the level of natural
language, with (P|-Q)|-(P->Q) meaning "you can prove P->Q from P|-Q in
sentential logic", which is not meaningless but false...
>
> > so then how do you write out the rule for CP or RAA etc. in a formal
> > way rather than just showing an example of it?
>
> I don't understand the question. Do you think one needs to nest |-
> to state these rules?
one certainly needs to nest something. and i want to have a single
format for all ND rules.
futurist
> > I think what he means is this: In sequent-style proof systems,
> > CP has this form:
> >
> > A |- B
> > ----------
> > |- A -> B
> >
> > He's thinking of this as a kind of "higher-level" sequent
> >
> > (A |- B) ==> (|- A -> B)
> >
> > where ==> acts sort of like |-, except that the hypotheses
> > and conclusion are sequents, instead of statements.
>
> I see. Well, he should stop thinking that. :-)
>
> -chris
lol. but seriously, doesn't changing the middle connective to => fix
the problems from before?
Torkel Franzen
> Conditional Proof:
>
> P|-Q => P->Q
>
You can use any notation you like as long as you define a precise
syntax and semantics.
> just the form you told me was called constructive reductio:
>...
> is one with no premises, and is presumably construed as a 'variety' of
> RAA.
There can be any number of premises in both constructive reductio
and indirect proof - I just left them out in the notation.
> i suppose we could simply call it the 'nonconstructive reductio' but
> 'reductio ad falsum' seems a rather good term to me--relating it to the
> link i gave before
Your "reductio ad falsum" is constructively valid, and we don't need
non-constructive reductio to prove it as a derived rule.
futurist
William Elliot wrote:
> On Thu, 1 Sep 2005 adamg...@gmail.com wrote:
> > William Elliot wrote:
> > > On Sun, 28 Aug 2005, futurist wrote:
> >
> > > Becuase -> combines two formal statements into another.
> > > P |- Q is a statement about a sequence of formal statements.
> > > (P |- Q) |- R, is a statement about a sequence of formal statements
> > > because P |- Q isn't a formal statement.
> >
> > replace the last is with 'isn't' and i think i understand..
> >
> You do not understand. P |- Q is not a formal statement or well formed
> formula of the object language.
agreed
It is a statement of the metalanguage
> and can't be expressed with -> & v <-> (Ex) (Ax) of the object language.
agreed
so then why would you say that (P |- Q) |- R is a statement about a
sequence of formal statments?
>
> > > > 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.
> >
> > ok, but which set of formal statements to express the rule of CP?
> >
> Given
> |- P
> |- P -> Q
> infer
> |- Q
>
> You must use meta language "infer" and not object language "->" because
> |-P is not a statement of the object language.
modus ponens does NOT conclude a statement in the metalanguage, so no
rule which ends in "infer |- Q" could be modus ponens. you must mean:
Given
P
P->Q
infer
Q
which is expressed as P, P->Q |- Q (in this case the formluation comes
straight from Allen & Hand and not from me--they describe all the rules
in sequents like this, except for CP and RAA)
>
> > i just want a way to express, precisely and formally, the ND rules of
> > CP, and RAA, and possibly a way to distinguish various forms of RAA.
> > although at this point i can't see how to do that since |- doesn't
> > nest...
> >
> Then do so as I have show with MP without confusing the object language
> with the metalanguage.
see above: i think for a moment it was you who got them confused. and
we're no closer to describing CP precisely.
>
> > > > 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)
> >
> > i don't know about that--i was taught ND in two separate classes where
> > we had lists of premises, AND we could introduce assumptions for CP,
> > which is what i've done here. at any rate, what you gave me was an
> > example of a proof using a rule, not a formalization of that rule...
> >
> The rule doesn't formalize within the propositional calculus.
> Which you are insisting upon doing.
ok this part needs some explanation--how is using sequents in a
metalanguage 'insisting on formalization withing PC'? actually i
basically don't know PC at all, so i doubt i'm 'confusing it' with
ND--the use of sequents here is adopted from Allen & Hand, an ND book
if i understand correctly...
> You have to express the rule in the
> metalanguage.
yes, which is why i'm trying to express the rule using sequents,
because sequents are in the meta language. however you seem to keep
trying to push the rule into the meta-meta langage (english statments
about sequents), placing it out of reach for application in the object
language...
> Are you taking logic thru the philosophy dept?
the courses i mentioned were phil courses, although i just finished a
comp sci logic course as well (no talk of 'systems' at all in that one
though--just proof structure for mathematics, mostly)
> > > > 1. (what i'm inclined to call reductio ad falsum)
> >
> <snip>
>
> I'll let you revise reductio ad falsum
have you seen the name used in logic at all?
>
> > ???? P was my premise. A was my assumption A was discharged when i
> > concluded ~A. thus using only the truth of P i concluded ~A--in other
> > words i proved that P |- ~A.
> >
> You haven't explained what ???? P is.
>
> > P is not atomic here--i'm assuming it has an inner structure that lets
> > me conclude Q. (i'm not writing out a specific proof, i'm showing a
> > schematic application of the rule (which is still not really a
> > *formalization* of the rule))
> >
> It's too vague. You'll have to formalize this, description of internal
> structure et. all with the metalanguage. Use "infer" or other
> metalanguage expressions. Don't use the symbol "->" to mean infer, it
> is causing you confusion.
actually i never used '->' for infer, i used '|-' -- although i think
you're right that it is/was causing me confusion--it happens to be in
Allen and Hand that many of the 'rules' about what you can infer also
happen to be truths about what literal wffs follow from others (i.e. P
|- P v Q) but this appears to break down for CP and RAA... (although
i dont' totally understand why yet...)
>
> > > > 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.
> >
> > again, A is not atomic, this is the sort of outline they give in many
> > books of these sorts of proof.. i.e. imagine that A was "Q&~Q" for the
> > simplest case. then this would definitely yield a proof of |- ~A .
> > at any rate these are just examples of these rules and not precise
> > formulations of them.
> >
> Yes |- A&~A -> ~A. So you're done.
>
> All the outline is saying is
> |- (A -> Q&~Q) -> ~A
well, except it allows you to skip some steps that referring to that
theorem would not (i.e. you would have to have a substep where you
conclude "A -> Q&~Q"
>
> Or to use words
> If you assume A and can derive Q and ~Q, then you can infer ~A
> To restate the outline. From
> A |- Q, ie assuming A and deriving Q
> A |- ~Q, ie assuming A and deriving ~Q
> conclude
> |- ~A
the last thing you wrote is a weaker form, i think, (what another
poster called the 'constructive reductio', because it says that both Q
and ~Q have to follow from A *alone*--so it doesn't provide for the
following case:
Q
---
A (Assumption)
...
~Q
~A
since A |- Q is never demonstrated here (and may in fact be false)
>
> > my understanding is that PC uses several axioms and one rule (MP),
> > whereas ND uses many rules and no axioms. i'm not thinking of PC at
> > all, although i understand that they both begin with a list of
> > premises.
> >
> Yes, ND is an inference or rule logic.
> I suggest PC as it's clearer, able to easily express theorem schemata in a
> single line while ND has to labor with ... sort of stuff to express the
> same theorem or rule schemata. Does your text prove the equivalence of PC
> and ND? That is a essential methatheorm for any logic text that
> considers both PC and ND.
i believe i saw that equivalence awhile back--and i'm sure i'll
encounter it again when i take metalogic, although ND is definitely the
system for me right now, since i want to be applying it heavily to
natural language in some of my philosophy courses.
>
> > > 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
> >
> > this one doesn't seem sufficiently general-- couldn't you have P->Q&~Q
> > withought P->~P? or at the very least, you could get the former in
> > fewer steps... so we can say:
> >
> Mathformlaswithnospacesaren'teasytoread!
>
> > P -> Q&~Q |- ~P
> >
> > > P -> Q, P -> ~Q |- ~P
> >
> > yes i know this one as 'impossible antecent'
> >
> Note: (P -> Q&~Q) <-> (P -> Q) & (P -> ~Q)
> So they are the same and all these distincitions of narrow interest.
>
> > so, the formulations immediately above are examples of rules that could
> > work *in conjunction* with CP to yield the proofs in my example--this
> > places the burden of describing the rule on CP--how do we precisely
> > describe the rule of Conditional Proof?
> >
> I'm not recalling what that is. I'd first express it as theorem
> P,Q,R... |- A
> in PC and then transcribe it to the cumbersome ND.
> ND, tho easy to teach and philosophize about, lacks the expressive
> power of PC
how so? you just said yourself that they are equivalent.
> and in philosophical logic, the essential precision of
> mathematical logic is likely neglected.
i cannot decode this sentence--do you mean that PC is more 'precise'
than ND?
futurist
Torkel Franzen wrote:
> "futurist" <adamg...@adamgolding.com> writes:
>
> > Conditional Proof:
> >
> > P|-Q => P->Q
> >
>
> You can use any notation you like as long as you define a precise
> syntax and semantics.
i want to use standard notation whenever possible for my purposes.
>
> > just the form you told me was called constructive reductio:
> >...
> > is one with no premises, and is presumably construed as a 'variety' of
> > RAA.
>
> There can be any number of premises in both constructive reductio
> and indirect proof - I just left them out in the notation.
>
> > i suppose we could simply call it the 'nonconstructive reductio' but
> > 'reductio ad falsum' seems a rather good term to me--relating it to the
> > link i gave before
>
> Your "reductio ad falsum" is constructively valid, and we don't need
> non-constructive reductio to prove it as a derived rule.
ok, the main distinction i'm trying (hoping) to get at is this:
in ND, when you complete an argument, you either had premises or you
didn't. if you had (true) premises your conclusion is true. if you
had NO premises your conclusion is not only true but is a tautology.
in some applications of 'proof by contradiction' the contradiction is
between one of the formal (as opposed to material) consequences of your
assumption and one of the premises--that is to say, your assumption
contradicts the facts and is contingently false (reductio ad falsum,
i'd like to say.)
in the other case, the contradiction is independent of any premises,
and is a contradiction between two formal consequences of your
assumption, showing that your assumption is a *self* contradiction and
is thus *necessarily* false. (reductio ad absurdum, i'd like to say)
both are a 'proof by contradiction' or a 'reductio' in that in both
cases we are 'reducing' an assumption to a 'contradiction', but in the
first case it is a 'contradiction' of the *facts* (the premises), and
in the second case it is a *self-contradiction*--the first yields a
contingent conclusion, the second yields a necessary one.
these two modes of reasoning seem fundamentally different to me, and
thus seem to deserve separate names in ND, which is supposed to model
natural reasoning, after all. however i certainly don't want to assign
names to them without any heed of standard usage or etymology--hence my
attempt to logicize the terminology in the link in my first post.
PS however, i'm a little confused as to what distinguishes a
constructive from a nonconstructuve reductio (combining your
distinction and mine, we might even end up with a fourfold
distinction.. or not, please try to re-explain your distinction in
light of what i've written above)
Torkel Franzen
> these two modes of reasoning seem fundamentally different to me, and
> thus seem to deserve separate names in ND, which is supposed to model
> natural reasoning, after all.
But we use exactly the same rules in proving results of the form
G=>~A and in proving results of the form =>~A.
> PS however, i'm a little confused as to what distinguishes a
> constructive from a nonconstructuve reductio
Just examine the form of the rules. They are not the same.
Constructive reductio:
G,A => Q G,A => ~Q
--------------------
G => ~A
Indirect proof:
G,~A => Q G,~A => ~Q
----------------------
G => A
Constructive reductio always leads to a conclusion G => ~A. Indirekt
proof yields a conclusion G => A where A can have any form.
For example, you need to use an indirect proof to prove => pv~p.
Chris Menzel
Changing |- to =>? ==> to =>? I'd find it helpful if you would
write out what you have in mind completely, and say what you mean by
each symbol.
William Elliot
> William Elliot wrote:
> > You do not understand. P |- Q is not a formal statement or well formed
> > formula of the object language.
>
> agreed
>
> It is a statement of the metalanguage
> > and can't be expressed with -> & v <-> (Ex) (Ax) of the object language.
>
> agreed
>
> so then why would you say that (P |- Q) |- R is a statement about a
>
No it is nonsense neither a wff of the object language nor a coherent
statement of the meta language.
> > Given
> > |- P
> > |- P -> Q
> > infer
> > |- Q
> >
> > You must use meta language "infer" and not object language "->" because
> > |-P is not a statement of the object language.
>
> modus ponens does NOT conclude a statement in the metalanguage, so no
> rule which ends in "infer |- Q" could be modus ponens. you must mean:
>
> Given
> P
> P->Q
> infer
> Q
>
That is modus ponens. That is different that what you were trying
which is what I explained to you above which is a meta-theorem
that's an immediate result of MP and the definition of |-.
> which is expressed as P, P->Q |- Q
>
Correct.
> > You have to express the rule in the
> > metalanguage.
>
> yes, which is why I'm trying to express the rule using sequents,
> because sequents are in the meta language. however you seem to keep
> trying to push the rule into the meta-meta language (English statements
> about sequents), placing it out of reach for application in the object
> language...
>
The object language doesn't have the capacity to discuss itself!
> > Are you taking logic thru the philosophy dept?
>
> the courses i mentioned were phil courses, although i just finished a
> comp sci logic course as well (no talk of 'systems' at all in that one
> though--just proof structure for mathematics, mostly)
>
Oh, you've learned negative amounts of mathematical logic.
> > I'll let you revise reductio ad falsum
>
> have you seen the name used in logic at all?
>
No.
> actually i never used '->' for infer, i used '|-' -- although i think
> you're right that it is/was causing me confusion--it happens to be in
> Allen and Hand that many of the 'rules' about what you can infer also
> happen to be truths about what literal wffs follow from others (i.e. P
> |- P v Q) but this appears to break down for CP and RAA... (although
> i dont' totally understand why yet...)
>
Yes, |- doesn't mean infer, it means there's a sequence of wffs
such that ...
> > Or to use words
> > If you assume A and can derive Q and ~Q, then you can infer ~A
> > To restate the outline. From
> > A |- Q, ie assuming A and deriving Q
> > A |- ~Q, ie assuming A and deriving ~Q
> > conclude
> > |- ~A
>
> the last thing you wrote is a weaker form, i think, (what another
> poster called the 'constructive reductio', because it says that both Q
> and ~Q have to follow from A *alone*--so it doesn't provide for the
> following case:
>
> Q
> ---
> A (Assumption)
> ...
> ~Q
> ~A
>
You haven't defined and explained the semantics and syntax of
---
> since A |- Q is never demonstrated here (and may in fact be false)
>
> i believe i saw that equivalence awhile back--and I'm sure ill
> encounter it again when i take metalogic, although ND is definitely the
> system for me right now, since i want to be applying it heavily to
> natural language in some of my philosophy courses.
>
Spare me, what's that? Metalogic is to logic like metaphysics is to
physics?
> > >
> > I'm not recalling what that is. I'd first express it as theorem
> > P,Q,R... |- A
> > in PC and then transcribe it to the cumbersome ND.
> > ND, tho easy to teach and philosophize about, lacks the expressive
> > power of PC
>
> how so? you just said yourself that they are equivalent.
>
Then use ND, just more sure you've defined new symbols or new or extended
usage of established symbols.
> > and in philosophical logic, the essential precision of
> > mathematical logic is likely neglected.
>
> i cannot decode this sentence--do you mean that PC is more 'precise'
> than ND?
>
Before getting into the detains of logical precision, first be more
precise about your use of language using capital I and I'm instead of i
and i'm. Then with demostrated attention to details, attention to
precise mathematical and logical details will be easier.
futurist
of handwriting and not of ASCII. i meant using
(A |- B) => (|- A -> B) OR (A |- B) ==> (|- A -> B)
instead of
(A |- B) |- (|- A -> B)
|- meaning what other posters have said it should, that the following
wffs are provable from the preceding wffs,
=> or P ==> Q meaning "it is permitted in this system to infer Q from
P, but Q and P do not have to be wffs, but instead can be statments
about what syntactical relationships you have already proven in the
system.
futurist
does A have to be atomic in the first case?
> For example, you need to use an indirect proof to prove => pv~p.
if A is not atomic, couldn't you have any number of '~' symbols
'inside' the A? (i.e. in the wff that A represents?)
Torkel Franzen
> does A have to be atomic in the first case?
No.
> if A is not atomic, couldn't you have any number of '~' symbols
> 'inside' the A? (i.e. in the wff that A represents?)
Yes. What is the relevance of this observation?
futurist
Torkel Franzen wrote:
> "futurist" <adamg...@adamgolding.com> writes:
>
> > these two modes of reasoning seem fundamentally different to me, and
> > thus seem to deserve separate names in ND, which is supposed to model
> > natural reasoning, after all.
>
> But we use exactly the same rules in proving results of the form
> G=>~A and in proving results of the form =>~A.
indeed--i suppose i'm objecting more the appropriateness of the english
and latin names in the way they are currently mapped onto the logical
rules.
when i hear 'contradiction' i tend to assume 'self-contradiction' ..
i.e. the 'statment' which is sometimes represented by 'F' is said to be
a 'contradiction' meaning that it is a 'self-contradiction'--similarly
with more specific contradictions, i.e. P&~P, and so on. thus, it
would seem, for consistency's sake, that 'proof by contradiction'
should be sort for 'proof by self-contradiction'--furthermore
'reduction ad absurdum' is suppose to be 'poof by contradiction' and
thus RAA should be 'proof by self-contradiction'.
if there is a rule in ND which covers both what RAA and RAF should mean
in english latin, that rule should be given a more general name which
does not make it seem more specific than it is.
also, the result G=>~A could concievably be proven in either way--by a
self-contradiction in A, or by a contradiction between A and G--so i
suppose what i said earlier about the essential differenct--what
matters is not so much whether there *are* premises, but whether the
premises are required to generate the contradiction.
futurist
then you should be able to prove pv~p using either rule.
in the first case you assume A where A <=> ~(Pv~P)
in the secome case you assume ~A where A <=> (Pv~P)
(with <=> meaning formal equivalence here)
the second form seems like the first rule with an unnecessary tilde (~)
added in... am i missing something?
Torkel Franzen
> when i hear 'contradiction' i tend to assume 'self-contradiction' ..
> i.e. the 'statment' which is sometimes represented by 'F' is said to be
> a 'contradiction' meaning that it is a 'self-contradiction'--similarly
> with more specific contradictions, i.e. P&~P, and so on. thus, it
> would seem, for consistency's sake, that 'proof by contradiction'
> should be sort for 'proof by self-contradiction'
Well, it isn't.
Torkel Franzen
> then you should be able to prove pv~p using either rule.
>
> in the first case you assume A where A <=> ~(Pv~P)
> in the secome case you assume ~A where A <=> (Pv~P)
>
> (with <=> meaning formal equivalence here)
>
> the second form seems like the first rule with an unnecessary tilde (~)
> added in... am i missing something?
Using constructive reductio, you can only prove ~~(Pv~P).
futurist
> > > Given
> > > |- P
> > > |- P -> Q
> > > infer
> > > |- Q
> > >
> > > You must use meta language "infer" and not object language "->" because
> > > |-P is not a statement of the object language.
> >
> > modus ponens does NOT conclude a statement in the metalanguage, so no
> > rule which ends in "infer |- Q" could be modus ponens. you must mean:
> >
> > Given
> > P
> > P->Q
> > infer
> > Q
> >
> That is modus ponens. That is different that what you were trying
> which is what I explained to you above which is a meta-theorem
> that's an immediate result of MP and the definition of |-.
i may have mistakenly given the impression that i was interested in the
meta-theorem but i am not. i am interested in precisely describing the
rules of the object language that is ND.
>
> > which is expressed as P, P->Q |- Q
> >
> Correct.
>
> > > You have to express the rule in the
> > > metalanguage.
> >
> > yes, which is why I'm trying to express the rule using sequents,
> > because sequents are in the meta language. however you seem to keep
> > trying to push the rule into the meta-meta language (English statements
> > about sequents), placing it out of reach for application in the object
> > language...
> >
> The object language doesn't have the capacity to discuss itself!
of course not. which is why the rule OF a language cannot be expressed
IN that language. thus i am using sequents which are NOT part of ND,
and are thus ONE level up, and are in the *meta*-language, as opposed
to the meta-meta-language, which is where you place us when you connect
sequents with english. the rules should be expressed in the
meta-langage. the meta-meta-language would, i suppose, be better for
'rules about rules' but i don't see any need for that here.
it's nothing but the horiztonal line that separates the premises from
their consequences in every version of ND i've ever seen... at any rate
the sketch immediately above was not an attempt at a precise
formulation of the rule--it was just to discuss an example--an argument
which wouldn't fall under your description of the rule, thus showing
your description of the rule is not general enough, or at least that a
second rule is required.
>
> > since A |- Q is never demonstrated here (and may in fact be false)
> >
> > i believe i saw that equivalence awhile back--and I'm sure ill
> > encounter it again when i take metalogic, although ND is definitely the
> > system for me right now, since i want to be applying it heavily to
> > natural language in some of my philosophy courses.
> >
> Spare me, what's that? Metalogic is to logic like metaphysics is to
> physics?
no. the study of metaphysics was so named partially because aristotle's
metaphysics, which had no title from the author, came 'after' ('meta')
aristotle's physics in traditional compilations of his work.
metaphysics is not 'physics about physics', it is the study of
principles about causation, existence, truth, etc. which are intended
to have greater generality than topics discussed in real-world physics.
so the sense of 'meta' is similar but not the same.
metalogic is to logic as metamathematics is to mathematics. thus
metalogic and metamathematics are essentially the same discipline.
Godel's theorem is a metalogical/metamathematical theorm. statments
like 'ND is complete' are statements of metalogic.
> > > and in philosophical logic, the essential precision of
> > > mathematical logic is likely neglected.
> >
> > i cannot decode this sentence--do you mean that PC is more 'precise'
> > than ND?
> >
> Before getting into the detains of logical precision, first be more
> precise about your use of language using capital I and I'm instead of i
> and i'm. Then with demostrated attention to details, attention to
> precise mathematical and logical details will be easier.
I cannot decode the sentence mentioned above--do you mean that PC is
more 'precise' than ND?
futurist
removes (eliminates) one. they are only equally powerful if you have
DN (double negation).
William Elliot
about. Removal of references often means that I don't notice a reply to
me. Removal of essential context often means no well thought reply.
I've not the time nor the inclination for the clerical
chore of back tracking the thread to reconstruct the
line of thought. If you want intelligent and well thought
answers, then include the context pertinent to your reply
and to whom your are talking.
Please learn and use better math group manners as demonstrated
by other participants of this newsgroup and as described at
http://oakroadsystems.com/genl/unice.htm#quote
futurist
quick-reply feature, which i assumed would just quote the entire
previous message. anyway, this was a reply to Torkel Franzen's
distinction between contructive reductio and indirect proof. there is
another post which is in response to you which has all the appropriate
quotations in place.
William Elliot
> sorry about that--that was the first time i've used Google Groups'
> quick-reply feature, which i assumed would just quote the entire
> previous message. anyway, this was a reply to Torkel Franzen's
> distinction between contructive reductio and indirect proof. there is
> another post which is in response to you which has all the appropriate
> quotations in place.
>
Google quick-reply feature for math, science and serious discussion
sucks big time. Don't use it except for the frivolous of yack yack
newgoupies for which it's designed. Upon hearing Google was getting
greedy with public stock offering, I knew it was going to deteriorate.
Indeed and alas, my foreknowledge wasn't disappointed.
Use the include reply feature and trim out of it only that context that
has been resolved or nor longer pertinent to the continuation.
Related reading at http://oakroadsystems.com/genl/unice.htm
I hadn't noticed any replies addressed to me.
Note, I read by new arrivals and not by thread.
BTW the way, using capital "I" would polish your posts
toward appearing studious and scholarly.
adamg...@gmail.com
William Elliot wrote:
> On Tue, 6 Sep 2005, futurist wrote:
>
> > sorry about that--that was the first time i've used Google Groups'
> > quick-reply feature, which i assumed would just quote the entire
> > previous message. anyway, this was a reply to Torkel Franzen's
> > distinction between contructive reductio and indirect proof. there is
> > another post which is in response to you which has all the appropriate
> > quotations in place.
> >
> Google quick-reply feature for math, science and serious discussion
> sucks big time.
so i've discovered--believe me i'm as big a fan of proper quotation as
you are (although i'm suprised that your newsreader doesn't let you
switch between threaded/new-arrivals on the fly by means of a
convenient keyboard shortcut--even when messages are properly quoted i
like to see the tree structure)
> Don't use it except for the frivolous of yack yack
> newgoupies for which it's designed. Upon hearing Google was getting
> greedy with public stock offering, I knew it was going to deteriorate.
> Indeed and alas, my foreknowledge wasn't disappointed.
while google groups' (beta) interface leaves much to be desired, one
can hardly complain that the massive archive that was dejanews returned
and was expanded, (and at no cost to the user)
>
> Use the include reply feature and trim out of it only that context that
> has been resolved or nor longer pertinent to the continuation.
> Related reading at http://oakroadsystems.com/genl/unice.htm
i know the nettiquite pretty well--i just don't know google's interface
that well yet.
>
> I hadn't noticed any replies addressed to me.
> Note, I read by new arrivals and not by thread.
sorry, the quotes were there but the "____ wrote:" header was
missing--this is the post here:
http://groups.google.com/group/sci.logic/msg/17b42846e1d3247f
>
> BTW the way, using capital "I" would polish your posts
> toward appearing studious and scholarly.
there are new and developing standards of language online. (consult
Crystal's book on language and the internet for an attempt at a
scholarly overview of it) i choose between 'i' and 'I' depending on the
level of formality i wish to convey. on sci.logic, which is a
discussion group and not an academic journal, i choose 'i' as it
conveys the level of formality at which i wish to discuss things--i do
not, however, speak in 13375p3ak or other such gibberish, nor do i
abuse traditional style to the point of obscuring content. the
'appearance' of studiousness is largely irrelevant.
William Elliot
Newsgroups: sci.logic
Subject: Re: reductio ad falsum versus reductio ad absurdum
William Elliot wrote:
> On Tue, 6 Sep 2005, futurist wrote:
>
> > sorry about that--that was the first time i've used Google Groups'
> > quick-reply feature, which i assumed would just quote the entire
> > previous message. anyway, this was a reply to Torkel Franzen's
> > distinction between contructive reductio and indirect proof. there is
> > another post which is in response to you which has all the appropriate
> > quotations in place.
> >
> > Google quick-reply feature for math, science and serious
> > discussion sucks big time.
> so i've discovered--believe me i'm as big a fan of proper quotation
> as you are (although i'm suprised that your newsreader doesn't let
> you switch between threaded/new-arrivals on the fly by means of a
> convenient keyboard shortcut--even when messages are properly quoted
> i like to see the tree structure)
It does and it isn't convenient when there are scores of posts in several
math groups and forums. The quick-reply feature works both ways. Those
who use it frequently get a quick no-reply from me. It cuts down the
number of posts to read and adequately consider to a manageable few. Even
so, with the up take of school, I've dropped two newsgroups.
> > Don't use it except for the frivolous of yack yack
> > newgoupies for which it's designed. Upon hearing Google was
> > getting greedy with public stock offering, I knew it was going to
> > deteriorate. Indeed and alas, my foreknowledge wasn't
> > disappointed.
> while google groups' (beta) interface leaves much to be desired, one
> can hardly complain that the massive archive that was dejanews
> returned and was expanded, (and at no cost to the user)
Ya, they fucked it up and it's no longer the great tool it was before they
went to stock market offerings and corporate greed.
> > I hadn't noticed any replies addressed to me.
> > Note, I read by new arrivals and not by thread.
> sorry, the quotes were there but the "____ wrote:" header was
> missing--this is the post here:
> http://groups.google.com/group/sci.logic/msg/17b42846e1d3247f
Oh spare me. Only if it's a slow night, which is won't be until xmas
vacation, I'm little inclined to spend extra time to open an outside link
and then go scrolling thru the site until I find the referenced material.
As I'm now composing off line from replies I've down loaded, it's
additional bother to reconnect, pull up the post and download it with the
next batch of downloaded email, clean it of all google stuff and hope that
there's no "press here for complete post" button. Well if I get around to
it after all the other stuff I've downloaded and if I remember to look for
it after a quick scan of new arrivals, and if none of them are more
> > BTW the way, using capital "I" would polish your posts
> > toward appearing studious and scholarly.
> there are new and developing standards of language online.
There are new and developing online standards of linguistic crap.
There are new and developing capitalist standards of corruption.
----