Pairs and lists
Passes 7-0 / Skju
Adminned at 22 Jun 2013 21:54:31 UTC
Axioms:
* For all a and b, (a,b) is an ordered pair.
* For all a, b, c and d, (a,b) = (c,d) if and only if a = c and b = d.
* There exists exactly one a such that a is an empty list.
* For all a and b, if b is a list, then a:b is a non-empty list.
* For all a, if a is a non-empty list, then there exist b and c such that a = b:c and c is a list.
* For all a, b, c, and d, if b and d are lists, then [a:b = c:d if and only if [a = c and b = d]].
* For all a and b, if b is a list, then [the head of a:b is a, and the tail of a:b is b].
* For all a, b and c, if c is a list, then [a is an element of b:c if and only if [a = b or a is an element of c]].
* For all a, a is not an element of the empty list.
* For all a, b and c, if b and c are lists, then (a:b) ++ c = a:(b ++ c).
* For all c, if c is a list, then {} ++ c = c (where {} is the empty list).
We could, if we wanted to, add an axiom stating that every Atom is a list. Or that each value is an Atom if and only if it is not a list. Or that all values are lists. We could also say that there is a list a such that a = a:a. The possibilities for mischief are endless,
I think we could also add an axiom stating that for every list a, there is a list b such that any given value is an element of a if and only if it is not an element of b. That would be pretty weird,
nqeron:
why do I feel there’s room for Russel’s paradox? For all a implies a can be any type, even a list, so this is legit: (1,(2,3)). Is this intended?