How would you represent an abstract set on a computer?

Question

I'm trying to come up with a simple language for specifying mathematics.

We can't simply define a set as a collection of objects because that's meant for human understanding and that would also lead to tail chasing. And we can't create a datatype that does a good job of defining an arbitrary set. So we have to treat set either as atomic (by atomic I mean, the definition of it can't be broken down further), or... ?

Here's my idea using the language:

Def set S: (S,in,<,U,&,x,) where (x in S):atom; A,B:sets => A&B ... (here we define the logical rules of sets)

or something. Any ideas?

Answer 1

What you are describing makes me think about formalism, which was one of the most prominent or popular schools of mathematical philosophy with many famous mathematicians in favour of it, for instance David Hilbert.

The school (or philosophy) stated that a mathematical theory should be possible to express as systematic string manipulations according to rules (axioms). To prove a theorem would be to compute it's string and then use the string manipulation rules (axioms) together with previously "proven" strings (theorems) to prove new theorems.

For computer scientists and mathematicians this can be very exciting as strings are expressible and manipulable with computers, possibly leading to methods for machinated theorem proving / disproving, although the school of philosophy was popular many decades before the first electric computers.

Answer 2

Here's the language so far (an example string in the language):

Def (x in A):(atomic; bool) 
        iow (x "is a member of" A; x "is an element of" A)
    (a,b,...):atomic cld ("tuple"; "tuple of objects")
    (a,b):tuple cld "ordered pair"

Def set(s):atomic

Def (a;b;...):type <=> (a:type; b:type, ...)

Def (a and b; a or b; not a):(atomic; bool)

Def Let (A,B):sets
    (x not in A) <=> not (x in A)
    (x in A) and (x in B) <=> (x in (A & B):set)
    (x in A) or (x in B) <=> (x in (A U B):set)
    (x in A) and (x not in B) <=> (x in (A \ B):set)
    (x in A) and (y in B) <=> ((x,y) in (A x B):set)
    ((x in A) => (x in B)) <=> (A < B):bool

property: ((A U B) U C) = (A U (B U C))


synonyms:
    (A & B) = A intersect B = the intersection of A [and|with] B
        = (the intersection of the two sets)
    (A U B) = (A union B) = ...

Answer 3

I've worked on it all day and tested parts in grako. The culmination of my work is this little piece of crap:

Def (map; function) Let sets:(X;Y). Isa subset(X x Y):f sothat
     ((x,y) in f) and ((x,z) in f) => (y = z). 
     Iow (f is single-valued; f:X->Y).

It's very interesting and hard work to design a language.

Answer 4

Did some more work, so might as well share it. I've built up some classes in python and also (re-)designed some more of the language. The two sides aren't connected yet though, so nothing working yet.

Let S be a set.
Atom (IN) (x in S)

Let P,Q be boolean.
Def (if-then) (P => Q) = (not P) or Q.
Def (iff) (P <=> Q) = (P => Q) and (Q => P).

Let P,Q be bool .
Axiom (AND) P and Q <=> Q and P.
Axiom (OR) P or Q <=> Q or P.
Axiom (ARB-AND) for all i in I, P(i) <=> for i,j in I
Axiom 

Let A,B be sets.
Axiom (SET1) A < B <=> (x in A => x in B) <=> (For all x in A, x in B).
Axiom (SET2) A = B <=> (A < B and B < A)


Def (set intersection) A&B is a set such that: 
    x in A&B <=> (x in A and x in B).

Let I be a set.

Def (arbitrary set intersection) 
    &_(i in I) A_i is a set, A, such that:
    a in A <=> for all i in I, a in A_i.
    Notation: = &_i A_i = &A_i.

Def (arbitrary set union)
    U_(i in I) A_i is a set, A, such that:
    a in A <=> for some i in I, a in 

---------------- one proof per page --------------
Let A,B be sets.
Prop (Set intersection is commutative.) A & B = B & A.  

Proof:  x in A & B <=> (x in A and x in B)  (By definition of set intersection) (1)
        <=> (x in B and x in A)             (By axiom AND)  
        <=> x in B & A                      (Same reason as (1))
        Therefore, (x in LHS => x in RHS) and conversely. 
        We have, (LHS < RHS and RHS < LHS) => LHS = RHS (By axiom SET2.).
        QED.
--------------------------------------------------