A problem on induction and infinite ranges

Article View: sci.logic

Article #1016

#1016

From: Jordi Bataller i Mascarell
Date: Thu, 29 Apr 2004 14:02

42 lines
2049 bytes

First I use notation of and axioms of "A logic approach to discrete 
Math" by D. Gries and F. Schneider
(http://webster.cs.uga.edu/~gries/Logic/LogicalApproach.html)

Note:
u : union
v : or
E : exists
A : forall
== : equivalence
=> : implication
belongsTo: an element belongs to a set

I want to prove

(1) a belongsTo (u i |: B_i) == (E i | : a belongsTo B_i)

(a belongs to an infinite union of sets iff a belongs
  to (at least) one of the sets)

using axiom:

(2) a belongsTo (B u C) == (a belongsTo B) v (a belongsTo C)

I can prove easily by induction:

(3) (A k |: a belongsTo (u i |i<=k: B_i) == (E i |i<=k: a belongsTo B_i)

(This is a restriction of (1) for *any* k)

BUT (and this is the problem)

how can I prove (3) => (1)
or generalize (3) into (1) ?

(Of course (1) => (3))

Thanks

	Jordi Bataller
		Spain

Technical Details

Message-ID: <40910AF0.7050608@dsic.upv.es>

Path:

arc1-ca.pugleaf.net!archiver1.google.com!news1.google.com!news.glorb.com!newsfeed00.sul.t-online.de!t-online.de!irazu.switch.ch!switch.ch!newsmi-eu.news.garr.it!newsmi-us.news.garr.it!NewsITBone-GARR!news.rediris.es!news.uv.es!news.upv.es!not-for-mail

Show Full Headers

Complete Article Headers

X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 10cc56,40fa73e129685071,start
X-Google-Thread: 1100bb,2ff000a4e26fca1b,start
X-Google-Attributes: gid10cc56,gid1100bb,public
X-Google-ArrivalTime: 2004-04-29 05:18:03 PST
Path: arc1-ca.pugleaf.net!archiver1.google.com!news1.google.com!news.glorb.com!newsfeed00.sul.t-online.de!t-online.de!irazu.switch.ch!switch.ch!newsmi-eu.news.garr.it!newsmi-us.news.garr.it!NewsITBone-GARR!news.rediris.es!news.uv.es!news.upv.es!not-for-mail
From: Jordi Bataller i Mascarell <bataller@dsic.upv.es>
Newsgroups: sci.logic,es.ciencia.matematicas
Subject: A problem on induction and infinite ranges
Date: Thu, 29 Apr 2004 16:02:24 +0200
Organization: U.P.V.
Lines: 43
Message-ID: <40910AF0.7050608@dsic.upv.es>
NNTP-Posting-Host: ocell.gnd.upv.es
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: polaris.cc.upv.es 1083240146 8089 158.42.145.147 (29 Apr 2004 12:02:26 GMT)
X-Complaints-To: newsmaster@upv.es
NNTP-Posting-Date: 29 Apr 2004 12:02:26 GMT
User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.0) Gecko/20020623 Debian/1.0.0-0.woody.1
X-Accept-Language: en