Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
Re: Are Wikipedia's rules of inference correct?
Posted:
Jul 18, 2006 8:01 PM
|
|
Mike H wrote:
> 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
|
|
|
|
