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.