Help in proving the OR induction theorem in class...

[jdiamond]

A theme that came up in attempting some of the class proofs was that
you need to show something like this:

(A v B) -> C

The problem is that this is an abbreviation for:
~(A v B) v C

As far as I know, we have no mechanism yet for distributing a not (nor
any concept of AND.) We could create this term through Expansion of
C, but in most of these proofs, you cannot simply assume C.

I'm not aware of us having any inference rule for combining sources of
implies, so I wanted to ask you guys if I missed something? Has
anyone found a way to create a composite implies in a proof?

Thanks for the ideas,
- Jeff

[Sandip Ray]

Hi,

I class I gave the following derived rule of inference (without
proof), and left the proof as an exercise for you to try.

Derived Rule [OR-Implication]:
Given (A => C) and (B => C), Derive (A \/ B) => C

We used this derived rule of inference in class to prove the theorems
in class. Note that this allows us to get a disjunction on the
antecedent of the implication, if you can prove the implications with
each antecedent separately.

I'm not sending a proof of this derived rule, since some of you are
hopefully working on it (although it's not a homework --- doing this
is completely optional, but I strongly urge you to do it), and I don't
want to blow the problem for you. Let me know if you need help trying
to prove this --- I'll be happy to help.

Thanks,

-- Sandip

DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=googlegroups.com; s=beta;
h=domainkey-signature:received:received:x-sender:x-apparently-to
:mime-version:content-type:received:date:x-ip:user-agent
:x-http-useragent:message-id:subject:from:to:reply-to:sender
:precedence:x-google-loop:mailing-list:list-id:list-post:list-help
:list-unsubscribe:x-beenthere-env:x-beenthere;
bh=6I5PVKA7E02FZPvczDSv+1cnv0rPZE8I0Ed3f4W0YiM=;
b=XzoI44Bjf5jF/p6/1dFfso2UB/SuYSIu+dSr0Lt0Zr9NVuVojp9ioPgJxtnh8oTwvA
Iq0/IlqMLKBSBe8yV9RSaI/inpFbU0EZrIZ69FFmt60THCSsrkUIPNY6gKEpdtWd6LIP
EfhI2Xx6uzSbiSdIwNlqanYCRrqqUeTgNjojg=
DomainKey-Signature: a=rsa-sha1; c=nofws;
d=googlegroups.com; s=beta;
h=x-sender:x-apparently-to:mime-version:content-type:date:x-ip
:user-agent:x-http-useragent:message-id:subject:from:to:reply-to
:sender:precedence:x-google-loop:mailing-list:list-id:list-post
:list-help:list-unsubscribe:x-beenthere-env:x-beenthere;
b=6G8aTxn5K7aF21aAKtBM9cqwz7B43RhgiCkTst3AJH337MH4cWTiA5me9lDcktA+Er
Q9gSb4Dmq5b4eOJAvHLfb3xLkuPsQIL+h4+zEgP9G8Zxvly8JRFTIY9sqKxZF2JAwEhP
PYxSr6SuS6hp3T3zb7OxPnWFugFjtji4897tE=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Wed, 10 Sep 2008 13:09:51 -0700 (PDT)
X-IP: 32.97.110.142
X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.0.1) Gecko/2008070206 Firefox/3.0.1,gzip(gfe),gzip(gfe)
From: jdiamond <jeffrey...@gmail.com>
Reply-To: utexas-cs38...@googlegroups.com
Sender: utexas-cs38...@googlegroups.com
X-Google-Loop: groups
Mailing-List: list utexas-cs38...@googlegroups.com;
contact utexas-cs389r-...@googlegroups.com
X-BeenThere-Env: utexas-cs38...@googlegroups.com
X-SpamAssassin-Status: No, hits=0.6 required=5.0
X-UTCS-Spam-Status: No, hits=-110 required=165