In this address, no attempt to deal with any problem of symbolic technique will be made, for even if a problem of this kind should be found that was suitable to the present occasion, I should probably lack sufficient competence in the handling of symbols to deal with it satisfactorily. It occurred to me, however, that it might be interesting to consider the nature of symbols in general, to point out certain characteristics peculiar to the symbols used by logicians and mathematicians, and to say something concerning the relations of these symbols to the knowledge of Nature. Although developments in the science of logic are not dependent on such an inquiry, it yet provides us with a perspective on the nature and importance of that science which we cannot gain so long as we attend only to the problems arising inside its field.

The symbolic relation. Our attempt to gain this perspective may well begin with the trite remark that nothing is intrinsically a symbol, but that anything is a symbol if and only if it symbolizes. Moreover, the relation called symbolizing is not a dyadic but rather a tetradic relation. That is, in order for something A to be a symbol of something B, there must be in addition C, a mind trained in a special way, and D, a certain manner in which that mind is occupied at the time. For although we do say, for instance, that a mark consisting of a little cross is the symbol of addition, the fact is of course that at times when that mark is not present to a mind, it does not symbolize addition or anything else. Moreover, even when it is present to a mind, it does not symbolize addition unless that mind has been trained in a certain manner; for obviously such a mark does not symbolize addition to the mind of a Hottentot or other wholly illiterate person.

This paper is an attempt to explain as non-technically as possible the principles and devices used in the various proofs of Gödel's Theorems and Church's Theorem.

Roman numerals in references shall refer to the papers in the bibliography. In the statements of Gödel's Theorems and Church's Theorem, we will employ the phrase “for suitable L.” The hidden assumptions which we denote by this phrase have never been put down explicitly in a form intelligible to the average reader. The necessity for thus formulating them has commonly been avoided by proving the theorems for special logics and then remarking that the proofs can be extended to other logics. Hence the conditions necessary for the proofs of Gödel's Theorems and Church's Theorem are at present very indefinite as far as the average reader is concerned. To partly clarify this situation, we will now mention the more prominent of these assumptions.

I. In any proof of Gödel's Theorems or Church's Theorem, two logics are concerned. One serves as the “logic of ordinary discourse” in which the proof is carried out, and the other is a formal logic, L, about which the theorem is proved. The first logic may or may not be formal. However L must be formal. Among other things, this implies that the propositions of L are formulas built according to certain rules of structure.

I. The present paper contains a formal proof of the following theorem of the elementary system ⊨ [ 1 0 ] c:

This theorem means that if there were a theorem of ⊢0 ( 3 2 ) 0 stating that there is no contradiction in ⊢2 ( 5 4 ) 2, we would have a contradiction in ⊢2 ( 5 4 ) 2. (This is in accordance with the second theorem of Gödel.)

Our proof is based on the calculus of the system ⊨ [ 1 0 ] c and of the metasystem ⊢0 ( 3 2 ) 0.

Note that we could take

instead of Ax E .1 ( L ) (.1 ( L ) .0 ( L ) L) Z. We would then have to do with the simple systems and metasystems of Hetper, which do not contain propositional variables or the logico-semantical axiom. Our method applies equally to the systems and metasystems of New Foundation and to the simple systems and metasystems of Hetper.

Our proof can be considerably simplified by using a recent result of Hetper concerning ancestral functions. Hetper introduces the following abbreviations:

If A ( Z1c), B ( x1cy1cZ1c) are propositions, the expression will be called an ancestral function (we prove without difficulty that this expression is a proposition). The expressions will be called respectively the principal term and the term of derivation of this function.

The question of the independence of the axioms of the theory of sets has been dealt with in a number of works, although not in a final manner. The writer will be concerned solely with the axiomatic system of Zermelo and Fraenkel, and only with that feature of the system whereby all the objects of the underlying domain are sets (so that there is no difference between objects in general and sets in particular).

A special place among the axioms is occupied by a purely relational one, an axiom of definiteness, which establishes the character of equality within the system.

Zermelo introduces equality intensionally—if two symbols x and y represent the same object, we write = (x, y). According to this there is no necessity for axioms to assure the interchangeability of equal objects as arguments of the primitive relation ϵ( , ). For under the intensional interpretation it is clear that:

Similarly it is clear that there is no necessity for a separate axiom that will assure to equality the properties of an equivalence relation. Therefore Zermelo introduces only the following axiom of extensionality:

(if one set is a subset of another set, and the second set is also a subset of the first, then the two sets are equal).

Lewis has made an attempt to construct a logistic system containing an implication-relation ⊰ in such a way that p⊰q shall have the meaning: q is deducible from p. Lewis and Langford admit that “the one serious doubt which can arise concerning the equivalence of p⊰q to the relation of deducibility … arises from the fact that strict implication has its corresponding paradoxes:

19.74˜⋄ p ⊰ · p ⊰ q,

‘If p is impossible, then p strictly implies any proposition q’; and

19.75 ˜⋄˜p ⊰ · q ⊰ p,

‘If p is necessary, then any proposition q strictly implies p.’”

Indeed, it is not obvious that 19.74 and 19.75 should hold. It is true that in many cases 19.75 (as well as 19.74) is valid; for in the system of Lewis and Langford

p · ˜p · ⊰ q

is provable, and the conformity of this law with real deduction is shown by them. In all cases in which a proposition of the form p·∼p can be derived from an impossible proposition, 19.75 holds. But it is not obvious that there are no other kinds of impossible propositions.

Fortunately it is easy to see what is the origin of the paradoxes. They are introduced into the system by the definition

11.02 p ⊰ q · = ˜ ⋄(p · ˜q).

Assume this definition. Then if q is necessary, p·∼q is impossible, and so, in accordance with 11.02, p⊰q is valid.

It is known that the usual definition of a dense series without extreme elements is complete with respect to first-order functions, in the sense that any first-order function on the base of a set of postulates defining such a series either is implied by the postulates or is inconsistent with them. It is here understood, in accordance with the usual convention, that when we speak of a function on the base , the function shall be such as to place restrictions only upon elements belonging to the class determined by f; or, more exactly, every variable with a universal prefix shall occur under the hypothesis that its values satisfy f, while every variable with an existential prefix shall have this condition categorically imposed upon it.

Consider a set of postulates defining a dense series without extreme elements, and add to this set the condition of Dedekind section, to be formulated as follows. Let the conjunction of the three functions,

be written H(ϕ), where the free variables f and g, being parameters throughout, are suppressed. This is the hypothesis of Dedekind's condition, and the conclusion is

which may be written C(ϕ).

In Quine's New foundations the axiom of infinity does not appear to be provable. In a certain stronger system, very closely related to Quine's New foundations, the axiom of infinity is provable. One of the peculiarities of this latter system is that even unstratified propositions can be proved by induction (this is used in the proof of the axiom of infinity). It would seem that definition by induction should also be possible quite irrespective of any conditions of stratification in this latter system. In this paper it is shown that such is the case.

Theorem. If α, α1, α2, …, αs are any classes, and if there is no confusion of bound variables in {Sxp}(v) or {Sxq}(v) and neither z nor v occurs free in p or q, and if

⊦ (y1, y1, … ys):. y1ϵα1 . y2ϵα2 . … . ysϵαs : ⊃ : (Ez) : zϵα : (v) : v . ≡ . {Sxp}(v),

⊦ (y, n, y1, y2, …, ys) :. yϵα . n ϵ Fin . y1ϵα1 . y2ϵα2. … . ysϵαs : ⊃ : (Ex) :zxα : (v) : v=z . ≡ . {Sxq}(v),

then there is an r such thai there is no confusion of bound variables in {Sxr}(v) and neither z nor v occurs free in r, and

⊦ (n, y1, y2, …, ys) :. nϵ Fin . y1ϵα1 . y2ϵα2 . … . ysϵαs : ⊃ : (Ez) : zϵα : (v) : v=z . ≡ . {Sxr}(v),

⊦ (y1, y2, …, ys) : y1ϵα1 . y2ϵα2 . … . ysϵαs . ⊃ . ιx{Snr}(0) = ιxp,

⊦ (n, y1, y2, …, ys) : nϵ Fin . y1ϵα1 . y2ϵα2 . … . ysϵαs . ⊃ . ιx{Snr}(n+1) = ιx{Syq}(ιxr).