 Forum index » Science and Technology » Math
Author Message
Mike H

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? 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 non-discharged 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 Mike H

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 non-discharged 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 "non-discharged assumption"? I don't
see why we can't derive (Aa) P from P(b/a) the way the rules are
explained there. 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 non-discharged 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 "non-discharged 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
well-known 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 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 non-discharged 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 "non-discharged 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  Display posts from previous: All Posts1 Day7 Days2 Weeks1 Month3 Months6 Months1 Year Oldest FirstNewest First
 The time now is Sat Mar 23, 2019 10:15 am | All times are GMT Forum index » Science and Technology » Math
 Jump to: Select a forum-------------------Forum index|___Science and Technology    |___Math    |   |___Research    |   |___num-analysis    |   |___Symbolic    |   |___Combinatorics    |   |___Probability    |   |   |___Prediction    |   |       |   |___Undergraduate    |   |___Recreational    |       |___Physics    |   |___Research    |   |___New Theories    |   |___Acoustics    |   |___Electromagnetics    |   |___Strings    |   |___Particle    |   |___Fusion    |   |___Relativity    |       |___Chem    |   |___Analytical    |   |___Electrochem    |   |   |___Battery    |   |       |   |___Coatings    |       |___Engineering        |___Control        |___Mechanics        |___Chemical

 Topic Author Forum Replies Last Post Similar Topics Rules Angelo Campanella Acoustics 0 Thu Jul 20, 2006 3:42 pm Curve integral - correct or not? Daniel Nierro Undergraduate 2 Thu Jul 20, 2006 2:47 pm Fuzzy Inference System (FIS) Based Decision-Making Algori... amizo1@gmail.com Mechanics 0 Fri Jul 14, 2006 7:26 pm What is the correct expression in English? pkg Math 4 Sat Jul 08, 2006 1:47 pm Please tell me What I know it's Correct or not???(about EIS) EIS_MAN1984 Electrochem 1 Fri Jun 30, 2006 6:32 pm