FOM: The ineffability theorem: definitions and proof

[Neil Tennant]

Charlie Silver asked for a precise statement of the Ineffability
Theorem.

Notions:

L: any language for mathematics, be it first-order or higher-order,
containing the identity predicate =. A sentence of the form t=u will
be called an identity. Identities and negations of identities will be
called id-literals.

A system of proof for L produces finitary, effectively checkable
constructions whose 'results' (P,C) can be read off them. P is a
finite set of sentences of L. C is a sentence of L. We allow as a
special case the absurdity symbol #; and if C is #, then P is
non-empty. When the conclusion is #, we also call the proof a
refutation. Thus a system of refutation for L would produce constructions
whose results are of the form (P,#), with P a finite non-empty set of
sentences of L. A refutation with result (P,#) is said to be a
refutation of P.

We assume a semantics for L that characterizes the notions "sentence C
is true in model (interpretation) M" and "term t denotes individual m
in M".

A set of sentences is satisfiable iff there is an interpretation that
makes every one of its members true.  

A set of sentences is categorical iff there is exactly one
interpretation (up to isomorphism) that makes every one of its members
true.

When a model provides an interpretation of every non-logical
expression in L, we call it an L-model.

In an L-model M an individual is said to be definable iff there is
some L-term denoting that individual in M.

A system of proof for L is sound iff for every (P,C) that is the
result of a proof in that system, every interpretation of L that makes
all of P true makes C true also.

A system of refutation for L is sound iff for every (P,#) that is the
result of a refutation in that system, no interpretation of L makes
all of P true.

Every concept introduced so far is bread-and-butter stuff from
introductory undergraduate logic courses.

It is usual to think of systems of proof (and refutation) as given for
the language L, with no particular eye to the L-theories that those
systems will be used to develop. This is a 'uniformity assumption' for
logical systems, which we could consider relaxing. That is, we could
contemplate making our choice of proof- and refutation-systems
'sensitive to' the particular set X of axioms whose consequences we
are trying to capture.

We now state a very weak completeness requirement on satisfiable sets
X of L-sentences:

(I) For any extension L* of L (via finitely many new extralogical
expressions), there is a sound system of refutations such that for any
decidable (= recursive) and satisfiable set Y of id-literals in L*, if
(X union Y) has no model, then the system provides a refutation of
some finite subset of (X union Y).

No problem with (I), except for all the qualifications securing its
weakness. To motivate it for students, point out that it follows from
the usual statement of completeness. 

Ineffability Theorem: If M is a countably infinite L-model every one
of whose individuals is definable, then M cannot be categorically
described by any set X of M-truths in L for which (I) holds.

Proof: Let M be a countably infinite L-model every one of whose
individuals is definable. Thus for every individual m in M, there is
some term t_m denoting m in M. Let X be any set of M-truths in L.
Introduce a new name a.  This gives us the extension L* of L. Consider
the set X* defined as

	X union {~(t_m=a))|m in M}.

Suppose for reductio that X* has no model. Then by (I) there is a
(sound) refutation of some finite subset Z, say, of X*. Now extend 
the model M of X by letting the new name a denote a member of M not
denoted by any term occurring in any sentence in Z. This can be done,
since there are only finitely many such terms and M is infinite. We
thereby obtain a model for Z---which is impossible, since there is a
sound refutation of Z.

So by classical reductio ad absurdum, X* has a model after all. And
such a model cannot be isomorphic to M, because it has to contain a
denotation for the new name a distinct from every member of M. 

							QED 

Philosophical corollaries: we cannot simultaneously have deductive
access (from a set of axioms) to all truths about the system of
natural numbers, *and* characterize them categorically by means of the
axiom set we use. This is independent of what sort of language we use
(first order or higher order). The same holds for the system of
rational numbers.

The interest of the theorem stated this way is that all its
assumptions have been stripped down, and its conclusion has
considerable philosophical generality. (I) is an obvious
epistemological desideratum in the study of mathematical structures,
as is the requirement that proofs and refutations be finite.

The Ineffability Theorem could have been proved as early as 1918, but
it wasn't until the mid-1930s that anyone would have stated it this
way. It can be established without knowledge of any completeness or
compactness of Lowenheim-Skolem theorems, and without knowledge of
ultraproduct constructions. It was just there, ready to stare any
logician in the face, as soon as clarity had been attained about
logical consequence v. deducibility, and satisfiability v.
consistency, and the finitary nature of proof.

It should be accessible to any philosophy or mathematics undergraduate
who has done an introductory logic course taking them to the point
where they can translate English sentences into first-order (and
second-order) notation, but who have not yet been taken through the
completeness proof for first-order logic (or indeed even a
completeness proof for propositional logic).

Neil Tennant