Making Sense of Tony
- From: stevendaryl3016@xxxxxxxxx (Daryl McCullough)
- Date: 18 Sep 2005 12:06:31 -0700
Inspired by Brian Chandler, here's an attempt to make sense of
the various things that Tony has said.
Consider the following mathematical theory:
1. There are two sorts of variables, variables x,y,z, etc
range over individuals, and variables X,Y,Z, etc range over
sets of individuals. Functions and predicates have particular
"signatures", and it is illegal to use an individual as an
argument to a function that requires sets, and vice-versa.
2. There are a number of "built-in" primitive recursive
functions and operators on individuals: x+y, successor(x), x*y, etc.
There are binary relations <, >, <=, >= on individuals. We will
assume that these functions operations and relations are axiomatized
in the usual way. There is a constant individual symbol 0, and
a second constant symbol, K, which will be defined later.
3. We will also assume that there are pairing and unpairing functions:
pair, first, second, with the axioms
first(pair(x,y)) = x
second(pair(x,y)) = y
This allows us to code a function as a set of individuals (interpreted
as a set of ordered pairs).
4. There is a binary relation "in" between sets and
individuals: x in X means that x is an element of X. There is
a binary relation "subset of" on sets, which is axiomatized by
X subset of Y <-> forall x, x in X -> x in Y.
5. For each formula Phi(x) with one free individual variable, there
is an axiom (comprehension)
exists X, forall x, Phi(x) <-> x in X
6. There is an axiom (extentionality)
forall X,Y, (forall x, x in X <-> x in Y) -> X=Y
7. There is a predicate symbol on individuals: finite(x). This
is axiomatized by finite(0), and forall x, finite(x) -> finite(x+1).
8. There is a predicate symbol on sets of individuals: internal(x).
9. If Phi(x) is a formula that is expressible without using
"finite" or "internal", then there is an additional axiom
forall X (forall x, Phi(x) <-> x in X) -> internal(X)
10. There is an axiom (induction for internal sets):
forall X, (0 in X)
and forall x, (x in X -> (x+1) in X)
and internal(X)
-> forall x, x in X
11. There is an axiom (existence of an infinite individual)
not(finite(K)).
The following are definable predicates, so they are not used
for the comprehension axioms:
12. A set X is "bounded" if it has a largest element. Otherwise,
it is unbounded.
13. A set X is said to be an "initial segment" if X is
empty, or if 0 is in X and forall x, x+1 in X -> x in X. So,
{}, {0}, {0,1}, {0,1,2} are all initial segments. For any
individual x, the set of all y less than or equal to x is
an initial segment.
14. If an initial segment has a largest element, then its
size is 1 more than its largest element. So size({0}) = 1,
size({0,1}) = 2, etc. We'll define size({}) = 0.
If an initial segment is nonempty, and has no largest element,
then its size is undefined.
15. Two sets X and Y are said to be "the same size" if there is
an internal bijection between them. This allows us to define
size on sets that are not initial segments.
16. A set X is said to be "standard" if all of its elements
is finite.
17. A set X is said to be "finite" if its size is defined,
and is equal to a finite number.
18. A set X is said to be "hyperfinite" if its size is defined.
Okay, so given this structure and these axioms, we can conclude:
Induction only works for internal sets. In particular, the
set U of all standard individuals satisfies
0 in U
x in U -> x+1 in U
but U does not satisfy
forall x, x in U
The size of U is undefined. However, U is a subset of a set
whose size *is* defined: U is a subset of {0,1, ..., K} where
K is an infinite number.
What I think is true is the following:
If X is any internal set, and X is standard (contains only
finite elements) then X is finite.
So with this structure, Tony is *almost* right. Any *internal*
set that contains only finite elements must be finite. But there
are sets (e.g., U) that are not finite but which contain only
finite elements.
--
Daryl McCullough
Ithaca, NY
.
- Prev by Date: Re: Categorty theory - adding apples and oranges - disjoint union example needed
- Next by Date: Combinatorial problem
- Previous by thread: Bayesian networks and Markov chains
- Next by thread: Combinatorial problem
- Index(es):
Relevant Pages
|
