From: "Richard J. Petti" Newsgroups: sci.math.symbolic Subject: Re: Set theory with a program? Date: 15 May 1998 15:01:18 GMT Joerg Luecke; ; ; ; 52809 wrote in article <98051315493000.11695@student>... > Does there exist a program which can handel problems like: > > 1. A \ (B \ C) = (A \ B) \/ (A /\ C) is true of false? > 2. > ((A subset of (B /\ C)) > /\ (C subset of (A /\ B)) > /\ (B subset of (C /\ A)) > /\ (B is no subset of C) > /\ (C is no subset of B)) => (A = (B /\ C)) is true or false? > > A,B,C are sets; A /\ B means intersection; A \/ B union; > A \ B exclusion; > To make my point clear: > I rather want to know whether there exists a program which can handel these > problems than in the solutions of the problems themselves. > Such problems often occure in proofs in set theoretical topology and it is > always a loss of time to concentrade on expressions like those above. > > Thank you for any information. > -- > #~/.signature > full name > > The standard releases of PC Macsyma 2.3 and UNIX Macsyma 421 contain the MLTLOGIC package which does bivalued and multivalued logic computations. One of the commands checks for tautological consequences, which I believe is isomorphic to the problem of identity of sets. I have attached the output of one of the on-line demonstration files. -- Richard J. Petti Macsyma Inc. 20 Academy Street Arlington, MA 02174 / U.S.A. tel: 781-646-4550 fax: 781-646-3161 email: petti@macsyma.com URL: http://www.macsyma.com --------------------------------------------------------------- Tautological Consequence and Kleene's-Style Implication Original version written by: Dr. Eugenio Roanes Lozano Dept. Algebra, Univ. Complutense de Madrid (Spain) email: eroanes@eucmos.sim.ucm.es (c1) (oldprederror: prederror, prederror:false, if get('mltlogic,'version)=false then load(mltlogic))$ C:\mac23b\Macsyma2\library1\MLTLOGIC.fas being loaded. MLTLOGIC package is setting PREDERROR to FALSE. 1. Classic Bivalued Logic In classic bivalued logic S is a tautogical consequence of R iff (R implies S) is a tautology. (c2) tautologyp([P,Q], (P or Q) iff (Q or P) ) (d2) true (c3) taut_consequencep([P,Q], [P or Q, Q or P] ) (d3) true (c4) tautologyp([P,Q], (P and Q) implies P) (d4) true (c5) taut_consequencep([P,Q], [P and Q, P]) (d5) true Of course, "to_be or not to_be" is a tautology. (c6) tautologyp(to_be, to_be or not to_be ) (d6) true 2. Kleene's Style Multi-Valued Logics This doesn't hold in Kleene's style multi-valued Logics. (c7) taut_consequencep([P,Q], [P or Q,Q or P], 3) (d7) true (c8) tautologyp([P,Q], (P or Q) iff (Q or P), 3) (d8) false Examine what has happened in a trivial example: P is a tautological consequence of P. (c9) taut_consequencep([P], [P,P], 3) (d9) true but (P implies P) is NOT a tautology. (c10) tautologyp([P], P iff P, 3) (d10) false That happens because whenever P is true, then P is True. (c11) logic_table([P], [P,P], 3) [0] [0, 0] 1 1 1 [-] [-, -] 2 2 2 [1] [1, 1] (d11) done In this Logic (P iff P) is not always True (i.e. 1)! (c12) logic_table([P], [P,P,P iff P], 3) [0] [0, 0, 1] 1 1 1 1 [-] [-, -, -] 2 2 2 2 [1] [1, 1, 1] (d12) done In this logic, "to be or not to be" is not a tautology. (c13) tautologyp(to_be, to_be or not to_be, 3) (d13) false The following statement has no analog in bivalued logic. (c14) tautologyp([p,q], possibility(p) or not p, 3) (d14) true 3. Tautological Consequence and Lukasiewicz's-Style Implication Observe that the previous biconditional does hold in Lukasiewicz's three-valued Logic. (c15) logic_table([P], [P,P,P ifflu P], 3) [0] [0, 0, 1] 1 1 1 [-] [-, -, 1] 2 2 2 [1] [1, 1, 1] (d15) done Clean up (c16) (prederror: oldprederror, remvalue(oldprederror))$