The universe of finiteness

The tools I build on naïve foundations exist for use in arbitrary context. Their purpose is to let me define a context and obtain an assortment of truths arising from my definition that are simply some appropriately restricted truths expressed more generally by those tools. The tools are designed around a premis that they will be used in a context which entertains some values of the context's chosing plus all values the tools provide means to build given the values thus present in the context.

In particular, there's one value the tools know how to build for themselves - without needing to use any values provided by the context: empty. The tools provide the means to build an endless supply of other values out of empty: and, with a little help from that, to define the notion finite. A permutation is a mapping which accepts, as inputs, all the values it outputs but never maps distinct inputs to equal outputs. It's described as a permutation of its collection of inputs. A collection, S, is finite if every permutation of S produces all values in S as outputs.

The easiest illustration of what that means is to look at 1+i ←i on the natural numbers, {0, 1, 2, …}, which it permutes to {1, 2, 3, …}, so it doesn't produce 0 as an output, but manifestly is a permutation (in the sense just given). On any individual natural number, typically {0, …, n}, the corresponding permutation wants to give {1, …, 1+n} but 1+n isn't one of the inputs: so, if we're to get a permutation with {n, ..., 1} as outputs produced from inputs other than n, the only option for n's output is 0, which exactly plugs the gap for us. Note that even infinite collections have permutations which do produce all outputs (try the identity), the crucial difference is that they have some which don't.

An important thing one can do with a non-empty finite collection, S: for any member, a, of S, we have S = {a}&unite;N with N = {s in S: s is not a}. From any monic (N: f |N) we can construct a monic (S: g |S) by (:g:N) = f with g(a) = a. Since a isn't in N, which contains all f's outputs, no f(n) is a, hence nor is any g(n), with n in N. Since g is monic (S:|S) and S is finite, we know (S| g :S), hence (S| g :N): but we know g(a) = a isn't in N, so equally, given S = {a}&unite;N, (N| g :N). Now, (:g:N) = f, so this says (|f:) = N, so f is epic. Thus, for each a in any non-empty finite S, S without a is also finite. (This is the time-reverse of: the union of finite N with {a} is also finite.)

Written by Eddy.