[FOM] Mycielski's finitized theories

[A.P. Hazen]

   Todd Wilson mentions Jan Mycielski's "finitized" theories: theories
locally interpretable in a trivial theory with a finite model, but which in
a certain precise sense "encode" all the **mathematical content** of
standard, infinitary, theories of interest from the p.o.v. of f.o.m.  The
paper Wilson cites
	J. Mycielski, "Analysis without actual infinity", JSL 46:3, Sept
    	1981, pp. 625-633
presents the special case of a formalization of analysis, but Mycielski's
technique is general, applying to any First-Order theory: cf.
	J. Mycielski, "Locally finite theories," JSL 51:1, Mar
    	1986, pp. 59-62.

   The basic idea is beautifully simple, and can be thought of in pictorial
terms.  Suppose you are explaining what a First-Order sentence--- suppose
for illustration a prenex one starting AxEyAz--- means by drawing a
diagram.  "It means," you say, "that for any object you choose," --- here
you draw a big, bold, dot --- "there is another object" --- here a slightly
smaller dot --- "related to it thusly" --- arrows and such representing the
predicates in the atomic subformulas of the matrix containing x and y ---
"and such that for any further object" --- here a quick dot, maybe just a
small open circle --- "they are related so." --- further arrows.  The
picture you have drawn shows only finitely many objects, x in full view, y
a bit off to one side, and z at the horizon.  The First-Order sentence may
require an infinite model: in pictorial terms, this would be because when
you "change focus" and concentrate on, say, the object y [[formally: when
you instantiate the initial universal quantifier to the new variable, but
let's leave formulas out of this and think pictorially!]] you will only be
able to produce a picture similar to the first one by adding a NEW dot,
connected by arrows to y as y was originally to x.

   Back to formulas.  Mycielski's "finitized" version of a First-Order
theory has infinitely many new monadic predicates, and every quantifier in
a theorem of the finitized theory is restricted by one of them.  In terms
of the pictures, we can think of these predicates as saying how far into
the background an object is, and the AEA sentence of the original theory
goes into a "For every foreground object x, there is a middle distance
object y, such that for every not-TOO-distant object z..." sentence of the
finitized theory.  Mycielski's surprising observation was that, given an
axiomatization of the original, infinitary, theory, a fairly simple,
reasonably usable, quite perspicuous, axiomatization (not a finite
axiomatization, but recursive) can be given for the "finitized" theory.
The finitized theory has the ***mathematical content*** of the original
theory in the senses that
	(i) you'd draw exactly the same diagrams to show what its theorems
mean as you would for theorems of the original theory, and, formally
	(ii) you can recover any theorem of the original theory from a
theorem of the finitized theory by simply erasing the restricting clauses.

	There is a good description and discussion of Mycielski's technique
in Shaughan Lavine's (I've commended it before, but I'll say it again: VERY
GOOD) book "Understanding the Infinite."  (Lavine has told me in
conversation that his interpretation of the philosophical significance of
Mycielski's idea is not the same as Mycielski's, but it is interesting-- I
would say a significant contribution to the philosophy of mathematics--
even if it ISN'T authentic Mycielskiism.)

---

Allen Hazen
Philosophy Department
University of Melbourne