FAQFAQ   SearchSearch   MemberlistMemberlist   UsergroupsUsergroups 
 ProfileProfile   PreferencesPreferences   Log in to check your private messagesLog in to check your private messages   Log inLog in 
Forum index » Science and Technology » Math
Are Wikipedia's rules of inference correct?
Post new topic   Reply to topic Page 1 of 1 [5 Posts] View previous topic :: View next topic
Author Message
David C. Ullrich
science forum Guru


Joined: 28 Apr 2005
Posts: 2250

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

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
Back to top
Chip Eastham
science forum Guru


Joined: 01 May 2005
Posts: 412

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

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
Back to top
Mike H
science forum addict


Joined: 28 Apr 2005
Posts: 57

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

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.
Back to top
Chip Eastham
science forum Guru


Joined: 01 May 2005
Posts: 412

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

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
Back to top
Mike H
science forum addict


Joined: 28 Apr 2005
Posts: 57

PostPosted: Tue Jul 18, 2006 8:56 pm    Post subject: Are Wikipedia's rules of inference correct? Reply with 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.

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
Google

Back to top
Display posts from previous:   
Post new topic   Reply to topic Page 1 of 1 [5 Posts] View previous topic :: View next topic
The time now is Thu Dec 14, 2017 12:44 am | All times are GMT
Forum index » Science and Technology » Math
Jump to:  

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

Copyright © 2004-2005 DeniX Solutions SRL
Other DeniX Solutions sites: Electronics forum |  Medicine forum |  Unix/Linux blog |  Unix/Linux documentation |  Unix/Linux forums  |  send newsletters
 


Powered by phpBB © 2001, 2005 phpBB Group
[ Time: 0.0273s ][ Queries: 20 (0.0042s) ][ GZIP on - Debug on ]