We do not believe in abstract entities. No one supposes that abstract entities -- classes, relations, properties, etc. -- exist in space-time; but we mean more than this. We renounce them altogether. We shall not forego all use of predicates and other words that are often taken to name abstract objects. We may still write "x is a dog", or "x is between y and z"; for here "is a dog" and "is between . . . and" can be construed as syncategorematic: significant in context but naming nothing. But we cannot use variables that call for abstract objects as values.1 In "x is a dog", only concrete objects are appropriate values of the variable. In contrast, the variable in "x is a zoological species" calls for abstract objects as values (unless of course, we can somehow identify the various zoological species with certain concrete objects). Any system that countenances abstract entities we deem unsatisfactory as a final philosophy.
Renunciation of abstract objects may leave us with a world composed of physical objects or events, or of units of sense experience, depending upon decisions that need not be made here. Moreover, even when a brand of empiricism is maintained which acknowledges repeatable sensory qualities as well as sensory events,2 the philosophy of mathematics still faces essentially the same problem that it does when all universals are repudiated. Mere sensory qualities afford no adequate basis for the unlimited universe of numbers, functions, and other classes claimed as values of the variables of classical mathematics.
Why do we refuse to admit the abstract objects that mathematics needs? Fundamentally this refusal is based on a philosophical intuition that cannot be justified by appeal to anything more ultimate. It is fortified, however, by certain a posteriori considerations. What seems to be the most natural principle for abstracting classes or properties leads to paradoxes. Escape from the paradoxes can apparently be effected only by recourse to alternative rules whose artificiality and arbitrariness arouse suspicion that we are lost in a world of make-believe.3
We decline to assume that there are infinitely many objects. Not only is our own experience finite, but there is no general agreement among physicists that there are more than finitely many physical objects in all space-time.4 If in fact the concrete world is finite, acceptance of any theory that presupposes infinity would require us to assume that in addition to the concrete objects, finite in number, there are also abstract entities.
Classical arithmetic presupposes an infinite realm of numbers. Hence if, in an effort to reconcile arithmetic with our renunciation of abstract entities, we were to undertake to identify numbers arbitrarily with certain things in the concrete world, we should thereby drastically curtail classical arithmetic; for, we cannot assume there are infinitely many such things.
Classical syntax, like classical arithmetic, presupposes an infinite realm of objects; for it assumes that the expressions it treats of admit concatenation to form longer expressions without end. But if expressions must, like everything else, be found within the concrete world, then a limitless realm of expressions cannot be assumed. Indeed, expressions construed in the customary way as abstract typographical shapes do not exist at all in the concrete world; the language elements in the concrete world are rather inscriptions or marks, the shaped objects rather than the shapes.5
The stock of available inscriptions can be vastly increased if we include, not only those that have colors or sounds contrasting with the surroundings, but all appropriately shaped spatio-temporal regions even though they be indistinguishable from their surroundings in color, sound, texture, etc. But the number and length of inscriptions will still be limited insofar as the spatio-temporal world itself is limited. Consequently we cannot say that in general, given any two inscriptions, there is an inscription long enough to be the concatenation of the two.Furthermore, there can be at most only as many inscriptions as concrete objects. Hence, if concrete objects are finite in number, there are bound to be some for which there are no names or descriptions whatever. Otherwise every concrete object would have to be the name or description of a unique and distinct concrete object; and we should thus be deprived of all predicates and connectives, to say nothing of synonyms, duplicate inscriptions, and non-inscriptions.
By renouncing abstract entities, we of course exclude all predicates that
are not predicates of concrete individuals or explained in terms of predicates
of concrete individuals. Moreover, we reject any statement or definition --
even one that explains some predicates of concrete individuals in terms of
others -- if it commits us to abstract entities. For example, until we find
some way of construing "is an ancestor of" in terms of "is
a parent of" other than the way the ancestral of a relation is usually
defined in systems of logic,6
the relationship between these predicates remains for us unexplained.
Some statements that seem to be about abstract entities can be rephrased
in well-known ways as statements about concrete objects. Thus, where "A"
and "B" are thought of as fixed terms and not as bindable
variables, the statement:
may be rephrased as:
The phrases "is an A" and "is a B" here
are predicates of concrete objects, and are regarded as naming nothing in
themselves; that is to say, the positions that they occupy are treated as
inaccessible to bound variables.
Certain statements that even involve explicit quantification over classes
are replaceable by equivalent statements that conform to the tenets of nominalism.
To take a simple example, the statement:
is equivalent to:
Statements purporting to specify sizes of finite classes of concrete objects
are also easily accommodated. Thus the statement:
may be rendered:
There are distinct objects x, y, and z such that anything
is an A if and only if it is x or y or z;
i.e.:
Obviously any statement affirming or denying that there are just, or at least,
or at most, a certain number of concrete individuals satisfying a given predicate
can be readily translated in similar fashion, provided the translation is
short enough to fit into the universe.8
The definition of ancestorhood in terms of parenthood according to Frege's
method seems to involve a class-variable even more essentially. The definiens
of "b is ancestor of c" would run thus:
b is distinct from c; and, for every class x, if c
is a member of x and all parents of members of x are members
of x then b is a member of x;
i.e.:
But we can translate this sentence also with the help of the notation "Part
st", meaning that the individual s is part (or all) of
the individual t.9 We
need only replace "class" by "individual", and "member"
by "part", provided we also stipulate that b be a parent
and c have a parent. This added stipulation insures that b and
c be single whole organisms, rather than fragments or sums of organisms.
In symbols, "b is ancestor of c" becomes:
b =/= c & (]u) Parent bu & (]w)
Parent wc & (x){Part cx & (y)(z)(Part
zx & Parent yz .--> Part yz) .--> Part bx}. The two-place predicate "is ancestor of" is, to borrow terminology
from the platonistic logic of relations, the (proper) ancestral of
the two-place predicate "is parent of". We have seen, above, how
it can be defined. But the scheme used there does not work for the ancestral
of every two-place predicate of individuals. It works so long as every individual
in the field of the predicate has some part that has no part in common with
any other individual in that field. At the present writing we know of no way
of defining the ancestral of every two-place predicate of individuals nominalistically.
A rather different problem is raised by such statements as:
As pointed out earlier, we are already able to deal with such statements
as "There is at least one cat and not at least one dog" and "There
are at least two cats and not at least two dogs". An alternation of enough
successive statements will be true if and only if there are more cats than
dogs, and because it will contain at least one component statement that is
true in view of the actual number of cats and of dogs. Use of this method
requires, first, knowledge that in all space-time there are not more than
so many (say fifty trillion) dogs, and second, a prodigious amount of writing
or talking. Even though the requisite knowledge be available, the practical
difficulties of actually writing or speaking the translation of the statement
about cats and dogs would be prohibitive.
A better method of translation makes use of the predicate "is part of"
and another simple auxiliary predicate: "is bigger than". The predicate
"is a bit" is then so defined that it applies to every object that
is just as big as the smallest animal among all cats and dogs. In other words,
"x is a bit" is defined to mean that for every y,
if y is a cat or a dog and is bigger than no other cat or dog, then
neither is x bigger than y nor is y bigger than x.
For brevity we shall call x a bit of z when x
is a bit and is part of z. Now if and only if there are more cats than
dogs will it be the case that every individual that contains at least one
bit of each cat is bigger than some individual that contains at least one
bit of each dog. (Such an individual will of course be spatio-temporally scattered.)
Accordingly we may translate the sentence "There are more cats than dogs"
as follows:
Every individual that contains a bit of each cat is bigger than some individual
that contains a bit of each dog. (Symbolic transcriptions are omitted here, as they will be given later for
parallel cases: D9-10.)
This method of translation has the great advantage, over the first method
suggested, that there is no practical difficulty about writing down an actual
translation, regardless of the multiplicity of individuals concerned. But,
like our method of defining the ancestral, it is not completely general. It
will still work if, in place of "is a cat" and "is a dog",
we choose any other two predicates each of which is such that the individuals
fulfilling it are discrete from one another. Thus it holds good for such a
case as:
and indeed for most cases where such numerical comparisons are made in ordinary
discourse. It has an important use in nominalistic syntax, as we shall see
later. Moreover, by a relatively simple change it can be made general enough
to work wherever each individual fulfilling either of the two predicates has
a part that has no part in common with any other individual fulfilling that
predicate. And in addition there are ways of modifying the method to take
care of certain cases where even this latter condition is not satisfied But
we have not found any general formulation that will cover all cases regardless
of how the individuals concerned overlap one another.
The method will, however, help us in finding a nominalistic reduction for
even so platonistic-sounding10
a statement as:
There are more age-classes than grade-classes in the White School. We just replace this by:
There are more age-wholes than grade-wholes in the White School, where an age-whole is the individual composed of all pupils in the school
who were born during a single calendar year, and a grade-whole is an individual
composed of all pupils who receive equally advanced instruction. The new sentence
is then readily translated in the same way as the one about cats and dogs.
A combination of devices already described enables us to translate a statement
like:
There are exactly one-third as many Canadians as Mexicans. Letting "the Mexican whole" stand for the individual that is comprised
of all Mexicans, the translation runs:
There are some mutually discrete wholes x, y, and z
such that each is comprised of Mexicans and such that x + y + z =
the Mexican whole; and there are exactly as many Canadians (in all) as there
are Mexicans in x and as in y and as in z. The last clause may then be further translated by a slight variation of the
method used in the example of cats and dogs.
The foregoing samples will illustrate some of the means that remain in our
hands for interpreting statements that prima facie have to do with
abstract entities. Certainly we have not as yet reached our goal of knowing
how to deal with every statement we are not ready to dispense with altogether.
But there is as yet no convincing reason for supposing the goal unattainable.
Some of the devices used above are rather powerful, and by no means all the
possible methods have been explored.
Since, however, we have not as yet discovered how to translate all statements
that we are unwilling to discard as meaningless, we describe in following
sections a course that enables us -- strictly within the limitations of our
language and without any retreat from our position -- to talk about certain
statements without being able to translate them.
It may naturally be asked how, if we regard the sentences of mathematics
merely as strings of marks without meaning, we can account for the fact that
mathematicians can proceed with such remarkable agreement as to methods and
results. Our answer is that such intelligibility as mathematics possesses
derives from the syntactical or metamathematical rules governing those marks.
Accordingly we shall try to develop a syntax language that will treat mathematical
expressions as concrete objects -- as actual strings of physical marks.11
Since one mark is as concrete as another, we can deal with such marks and
strings as "epsilon" and "(v)(v epsilon
v | v epsilon v)" quite as well as with ones like
"(" or "Eiffel Tower". But our syntax language must itself
be purely nominalistic; it must make no use of terms or devices that involve
commitment to abstract entities. It might seem that this program could be
carried out without any difficulty once we have specified that we are dealing
with concrete marks; but actually classical syntax has depended so heavily
upon platonistic devices in constructing its definitions that the nominalist
is faced with the necessity of finding new means of definition at almost every
step. Not only subsidiary terms, but such key terms as "formula",
"substitution", and "theorem" have to be defined by quite
new routes.12
The platonistic object language that our nominalistic syntax is to treat
of must contain notations for truth-functions, quantification, and membership.
All we need for these purposes are parentheses, variables, the stroke ''|''
of alternative denial, and the sign "epsilon" of membership. Parentheses
will serve both for enclosing alternative denials to indicate groupings and
for enclosing variables to form universal quantifiers. To simplify our syntactical
treatment, let us require that each alternative denial be enclosed in parentheses
even when it stands apart from any broader context. As variables we may use
"v", "v' ", "v'' ", etc.,
so that the simple typographical shapes of the object language reduce to six:
"v", " ' ", "(", ")", "|",
and "epsilon".
As already mentioned, the characters of our language are not these abstract
shapes -- which we, as nominalists, cannot countenance -- but rather concrete
marks or inscriptions. We can, however, apply shape-predicates to such individuals;
thus "Vee x" will mean that the object x is a vee
(i.e., a "v"-shaped inscription), and "Ac x"
will mean that x is an accent (i.e., a " ' "-shaped inscription),
and "LPar x" will mean that x is a left parenthesis,
and "RPar x" will mean that x is a right parenthesis,
and "Str x" will mean that x is a stroke (a "|"-shaped
inscription), and "Ep x" will mean that x is an epsilon.
But it happens actually that left parentheses and right parentheses are alike
in shape, and distinguishable only by their orientation in broader contexts.
It would appear therefore that instead of writing "LPar z",
to mean that x is intrinsically a left parenthesis, we should write
"LPar xy", meaning that x is a left parenthesis from
the point of view of its orientation within the longer inscription y;
and correspondingly for "RPar". Since however this exceptional treatment
is made necessary solely by a typographical idiosyncrasy, we may disregard
it. The reader may, if he likes, restore an intrinsic distinction between
left and right parentheses by thinking of each left parenthesis as comprising
within itself the straight uninked line joining its tips.
Our nominalistic syntax must contain, besides the six shape-predicates, some
means of expressing the concatenation of expressions. We shall write "Cxyz"
to mean that x and y and z are composed of whole characters
of the language, in normal orientation to one another, and contain neither
split-off fragments of characters nor anything extraneous, and that the inscription
x consists of y followed by z. The characters comprising
y and z may be irregularly spaced; furthermore the inscription
x will be considered to consist of y followed by z no
matter what the spatial interval between y and z, provided that x contains
no character that occurs in that interval.
The two remaining primitives of our syntax language are abbreviations of
the familiar predicates "is part of" and "is bigger than".
"Part xy" means that x, whether or not it is identical
with y, is contained entirely within y. "Bgr xy"
means that x is spatially bigger than y.
Our syntax language, then, contains the nine predicates "Vee",
"Ac", "LPar", "RPar", "Str", "Ep",
"C", "Part", and "Bgr", together with variables,
quantifiers and the usual truth-functional notations "V", "&",
etc. The variables take as values any concrete objects.
We now proceed to define certain useful auxiliary predicates. First, it is
convenient to have four-, five-, and six-place predicates of concatenation.
The definitions are obvious:
Also, later definitions will be shortened considerably if we can say briefly
that a given individual is a character of our object language. Since
a character is any concrete object that is either a vee or an accent or a
left parenthesis, etc., the definition runs:
The definition of final segment is strictly parallel:
We shall later want to be able to say that two inscriptions are equally long,
not in the sense that their ends are equally far apart but in the sense that
each inscription has as many characters as the other. Since the characters
comprising any inscription are discrete from one another, this numerical comparison
can be handled in a way explained in 4
above. We begin by so defining "Bit" for our present purposes that
"Bit x" means that x is just as big as every smallest
character.
It must not be supposed that, because accents are in general the smallest
characters of our object language, every accent will be a bit. For accents
may vary in size, and only the smallest characters, along with everything
that is just as big, will be bits.
An inscription x is longer than another, y, if x
contains more characters than y. Using the same method as for the example
of cats and dogs in 4
above -- where a verbal explanation is given -- we define:
Note that only inscriptions can be 'alike', in the sense here defined, since
only inscriptions can be equally long; and further, that likeness depends
solely upon the component characters and their order of occurrence, not upon
identical spacing.
(]x)(]y)(]z)(x =/= y & y
=/= z & x =/= z & (w)(Aw <-->:
w = x .V. w = y .V. w = z)).
b =/= c & (x){c epsilon x
& (y)(z)(z epsilon x & Parent yz
.-->. y epsilon x) .-->. b epsilon x}.
Clearly the above method of translation presupposes that an individual may be
spatio-temporally scattered, or discontinuous. It presupposes that continuity
is not necessary for concreteness. A broken dish is no less concrete than a
whole one, but merely has more complicated boundaries; and any totality of individuals,
however disperse in space and time, counts as an individual in turn. Individuals,
thus liberally construed, serve some of the purposes of classes, as is evident
from the above treatment of "ancestor". But it is by no means true
that we can in general simply identify any class of individuals with a scattered
single individual, and reconstrue "member" as "part". The
individual composed of all persons, e.g., has many parts that are not persons;
some of these parts are parts of persons, and some consist of many persons or
of parts of many persons. In the above analysis of "ancestor", we
were able to overcome this difficulty by inserting the clause "(]u)
Parent bu & (]w) Parent wc". Commonly, however,
this kind of difficulty admits of no such simple solution.
5. Elements of Nominalistic Syntax
6. Some Auxiliary Definitions
Cxyzwus = (]t)(Cxyt & Ctzwus).
Two inscriptions are equally long if neither is longer than the other.
We can now define what we shall mean by saying that two inscriptions are like
one another. Two characters are alike if both are vees, or both are accents,
etc. Two inscriptions x and y are alike if they are equally long
and if, for every two equally long inscriptions z and w such that
z is an initial segment of x and w is an initial segment
of y, the segments z and w end in like characters.
A variable of our object language is a vee, or a vee together with a string of one or more accents following it. We first define a string of accents as any inscription of which every part that is a character is an accent.
D14.
A variable is a vee or the result of concatenating a vee with a string of accents.
A quantifier will be simply a variable in parentheses. But it is more useful to define a string of (one or more) quantifiers directly. A method for doing this becomes evident when we reflect that any inscription will be a string of quantifiers if it begins and ends with facing parentheses and is such that every pair of facing parentheses within it frames an inscription that is either a variable or contains parentheses back to back.
An atomic formula of the object language consists of two variables with an epsilon between them.
We are supposing that the class logic to be developed in the object language will use one or another of the alternatives to the theory of types, so that the epsilons may grammatically occur between any variables without restriction.
The non-atomic formulas of the object language are constructed from the atomic formulas by quantification and alternative denial. In order to define an alternative denial we first need to be able to say that a given inscription x contains exactly as many left as right parentheses. This will be the case if x lacks parentheses altogether; and it will be the case also if the inscription which consists of all the left parentheses in x and the inscription which consists of all the right parentheses in x are equally long in the sense of D11. In symbols:
A quasi-formula will not necessarily be a formula, since the components of the alternative denial are not required to be formulas. But in terms of this notion of quasi-formula we can now easily define formula:
In other words, a formula is a quasi-formula such that every alternative denial in it is an alternative denial of quasi-formulas.
By requiring even the shortest alternative denials in a formula x to be alternative denials of quasi-formulas, the definition requires them to be alternative denials of atomic formulas or of quantifications of atomic formulas, and this makes them genuine formulas in the intuitively intended sense of the word. Accordingly, by requiring also the next more complex alternative denials in x to be alternative denials of quasi-formulas, the definition guarantees that these also will be formulas in the intuitively intended sense; and so on, to x itself.
Now that we have specified the characters and formulas of the object language within our nominalistic syntax language, the next problem is to describe the sorts of notational operations that pass for logical proof among the users of that object language. A full solution of this problem would consist in the formulation, in our syntax language, of a condition that is necessary and sufficient in order that an inscription x be a theorem of the object language.
The theorems are those formulas of the object language that follow from certain axioms by certain rules of inference. The axioms should be so chosen that we can obtain from them, by the rules of inference, every formula that is valid according to the logic of alternative denial and quantification and, in addition, a goodly array of formulas whose alleged validity is supposed to proceed from special properties of class-membership. We cannot aspire to completeness in this last regard, in view of Gödel's result.
There are many essentially equivalent sets of axioms suitable to the above purposes. The axioms that we shall adopt fall under three heads: axioms of alternative denial, axioms of quantification, and axioms of membership. In setting them forth let us understand "~ . . ." as short for " ( . . . | . . . ) ".
Axioms of alternative denial: All formulas of the form:
like letters being replaced by like formulas.
Axioms of quantification: All formulas of the forms:
If the reader reflects that the sign-combination " | ~" amounts to "-->", he will recognize in the forms (1) -- (3) a familiar set of axiom-schemata for quantification theory.16 Like capitals in (1) -- (3) are of course to be understood as replaced by like formulas, and the vees by like variables. The two brief provisos appended to (2) and (3), above, may be stated more precisely as follows: (i) the formulas supplanting the "R"s contain no free variables like the variables supplanting the vees, and (ii) the formula supplanting the "S" is like the formula supplanting the "P" except perhaps for containing other free variables, like one another, in place of all free variables like the variable supplanting the vee.
Axioms of membership: Here it happens that a limited list of specific expressions is adequate; e.g., Hailperin's.17 Let us suppose such a list put over into the primitive notation of our object language and set down here; then our axioms of membership are all inscriptions like those in the list.
In addition to the axioms, we need two rules of inference:
(1) From any formula, together with the result of putting a formula like it for "P" and any formulas for "Q" and "R" in "(P | (Q | R))", infer any formula like the one which was put for ''Q''.18
(2) From any formula infer any quantification thereof.
To reach a definition of "Axiom" we must first be able to define what it means to be an axiom of any given one of the five kinds above described. A simple auxiliary definition will be useful:
i.e., that x is a denial of y means that x is the alternative denial of y and some other inscription exactly like y.
Definition of "AADx", meaning that x is an axiom of alternative denial, is achieved by stating formally what we can observe from the general schema already given: that every axiom of alternative denial is an alternative denial of two formulas; one of these two main components is an alternative denial of formulas of which one is an alternative denial of formulas; the other of the two main components is an alternative denial of formulas of which one is an alternative denial of a formula with a formula like the denial of that formula, while the other is . . . etc., etc. In symbols
Formulation of "AQ1 x", meaning that x is an axiom of quantification of kind (1), proceeds in the same way; we shall omit the definition.
Formulation of "AQ2 x" offers the one additional difficulty that in order to express stipulation (i), appearing in the above description of the axioms of quantification, we must have a definition of free venable. A variable x is a free variable in an inscription y if x is a segment of y not followed by any additional accents in y, and if furthermore x is not a segment of any segment of y that consists of a formula preceded by a quantifier consisting of a variable like x framed in parentheses.
The definition of "AQ2 x" is then quite straightforward and may be omitted here.
Formulation of "AQ3 x" offers a further complication for nominalistic syntax. The problem lies in the notion of substitution, involved in stipulation (ii) . Let z and w be the respective formulas supplanting the "P" and "S" of (3), let y be the variable supplanting the "v", and let z be like the free variables which are to appear in w in place of the free variables like y in z. We have to find a way within nominalistic syntax of defining "Subst wzyz", meaning that the formula w is like the formula z except for having free variables like x wherever z contains free variables like y. Our method of definition depends upon the fact that the condition in the foregoing italics is equivalent to the following one: What remains when all free variables like y are omitted from the formula z is like what remains when some free variables like x are omitted from the formula w. The formal definition is as follows:
It was largely for the purpose of this definition that we so defined likeness of inscriptions as to allow their characters to be differently spaced.
Now that this definition is accomplished, the definition of "AQ3 x" offers no further difficulty (and is omitted here).
Definitions of axioms of the fifth and final kind -- the axioms of membership, "AM" -- present no problem; we can specify them in our syntax simply by spelling them out explicitly with the help of our primitive predicates.
We are then ready for a general definition of what it means for x to be an axiom of our object language. It means simply that x is an axiom of one of the five kinds specified.
D27.
An inscription is a theorem if it has a proof; and a proof is constructed by a series of steps of immediate consequence, starting from axioms. Roughly, a proof is describable as composed of one or more lines such that each is either an axiom or an immediate consequence of preceding lines. Actually we need not require that the so called 'lines' of a proof be at different levels on a page, or be segregated from one another by any other device. They could even be written end to end without intervening punctuation, and we could still single them out uniquely as separate 'lines'. For, the grammar of the object language is such that the result of directly concatenating two formulas z and w will never be a segment of a larger formula, nor will it contain as segments any formulas other than those that are segments of z alone or w alone. Accordingly it will be convenient in general to speak of x as a line of y (where y may or may not be a proof) if x is a formula that is part of y but not part of any other formula in y.
Line xy = (z)(Fmla z & Part xz & Part zy .<-->. z = x).
If a theorem is to be defined as a formula for which a proof exists, it is important not to demand that all lines of the proof be assembled in proper order in any one place and time. Accordingly we shall so define a proof as to allow it to consist of lines wherever they may be -- perhaps scattered at random throughout the universe, and perhaps not even all existing at any one moment or within any one century.
According to the rough characterization of proof proposed two paragraphs back, each line must be either an axiom or an immediate consequence of preceding lines. The reason for the word "preceding" here is to rule out cases where every line is deducible from other lines, in circular fashion, while not all lines are deducible ultimately from axioms. However, we must now resort to some other expedient for excluding such circularity; for we have chosen to dispense with the ordering of lines of a proof, and this deprives us of the notion of a 'preceding' line.
An expedient which will be shown to meet the requirements is this: We stipulate that if any individual y contains as parts some lines of a proof x but none that are axioms, then some line of x that lies in y must be an immediate consequence of lines of x that lie outside y. The following, then, is our definition:(1) is established as follows. Suppose x is a 'proof' in the sense of D29. We can begin our specification of an order of precedence among the lines of x by picking out, in an arbitrary order L1, L2 . . . , Lk, all those lines of x that are axioms. Next, from among the remaining lines of x, we pick one, call it Lk+1, which is an immediate consequence of lines from among L1, L2, . . . , Lk. (There will be such a line; for, by D29, that individual y which consists of all lines x except L1, L2, . . . , Lk must contain a line that is an immediate consequence of lines of x outside y.) Next, from among the remaining lines of x, we pick one -- call it Lk+2 -- which is an immediate consequence of lines from among L1, L2 . . . , Lk+1. (There will be such a one, for the same reason as before.) Continuing this, we eventually specify an order of precedence of the required kind.
(2) is established as follows. Suppose the lines of x can be counted off in some order such that each line is an axiom or an immediate consequence of earlier lines. Now consider anything y that contains some lines of x but none that are axioms. From among those lines of x that are parts of y, pick out the one that is earliest according to the assumed order. It must be either an axiom or an immediate consequence of earlier lines of x. But it is not an axiom, for y contains none of the lines of x that are axioms. Hence it is an immediate consequence of earlier lines of x; and those earlier lines are not in y. We see therefore that y contains a line of x that is an immediate consequence of lines of x outside y. Since y was taken as any individual containing some lines of x but none that are axioms, it follows that x is a proof in the sense of D29.
So it is now clear that D29, without stipulating any order among lines, gives us an adequate version of 'proof'.
Note incidentally that D29 abstains even from any requirement that a proof consist wholly of formulas; the 'lines' of a proof x are indeed formulas, but x may contain also any manner of additional debris without ill effect. Proofs are not in general 'inscriptions', in the sense of D5.
If a theorem is any inscription for which there is a proof, then an inscription is a theorem if and only if it is a line of some proof. But this formulation is a little too narrow. Given any inscription y for which a proof x exists, it will be true that for each inscription z that is like y, and that lies outside of x, a proof will also exist, consisting for example of z together with those lines of x that are not identical with y. Hence if y is a theorem all such inscriptions like it will also be theorems. But suppose that some inscription w that is like y lies embedded within some line t in the proof x, and suppose that no other line like t exists; in this case there may be no proof for w, so that some inscriptions like the theorem y may not be theorems. To prevent this anomaly, we construct our definition so that an inscription will be a theorem if and only if it is like some line of some proof. ("Like" has of course been so defined as to be reflexive.)
It may be interesting to observe in passing that the theoretical limitations just considered obtain under platonistic syntax as well, if that syntax construes expressions as shape-classes of inscriptions; for, shapes having no inscriptions as instances reduce to the null class and are thus identical.19 The platonist may indeed escape the limitations of concrete reality by hypostatizing an infinite realm of abstract entities -- the series of numbers -- and then arithmetizing his syntax; the nominalist, on the other hand, holds that any recourse to platonism is both intolerable and unnecessary.
At the same time, every advance we can make in finding direct translations for familiar strings of marks will increase the range of the meaningful language at our command.
6 The usual definition, which was first set forth by Frege in 1879 (Begriffschrift, p. 60), has become well known through Whitehead and Russell and other writers. It is presented once more in the next section.
19 According to the classical principles of syntax, any two expressions x and y have concatenate x^y, and moreover x^y is always distinct from z^w, unless the characters occurring in x and in y are successively the same as those in z and in w. This combination of principles is as untenable from the point of view of a platonistic syntax of shape-classes as from the point of view of nominalism.