Printer-friendly CSS, and nonfirstorderisability (original) (raw)

I recently discovered a CSS hack which automatically makes wordpress pages friendlier to print (stripping out the sidebar, header, footer, and comments), and installed it on this blog (in response to an emailed suggestion). There should be no visible changes unless one “print previews” the page.

In order to prevent this post from being totally devoid of mathematical content, I’ll mention that I recently came across the phenomenon of nonfirstorderisability in mathematical logic: there are perfectly meaningful and useful statements in mathematics which cannot be phrased within the confines of first order logic (combined with the language of set theory, or any other standard mathematical theory); one must use a more powerful language such as second order logic instead. This phenomenon is very well known among logicians, but I hadn’t learned about it until very recently, and had naively assumed that first order logic sufficed for “everyday” usage of mathematics.

Let’s begin with some simple examples of statements which can be expressed in first-order logic. If B(x,y) is a binary relation on two objects x, y, then we can express the statement

For every x, there exists a y depending on x such that B(x,y) is true

in first order logic as

\forall x \exists y: B(x,y)

whereas the statement

For every x, there exists a y independent of x such that B(x,y) is true

can be expressed as

\exists y \forall x: B(x,y).

Moving on to a more complicated example, if Q(x,x’,y,y’) is a quaternary relation on four objects x,x’,y,y’, then we can express the statement

For every x and x’, there exists a y depending only on x and a y’ depending on x and x’ such that Q(x,x’,y,y’) is true

as

\forall x \exists y \forall x' \exists y': Q(x,x',y,y')

(note that this allows y’ to depend on y also, but this turns out to be moot, because y depends only on x), and one can similarly express

For every x and x’, there exists a y depending on x and x’ and a y’ depending only on x’ such that Q(x,x’,y,y’) is true

as

\forall x' \exists y' \forall x \exists y: Q(x,x',y,y')

but it seems that one cannot express

For every x and x’, there exists a y depending only on x and a y’ depending only on x’ such that Q(x,x’,y,y’) is true (*)

in first order logic! For instance, the statement

To every finitely generated real vector space V one can associate a unique non-negative integer \dim(V) such that

  1. V, W are isomorphic if and only if \dim(V) = \dim(W);
  2. an injection from V to W exists if and only if \dim(V) \leq \dim(W);
  3. a surjection from V to W exists if and only if \dim(V) \geq \dim(W);
  4. \dim({\mathbb R}) = 1; and
  5. \dim(V \oplus W) = \dim(V) + \dim(W) for all V, W,

which is part of the fundamental theorem of linear algebra, does not seem to be expressible as stated in first order set theory (though of course the concept of dimension can be explicitly constructed within this language), even if we drop the uniqueness and restrict ourselves to just the assertion that \dim() obey, say, property 1, so that we get an assertion of the form (*). Note that the category of all finite-dimensional vector spaces is not a set (for reasons relating to Russell’s paradox) and so we cannot view \dim as a function. More generally, many statements in category theory dealing with large categories seem to not be expressible in first order logic.

I can’t quite show that (*) is not expressible in first-order logic, but I can come very close, using non-standard analysis. The statement

For every real numbers x and x’ there exists real numbers st(x) and st(x’) depending only on x and x’ respectively, such that st(x+x’) = st(x)+st(x’), st(xx’) = st(x) st(x’), st(1)=1, and st(x) is non-negative whenever x is non-negative, and also such that st(x) is not always equal to x

is true in the non-standard model of the real numbers, but false in the standard model (this is the classic algebra homework problem that the only order-preserving field homomorphism on the reals is the identity). Since the transfer principle ensures that all first-order statements that are true in the standard reals are also true in the non-standard reals, this means that the above statement cannot be expressed in first-order logic. If it weren’t for the “st(x) is not always equal to x” part, this would basically be of the form (*).

It seems to me that first order logic is limited by the linear (and thus totally ordered) nature of its sentences; every new variable that is introduced must be allowed to depend on all the previous variables introduced to the left of that variable. This does not fully capture all of the dependency trees of variables which one deals with in mathematics. In analysis, we tend to get around this by using English phrasings such as

… assuming N is chosen sufficiently large depending on \epsilon, and \delta chosen sufficiently small depending on N …

and

… where C can depend on k and d, but is uniform with respect to n and f …,

or by using the tremendously convenient O() and o() notation of Landau. One then takes for granted that one can eventually unwind all these phrasings to get back to a sentence in formal, first-order logic. As far as analysis is concerned, this is a fairly safe assumption, since one usually deals with objects in very concrete sets such as the real numbers, and one can easily model all of these dependencies using functions from concrete sets to other concrete sets if necessary. (Also, the hierarchy of magnitudes in analysis does often tend to be rather linearly ordered.) But some subtleties may appear when one deals with large categories, such as the category of sets, groups, or vector spaces (though in most applications, one can cap the cardinality of these objects and then one can represent these categories up to equivalence by an actual set). It may be that a more diagrammatic language (perhaps analogous to the commutative diagrams in category theory, or one based on trees or partially ordered sets rather than linearly ordered ones) may be a closer fit to expressing the way one actually thinks about how variables interact with each other. (Second-order logic is, of course, an obvious candidate for such a language, but it may be overqualified for the task. And, in practice, there’s nothing wrong with just using plain old mathematical English.)

[Update, Aug 27: bad link fixed.]