Author 
Message 
Mike H science forum addict
Joined: 28 Apr 2005
Posts: 57

Posted: Tue Jul 18, 2006 8:56 pm Post subject:
Are Wikipedia's rules of inference correct?



You can find them here:
http://en.wikipedia.org/wiki/List_of_rules_of_inference
Universal Introduction:
P(b/a)

(Aa)P
Existential Instantiation:
(Ea)P
P(b/a)  Q

Q
What I don't understand is how I can deduce (Aa)P from (Ea)P with these
two inference rules.
Quote:  From Universal Introduction, I can infer (Aa)P from P(b/a). But then I
can infer (Aa)P from (Ea)P as well from Existential Instantiation. 
What's going on here? 

Back to top 


Chip Eastham science forum Guru
Joined: 01 May 2005
Posts: 412

Posted: Tue Jul 18, 2006 10:32 pm Post subject:
Re: Are Wikipedia's rules of inference correct?



Mike H wrote:
Quote:  You can find them here:
http://en.wikipedia.org/wiki/List_of_rules_of_inference
Universal Introduction:
P(b/a)

(Aa)P
Existential Instantiation:
(Ea)P
P(b/a)  Q

Q
What I don't understand is how I can deduce (Aa)P from (Ea)P with these
two inference rules.
From Universal Introduction, I can infer (Aa)P from P(b/a). But then I
can infer (Aa)P from (Ea)P as well from Existential Instantiation.
What's going on here?

Think of P as a sentential formula "about" a. P(b/a) is the
result of "substituting" b for a.
You omitted the restriction given for Universal Introduction
(or Universal Generalization), that b is not free in (Aa)P or
in any nondischarged assumption.
These are clues that what is being described is a scheme
of inference rules derived from metatheorems about the
predicate calculus. Basically, it is a metatheorem that if
you can prove P(b/a), where b is a variable not bound in P,
in the predicate calculus, you could also prove (Aa)P(a).
Intuitively if a proof "works" for a completely nonspecific
b ("free term" not appearing in (Aa)P or any pending
assumption) to show P(b/a), the proof can be refactored
(using AxGen where necessary) to prove (Aa)P.
The rule of Existential Elimination is sometimes called
Rule C and illustrates the potential for "undischarged
assumptions" in this style of proof.
Note that the antecedents are:
(Ea)P
and: P(b/a)  Q
Then infer as consequence: Q
where b does not occur free in (Ea)P or in Q, or in any
undischarged assumption. Here P(b/a) was (for the
purpose of deducing Q in the second antecedent) an
assumption that has just been "discharged" by the
effect of Rule C (Existential Elimination).
The intuitive understanding is that we temporarily
reason about the "existential" term satisfying the
condition P on a, replacing it by (say) free variable
b in P(b/a), then proceeding to establish (deduce)
Q where Q no longer mentions b (b does not appear
free in Q). Q is then established free and clear of
any particular dependence on the choice of term
b that would "realize" (Ea)P, and so Q must (as
a metatheorem of the predicate calculus) be provable
without resorting to the shortcut of Rule C.
regards, chip 

Back to top 


Mike H science forum addict
Joined: 28 Apr 2005
Posts: 57

Posted: Tue Jul 18, 2006 11:39 pm Post subject:
Re: Are Wikipedia's rules of inference correct?



Chip Eastham wrote:
Quote:  Mike H wrote:
You can find them here:
http://en.wikipedia.org/wiki/List_of_rules_of_inference
Universal Introduction:
P(b/a)

(Aa)P
Existential Instantiation:
(Ea)P
P(b/a)  Q

Q
What I don't understand is how I can deduce (Aa)P from (Ea)P with these
two inference rules.
From Universal Introduction, I can infer (Aa)P from P(b/a). But then I
can infer (Aa)P from (Ea)P as well from Existential Instantiation.
What's going on here?
Think of P as a sentential formula "about" a. P(b/a) is the
result of "substituting" b for a.
You omitted the restriction given for Universal Introduction
(or Universal Generalization), that b is not free in (Aa)P or
in any nondischarged assumption.
These are clues that what is being described is a scheme
of inference rules derived from metatheorems about the
predicate calculus. Basically, it is a metatheorem that if
you can prove P(b/a), where b is a variable not bound in P,
in the predicate calculus, you could also prove (Aa)P(a).
Intuitively if a proof "works" for a completely nonspecific
b ("free term" not appearing in (Aa)P or any pending
assumption) to show P(b/a), the proof can be refactored
(using AxGen where necessary) to prove (Aa)P.
The rule of Existential Elimination is sometimes called
Rule C and illustrates the potential for "undischarged
assumptions" in this style of proof.
Note that the antecedents are:
(Ea)P
and: P(b/a)  Q
Then infer as consequence: Q
where b does not occur free in (Ea)P or in Q, or in any
undischarged assumption. Here P(b/a) was (for the
purpose of deducing Q in the second antecedent) an
assumption that has just been "discharged" by the
effect of Rule C (Existential Elimination).
The intuitive understanding is that we temporarily
reason about the "existential" term satisfying the
condition P on a, replacing it by (say) free variable
b in P(b/a), then proceeding to establish (deduce)
Q where Q no longer mentions b (b does not appear
free in Q). Q is then established free and clear of
any particular dependence on the choice of term
b that would "realize" (Ea)P, and so Q must (as
a metatheorem of the predicate calculus) be provable
without resorting to the shortcut of Rule C.
regards, chip

Let me see if I understand you. I cannot deduce (Aa)P from (Ea)P
because in the derivation with Existential Elimination, P(b/a) occurs
as a discharged assumption. That is, we treat the b in P(b/a) as being
merely *something* unknown, rather than *anything possible*, and then
discharge our original assumption (from which we could wrongly deduce
(Aa)P). Am I right?
If so, shouldn't the restriction below Universal Introduction say
"discharged assumption" instead of "nondischarged assumption"? I don't
see why we can't derive (Aa) P from P(b/a) the way the rules are
explained there. 

Back to top 


Chip Eastham science forum Guru
Joined: 01 May 2005
Posts: 412

Posted: Wed Jul 19, 2006 12:01 am Post subject:
Re: Are Wikipedia's rules of inference correct?



Mike H wrote:
Quote:  Chip Eastham wrote:
Mike H wrote:
You can find them here:
http://en.wikipedia.org/wiki/List_of_rules_of_inference
Universal Introduction:
P(b/a)

(Aa)P
Existential Instantiation:
(Ea)P
P(b/a)  Q

Q
What I don't understand is how I can deduce (Aa)P from (Ea)P with these
two inference rules.
From Universal Introduction, I can infer (Aa)P from P(b/a). But then I
can infer (Aa)P from (Ea)P as well from Existential Instantiation.
What's going on here?
Think of P as a sentential formula "about" a. P(b/a) is the
result of "substituting" b for a.
You omitted the restriction given for Universal Introduction
(or Universal Generalization), that b is not free in (Aa)P or
in any nondischarged assumption.
These are clues that what is being described is a scheme
of inference rules derived from metatheorems about the
predicate calculus. Basically, it is a metatheorem that if
you can prove P(b/a), where b is a variable not bound in P,
in the predicate calculus, you could also prove (Aa)P(a).
Intuitively if a proof "works" for a completely nonspecific
b ("free term" not appearing in (Aa)P or any pending
assumption) to show P(b/a), the proof can be refactored
(using AxGen where necessary) to prove (Aa)P.
The rule of Existential Elimination is sometimes called
Rule C and illustrates the potential for "undischarged
assumptions" in this style of proof.
Note that the antecedents are:
(Ea)P
and: P(b/a)  Q
Then infer as consequence: Q
where b does not occur free in (Ea)P or in Q, or in any
undischarged assumption. Here P(b/a) was (for the
purpose of deducing Q in the second antecedent) an
assumption that has just been "discharged" by the
effect of Rule C (Existential Elimination).
The intuitive understanding is that we temporarily
reason about the "existential" term satisfying the
condition P on a, replacing it by (say) free variable
b in P(b/a), then proceeding to establish (deduce)
Q where Q no longer mentions b (b does not appear
free in Q). Q is then established free and clear of
any particular dependence on the choice of term
b that would "realize" (Ea)P, and so Q must (as
a metatheorem of the predicate calculus) be provable
without resorting to the shortcut of Rule C.
regards, chip
Let me see if I understand you. I cannot deduce (Aa)P from (Ea)P
because in the derivation with Existential Elimination, P(b/a) occurs
as a discharged assumption. That is, we treat the b in P(b/a) as being
merely *something* unknown, rather than *anything possible*, and then
discharge our original assumption (from which we could wrongly deduce
(Aa)P). Am I right?
If so, shouldn't the restriction below Universal Introduction say
"discharged assumption" instead of "nondischarged assumption"? I don't
see why we can't derive (Aa) P from P(b/a) the way the rules are
explained there.

The discharged assumptions mean ones that have been in
effect removed from the proof, as if they never were introduced.
One set of these is from Rule C/Existential Elimination. A
similar thing occurs with proof by contradiction, where the
metatheorem is that if ~P  False, then you can give a direct
proof of P. (If you can deduce a contradiction from ~P, then
P is provable. Of course this only involves statement calculus,
in particular the deduction (meta)theorem, and needs no
quantifier logic from the predicate calculus.)
Here's why you can't carry formally carry out the proposed
deduction of (Aa)P from (Ea)P.
In the description of Existential Elimination, P(b/a) appears to
the left of the "deduction" sign, . Things that appear there
are called assumptions.
So, with that "undischarged assumption" involving a free
occurrence of b in P(b/a), you cannot "deduce":
P(b/a)  (Aa)P
by the application of Universal Introduction. That is the
point of the restriction you omitted in your citation of the
rule of Universal Introduction from Wikipedia.
Rather, the rule of Universal Introduction says only that
if you could prove P(b/a) without "special" assumptions
about b, ie. with no free appearances of b in undischarged
assumptions (or in (Aa)P for that matter), then you could
actually go back and step by step rework everything you
had done proving P(b/a) into a proof (using only axioms
of predicate calculus and a single rule of inference, the
wellknown modus ponens) of (Aa)P.
The proofs of these metatheorems (that if you can carry
out a proof of P(b/a) without special assumptions on b,
then you can prove (Aa)P directly; that if you can prove
(Ea)P and if you can _deduce_ from P(b/a) that Q holds,
then you can prove Q directly) are constructive. I can
recommend the Dover reprint of Angelo Margaris's
First Order Mathematical Logic for the details of these
and other such foundational results in logic.
regards, chip 

Back to top 


David C. Ullrich science forum Guru
Joined: 28 Apr 2005
Posts: 2250

Posted: Wed Jul 19, 2006 1:12 pm Post subject:
Re: Are Wikipedia's rules of inference correct?



On 18 Jul 2006 16:39:04 0700, "Mike H" <mikeh106@hotmail.com> wrote:
Quote:  Chip Eastham wrote:
Mike H wrote:
You can find them here:
http://en.wikipedia.org/wiki/List_of_rules_of_inference
Universal Introduction:
P(b/a)

(Aa)P
Existential Instantiation:
(Ea)P
P(b/a)  Q

Q
What I don't understand is how I can deduce (Aa)P from (Ea)P with these
two inference rules.
From Universal Introduction, I can infer (Aa)P from P(b/a). But then I
can infer (Aa)P from (Ea)P as well from Existential Instantiation.
What's going on here?
Think of P as a sentential formula "about" a. P(b/a) is the
result of "substituting" b for a.
You omitted the restriction given for Universal Introduction
(or Universal Generalization), that b is not free in (Aa)P or
in any nondischarged assumption.
These are clues that what is being described is a scheme
of inference rules derived from metatheorems about the
predicate calculus. Basically, it is a metatheorem that if
you can prove P(b/a), where b is a variable not bound in P,
in the predicate calculus, you could also prove (Aa)P(a).
Intuitively if a proof "works" for a completely nonspecific
b ("free term" not appearing in (Aa)P or any pending
assumption) to show P(b/a), the proof can be refactored
(using AxGen where necessary) to prove (Aa)P.
The rule of Existential Elimination is sometimes called
Rule C and illustrates the potential for "undischarged
assumptions" in this style of proof.
Note that the antecedents are:
(Ea)P
and: P(b/a)  Q
Then infer as consequence: Q
where b does not occur free in (Ea)P or in Q, or in any
undischarged assumption. Here P(b/a) was (for the
purpose of deducing Q in the second antecedent) an
assumption that has just been "discharged" by the
effect of Rule C (Existential Elimination).
The intuitive understanding is that we temporarily
reason about the "existential" term satisfying the
condition P on a, replacing it by (say) free variable
b in P(b/a), then proceeding to establish (deduce)
Q where Q no longer mentions b (b does not appear
free in Q). Q is then established free and clear of
any particular dependence on the choice of term
b that would "realize" (Ea)P, and so Q must (as
a metatheorem of the predicate calculus) be provable
without resorting to the shortcut of Rule C.
regards, chip
Let me see if I understand you. I cannot deduce (Aa)P from (Ea)P
because in the derivation with Existential Elimination, P(b/a) occurs
as a discharged assumption. That is, we treat the b in P(b/a) as being
merely *something* unknown, rather than *anything possible*, and then
discharge our original assumption (from which we could wrongly deduce
(Aa)P). Am I right?
If so, shouldn't the restriction below Universal Introduction say
"discharged assumption" instead of "nondischarged assumption"? I don't
see why we can't derive (Aa) P from P(b/a) the way the rules are
explained there.

It seems to me that you're misunderstanding the meaning
of the rule
[i]
P(b/a)

(Aa)P
You're applying this as though it read
[ii]
P(b/a) (Aa)P
or equivalently
[ii']  P(b/a) > (Aa)P.
but the two are very different! If [ii] were indeed a
valid rule then you could do what you're doing. But
the rule is [i], not [ii].
What's the difference? [i] says that if you can _prove_
P(b/a) (under whatever technical assumptions we're
omitting) then by definition you have proved (Aa)P.
That's correct. But that does not say that [ii]
holds! [ii] says something much stronger, in particular
something wrong, namely that if P(b/a) is _true_ then
(Aa)P is also true.
Say we're talking about arithmetic. If you've
proved (x+x)+x = x+(x+x) without assuming anything
about x then it follows that Ax((x+x)+x=x+(x+x))
is true! Because if (x+x)+x=x+(x+x) were not true
for every x then you would not have been able
to prove it without making some assumption
about x. This explains why [i] is correct.
On the other hand
(x>2) > Ax(x>2)
is not valid. Because if x = 3 then x > 2 is
true, but Ax(x>2) is false (because x could be 1.)
This shows that [ii] is not valid. Why does this
not show that [i] is not valid? Because you have
not given a _proof_ that x > 2 (without any assumptions
on x; if x = 3 then x > 2 holds, but that "x>3"
is an assumption about x).
************************
David C. Ullrich 

Back to top 


Google


Back to top 



The time now is Wed Sep 26, 2018 4:24 am  All times are GMT

