> On Sun, Dec 11, 2011 at 10:10 PM, Dan Christensen > <firstname.lastname@example.org> wrote: > > Using another kind of computer-like language, DC > Proof, we can represent a function f mapping set A to > set B as follows: > > > > ALL(x):[x in A => f(x) in B] (replace "in" by > epsilon) > > > > B = [ f(x) for x in A ] >
B is not the range of f. The range of f is as subset of B in this case.
> would work for me but I'd still to flesh out f and > set A for this to > work. set type supports intersection, union and so > on. >
Intersections and unions are supported in my system as well.
> One question is how much to stress the set concept, > big in the 1960s > thanks to New Math and still a feature in Saxon, > Singapore etc. > (inheritors of much Dolciani -type thinking, > subclasses we might say). > > Why not just treat sets as one more type and stop > trying to consider > which type is "most primitive"?
There is a Set predicate in my system. Only if you declare an object to be a set can you apply the various axioms of set theory on it, e.g. selecting an arbitrary subset of it. This setup avoids a number of theoretical difficlties that makes the system easier to use and more "mathematical."
> I'm from the > Wittgensteinian camp on > matters mathematical, which nets me some ridicule > from Hansen, but I > say it saves me time. > > I'm not as tempted to waste so many hours on the > union and > intersection of sets when we could also be playing > with lists, tuples > etc. Lists of lists, or multi-dimensional lists, are > worth relatively > more time, sets relatively less.
I don't spend any time on unions and intersections in my tutorial, but if you want to make up lessons based on them, I do have built-in notation to handle them. All of the rest is also possible.
Write to me with your ideas, and maybe we can come up with something. But do have a look at the tutorial. I think you will find that it is a nice introduction to logic and proof. It takes you all the way from proving if A and B is true then B and A is also true to proof by induction and elementary number theory in 10 lessons.
> > Along the DM track, we're free to make these > base-level pioneering > adjustments because we're not hampered by the AM > (analog math) > detritus, the cultural baggage, the flotsam and > jetsam. A new kind > of freedom, helps build ubuntu (community spirit). > > DC Proof looks interesting. I used to play WFF 'n > Proof a lot, used > that RPN style if that's what it was, not unlike LISP > which they'll > hasten to tell you is different etc. Fun world. > > Kirby > > > > In words: For all x, if x is an element of A, then > f(x) is an element B. > > > > This simple notation completely characterizes all > functions of 1 variable. > > > > In the tutorial included with my program is a > worked example (#6) illustrating the composition of > functions, e.g. f(g(x)), along with suitable > exercises with hints and full solutions. > > > > Dan > > Download my DC Proof 2.0 freeware at > http://www.dcproof.com