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))$