Main works:
Lmbert is known also for important contributions to mathematics, and astronomy; also for his work in logic, in particular his (unsuccessful, but historically significant) attempts at construction of a mathematical or symbolic logic. Cf. C. I. Lewis, Survey of Symbolic Logic.  A.C.
Main works:
Paroles d'un croyant, 1834;
squisse d'une philosophic, 184146.  L.E.D.
Main works:
While all three functions are normally distinguishable in any given utterance, typesentences (and, derivatively, words) may be classified according as one or the other of the functions normally predominates in the occurrence of the corresponding tokens. (Thus exclamations are predominantly expressive, commands evocative, scientific generalizations referential.) Such distinctions may, in turn, be made the basis for distinguishing different types of linguistic systems.
While most writers on language agree us to the value of making some such distinctions, there is little agreement as to the number and kinds of functions which may usefully be recognised. There is even less agreement about nomenclature. The account given follows that of Kretschmer (Sprache, 61 ff. in Gercke and Norden, Einleitung in die Altertumszvissenschaft, I) and Bühlcr (Sprachtheorie, passim). Ogden and Richards distinguish five functions (Meaning of Meaning, 357 fF.). The broad distinction between "referential" and "emotive" uses of language, due to the same authors, has been widely accepted.  M.B.
Philosophers have in the past been concerned with two questions covered by our definition, though attempts to organize the subject as an autonomous department of philosophy are of recent date.
Current studies in the philosophy of language can be classified under five hends:
See also Communication, Meaning, Referent, Semiotic, Sign, Symbol, Functions of Language, Scientific Empiricism.  M.B.
Main works: Die Philosophie Herakleitos d. Dunklen, 1858; System d. Eruorbenen Rechte, 1861; and political speeches and pamphlets in Collected Works (Leipzig, 18991901).  R.B.W.
(b) In epistemology and psychology, the term is applied to knowledge, e.g. memory, which lies dormant in the mind but is capable of becoming actual and explicit (see W. Hamilton, Lectures on Metaphysics, xviii, cited by J. M. Baldwin, Dictionary of Philosophy and Psychology, Vol. I, p. 628). Latency in this restricted sense, designates phenomena now embraced by the term subconscious. See Subconscious.  L.W.
(1) The scholastic period begins with the Recognitio summularum of Alonso de la Veracruz (1554) and continues to the dawn of the nineteenth century. According to Ueberweg, the influence of Duns Scotus during this period was greater than that of Thomas Aquinas.
(2) The predominantly naturalistic and positivistic period coincides roughly with the nineteenth century. The wars of independence were accompanied by revolt from scholasticism. In the early part of the century, liberal eclectics like Cousin and P. Janet were popular in South America, but French eighteenth century materialism exerted an increasing influence. Later, the thought of Auguste Comte and of Herbert Spencer came to be dominant especially in Mexico, Brazil, Argentina, and Chile. Even an idealistically inclined social and educational philosopher like Eugenio Maria de Hostos (18391903), although rejecting naturalistic ethics, maintains a positivistic attitude toward metaphysics.
(3) The predominantly idealistic period of the twentieth century was initiated by the work of the Argentine Alejandro Korn (18601936), who introduced modern German philosophy to his fellowcountrymen. Francisco Romero, also an Argentine, has brought about the translation of many European philosophical classics into Spanish. Leibniz, Kant, Hegel, and the more recent neoKantians and phenomcnologists have exerted wide influence in Latin America. North American personalism has also attracted attention. In Mexico, Jose Vasconcelos and Pedro Gringoire reflect in their own syntheses the main streams of idealistic metaphysics, ethics, esthetics. Puerto Rico, with its recent publication of the writings of Hostes, is also a center of philosophic activity. There are signs of growing philosophical independence throughout Latin America.  J.F., E.S.B.
Or the name may be applied to a proposition or sentence of logic corresponding to a certain form of valid inference. E.g., the law of exportation (q. v.) may be called the leading principle of the form of valid inference known as exportation.  A.C.
(b) Generic relationship or partial relationship. See Mo che.  W.T.C.
Leibniz's philosophy was the dawning consciousness of the modern world (Dewey). So gradual and continuous, like the development of a monad, so allinclusive was the growth of his mind, that his philosophy, as he himself says, "connects Plato with Democritus, Aristotle with Descartes, the Scholastics with the moderns, theology and morals with reason." The reform (if all science was to be effected by the use of two instruments, a universal scientific language and a calculus of reasoning. He advocated a universal language of ideographic symbols in which complex concepts would be expressed by combinations of symbols representing simple concepts or by new symbols defined as equivalent to such a complex. He believed that analysis would enable us to limit the number of undefined concepts to a few simple primitives in terms of which all other concepts could be defined. This is the essential notion back of modern logistic treatments.
In contributing some elements of a "universal calculus" he may be said to have been the first serious student of symbolic logic. He devised a symbolism for such concepts and relations as "and", "or", implication between concepts, class inclusion, class and conceptual equivalence, etc. One of his sets of symbolic representations for the four standard propositions of traditional logic coincides with the usage of modern logic He anticipated in the principles of his calculus many of the important rules of modern symbolic systems. His treatment, since it was primarily intensional, neglected important extensional features of recent developments, but, on the other hand, called attention to certain intensional distinctions now commonly neglected.
Leibniz is best known in the history of philosophy as the author of the Monadology and the theory of the Preestablished Harmony both of which see.
Main works:
In mathematics, a theorem proved for the sake of its use in proving another theorem. The name is applied especially in cases where the lemma ceases to be of interest in itself after proof of the theorem for the sake of which it was introduced.  A.C.
In his economic and political writings, Lenin extended and developed the doctrines of Marx and Engels especially in their application to a phase of capitalism which emerged fully only after their death  imperialism. In the same fashion Lenin built upon and further extended the Marxist doctrine of the state in his "State and Revolution", written just before the revolution of 1917. In this work Lenin develops a concept like the dictatorship of the proletariat which Marx treated only briefly and generally, elaborates a distinction like that between socialism and communism, only implicit in Marx's work, and asserts a thesis like the possibility of socialism in one country, towards which Marx was negative in the light of conditions as he knew them. After the Bolsheviks came to power, Lenin headed the government until his death on January 21, 1924. In Russian, Lenin's "Collected Works" comprise thirty volumes, with about thirty additional volumes of miscellaneous writings ("Leninskie Sborniki"). The principal English translations are the "Collected Works", to comprise thirty volumes (of which five in eight books have been published to date), the "Selected Works" comprising twelve volumes (for philosophical materials, see especially Volume XI, "Theoretical Principles of Marxism"), and the Little Lenin Library, made up mostly of shorter works, comprising 27 volumes to date.  J.M.S.
In Epistemology (See his Mind and the WorldOrder) Lewis has presented a "conceptualistic pragmatism" based on these theses:
(b) Benefit, "that which, when obtained, gives pleasure," or the largest amount of happiness for the greatest number of people, as a result of Universal Love (chien ai). Righteousness, loyalty, filial piety, and accomplishment are forms of li. (Mohism and NeoMohism.)  W.T.C.
Of specification; is the same as liberty of contrariety: a potentiality for either one of two contraries, as to do good or to do evil.  H.G.
Main works: Briefe aus England, 17768; editor of Göttingisches Mag. d. Literatur u. Wissensch., 17802; Ausführlkhe Erklärung d. Hogarthschen Kupferstiche, 17949.
The limit of an infinite sequence of real numbers a_{1}, a_{2}, a_{3}, . . . is said to be (the real number) b if for every positive real number ε there is a positive integer N such that the difference between b and a_{n} is less than ε whenever n is greater than N. (By the difference between b and a_{n} is here meant the nonnegative difference, i.e., b−a_{n} if b is greater than a_{n}, a_{n}−b if b is less than a_{n}, and 0 if b is equal to a_{n}.)
Let f be a monadic function for which the range of the independent variable and the range of the dependent variable both consist of real numbers; let b and c be real numbers; and let g be the monadic function so determined that g(c)=b, and g(x)=f(x) if x is different from c. (The range of the independent variable for g is thus the same as that for f, with the addition of the real number c if not already included.) The limit of f(x) as x approaches c is said to be b if g is continuous at c.  More briefly but less accurately, the limit of f(x) as x approaches c is the value which rrust be assigned to f for the argument c in order to make it continuous at c.
The limit of f(x) as x approaches infinity is said to be b, if the limit of h(x) as x approaches 0 is b, where h is the function so determined that h(x)=f( 1/x).
In connection with the infinite sequence of real numbers a_{1}, a_{2}, a_{3} . . ., a monadic function a may be introduced for which the range of the independent variable consists of the positive integers 1, 2, 3, . . . and a(1)=a_{1}, a(2)=a_{2}, a(3)=a_{3}, . . . . It can then be shown that the limit of the infinite sequence as above defined is the same as the limit of a(x) as x approaches infinity.
(Of course it is not meant to be implied in the preceding that the limit of an infinite sequence or of a function always exists. In particular cases it may happen that there is no limit of an infinite sequence, or no limit of f(x) as x approaches c, etc.)  A.C.
In these circumstances real knowledge is very limited. "Universals" register superficial resemblances, not the real essences of things. Experience directly "intuits" identity and diversity, relations, coexistences and necessary connections in its content, and, aided by memory, "knows" the agreements and disagreements of ideas in these respects. We also feel directly (sensitive knowledge) that our experience comes from without. Moreover, though taste, smell, colour, sound, etc. are internal to ourselves (secondary qualities) extension, shape, rest, motion, unity and plurality (primary qualities) seem to inhere in the external world independently of our perception of it. Finally, we have "demonstrative knowledge" of the existence of God. But of anything other than God, we have no knowledge except such as is derived from and limited by the senses.
Locke also was a political, economic and religious thinker of note. A "latitudinarian" and broad churchman in theology and a liberal in politics, he argued against the divine right of kings and the authority of the Bible and the Church, and maintained that political sovereignty rests upon the consent of the governed, and ecclesiastical authority upon the consent of reason. He was also an ardent defender of freedom of thought and speech. Main works: Two Treatises on Gov't, 1689; Reasonableness in Christianity, 1695; Some Thoughts on Education, 1693; An Essay on Human Understanding, 1690.  B.A.G.F.
Concerning the distinction between form and content see further the articles formal, and syntax, logical.
1. THE PROPOSITIONAL CALCULUS formalizes the use of the sentential connectives and, or, not, if . . . then. Various systems of notation are current, of which we here adopt a particular one for purposes of exposition. We use juxtaposition to denote conjunction ("pq" to mean "p and q"), the sign ∨ to denote inclusive disjunction ("p ∨ q" to mean ("p or q or both"), the sign + to denote exclusive disiunction ("p + q" to mean "p or q but not both"), the sign ∼ to denote negation ("∼p" to mean "not p"), the sign ⊃ to denote the conditional ("p ⊃ q" to mean "if p then q," or "not both p and notq"), the sign ≡ to denote the biconditional ("p ≡ q" to mean "p if and only if q," or "either p and q or notp and notq"), and the sign  to denote alternative denial ("p  q" to mean "not both p and q").  The word or is ambiguous in ordinary English usage between inclusive disjunction and exclusive disjunction, and distinct notations are accordingly provided for the two meanings of the word, The notations "p ⊃ q" and "p ≡ q" are sometimes read as "p implies q" and "p is equivalent to q" respectively. These readings must, however, be used with caution, since the terms implication and equivalence are often used in a sense which involves some relationship between the logical forms of the propositions (or the sentences) which they connect, whereas the validity of p ⊃ q and of p ≡ q requires no such relationship. The connective ⊃ is also said to stand for "material implication," distinguished from formal implication (§ 3 below) and strict implication (q. v.). Similarly the connective ≡ is said to stand for "material equivalence."
It is possible in various ways to define some of the sentential connectives named above in terms of others. In particular, if the sign of alternative denial is taken as primitive, all the other connectives can be defined in terms of this one. Also, if the signs of negation and inclusive disjunction are taken as primitive, all the others can be defined in terms of these; likewise if the signs of negation and conjunction are taken as primitive. Here, however, for reasons of naturalness and symmetry, we prefer to take as primitive the three connectives, denoting negation, conjunction, and inclusive disjunction. The remaining ones are then defined as follows:
A  B → ∼A ∨ ∼B.
A ⊃ B → ∼A ∨ B.
A ≡ B → [B ⊃ A][A ⊃ B].
A + B → [∼B]A ∨ [∼A]B.
The capital roman letters here denote arbitrary formulas of the propositional calculus (in the technical sense defined below) and the arrow is to be read "stands for" or "is an abbreviation for." Suppose that we have given some specific list of propositional symbols, which may be infinite in number, and to which we shall refer as the fundamental propositional symbols. These are not necessarily single letters or characters, but may be expressions taken from any language or system of notation; they may denote particular propositions, or they may contain variables and denote ambiguously any proposition of a certain form or class. Certain restrictions are also necessary upon the way in which the fundamental propositional symbols can contain square brackets [ ]; for the present purpose it will suffice to suppose that they do not contain square brackets at all, although they may contain parentheses or other kinds of brackets. We call formulas of the propositional calculus (relative to the given list of fundamental propositional symbols) all the expressions determined by the four following rules:
In order to complete the setting up of the propositional calculus as a logistic system (q. v.) it is necessary to state primitive formulas and primitive rules of inference. Of the many possible ways of doing this we select the following.
If A, B, C are any formulas, each of the seven following formulas is a primitive formula:
[A ∨ A] ⊃ A.
A ⊃ [B ⊃ AB].
A ⊃ [A ∨ B].
AB ⊃ A.
[A ∨ B] ⊃ [B ∨ A].
AB ⊃ B.
[A ⊃ B] ⊃ [[C ∨ A] ⊃ [C ∨ B]].
(The complete list of primitive formulas is thus infinite, but there are just seven possible forms of primitive formulas as above.) There is one primitive rule of inference, as follows: Given A and A ⊃ B to infer B. This is the inference known as modus ponens (see below, §2).
The theorems of the propositional calculus are the formulas which can be derived from the primitive formulas by a succession of applications of the primitive rule of inference. In other words,
The reader should distinguish between theorems about the propositional calculus  the deduction theorem, the principles of duality (below), etc.  and theorems of the propositional calculus in the sense just defined. It is convenient to use such words as theorem, premiss, conclusion both for propositions (in whatever language expressed) and for formulas representing propositions in some fixed system or calculus.
In the foregoing the list of fundamental propositional symbols has been left unspecified. A case of special importance is the case that the fundamental propositional symbols are an infinite list of variables, p, q, r, . . ., which may be taken as representing ambiguously any proposition whatever  or any proposition of a certain class fixed in advance (the class should be closed under the operations of negation, conjunction, and inclusive disjunction). In this case we speak of the pure propositional calculus, and refer to the other cases as applied propositional calculus (although the application may be to something as abstract in character as the pure propositional calculus itself, as, e.g., in the case of the pure functional calculus of first order (§3), which contains an applied propositional calculus).
In formulating the pure propositional calculus the primitive formulas may (if desired) be reduced to a finite number, e.g., to the seven listed above with A, B, C taken to be the particular variables p, q, r. A second primitive rule of inference, the rule of substitution is then required, allowing the inference from a formula A to the formula obtained from A by substituting a formula B for a particular variable in A (the same formula B must be substituted for all occurrences of that variable in A). The definition of a theorem is then given in the same way as before, allowing for the additional primitive rule, the definition of a valid inference must, however, be modified.
In what follows (to the end of §1) we shall, for convenience of statement, confine attention to the case of the pure propositional calculus. Similar statements hold, with minor modifications, for the general case.
The formulation which we have given provides a means of proving theorems of the propositional calculus, the proof consisting of an explicit finite sequence of formulas, the last of which is the theorem proved, and each of which is either a primitive formula or inferable from preceding formulas by a single application of the rule of inference (or one of the rules of inference, if the alternative formulation of the pure propositional calculus employing the rule of substitution is adopted). The test whether a given finite sequence of formulas is a proof of the last formula of the sequence is effective  we have the means of always determining of a given formula whether it is a primitive formula, and the means of always determining of a given formula whether it is inferable from a given finite list of formulas by a single application of modus ponens (or substitution). Indeed our formulation would not be satisfactory otherwise. For in the contrary case a proof would not necessarily carry conviction, the proposer of a proof could fairly be asked to give a proof that it was a proof  in short the formal analysis of what constitutes a proof (in the sense of a cogent demonstration) would be incomplete.
However, the test whether a given formula is a theorem, by the criterion that it is a theorem if a proof of it exists, is not effective  since failure to find a proof upon search might mean lack of ingenuity rather than nonexistence of a proof. The problem to give an effective test by means of which it can always be determined whether a given formula is a theorem is the decision problem, of the propositional calculus. This problem can be solved either by the process of reduction of a formula to disjunctive normal form, or by the truthtable decision procedure. We state the latter in detail.
The three primitive connectives (and consequently all connectives definable from them) denote truthfunctions  i.e., the truthvalue (truth or falsehood) of each of the propositions &min;p, pq, and p ∨ q is uniquely determined by the truthvalues of p and q. In fact,
&min;p is true if p is false and false if p is true;Thus, given a formula of the (pure) propositional calculus and an assignment of a truthvalue to each of the variables appearing, we can reckon out by a mechanical process the truthvalue to be assigned to the entire formula. If, for all possible assignments of truthvalues to the variables appearing, the calculated truthvalue corresponding to the entire formula is truth, the formula is said to be a tautology.The test whether a formula is a tautology is effective, since in any particular case the total number of different assignments of truthvalues to the variables is finite, and the calculation of the truthvalue corresponding to the entire formula can be carried out separately for each possible assignment of truthvalues to the variables.
pq is true if p and q are both true, false otherwise;
p ∨ q is false if p and q are both false, true otherwise.
Now it is readily verified that all the primitive formulas are tautologies, and that for the rule of modus ponens (and the rule of substitution) the property holds that if the premisses of the inference are tautologies the conclusion must be a tautology. It follows that every theorem of the propositional calculus is a tautology. By a more difficult argument it can be shown also that every tautology is a theorem. Hence the test whether a formula is a tautology provides a solution of the decision problem of the propositional calculus.
As corollaries of this we have proofs of the consistency of the propositional calculus (if A is any formula, A and ∼A cannot both be tautologies and hence cannot both be theorems) and of the completeness of the propositional calculus (it can be shown that if any formula not already a theorem, and hence not a tautology, is added to the list of primitive formulas, the calculus becomes inconsistent on the basis of the two rules, substitution and modus ponens).
As another corollary of this, or otherwise, we obtain also the following theorem about the propositional calculus:
If A ≡ B is a theorem, and D is the result of replacing a particular occurrence of A by B in the formula C, then the inference from C to D is a valid inference.
The dual of a formula C of the propositional calculus is obtained by interchanging conjunction and disjunction throughout the formula, i.e., by replacing AB everywhere by A ∨ B, and A ∨ B by AB. Thus, e.g., the dual of the formula ∼[pq ∨ ∼r] is the formula ∼[[p ∨ q] ∼r]. In forming the dual of a formula which is expressed with the aid of the defined connectives, , ⊃, ≡, +, it is convenient to remember that the effect of interchanging conjunction and (inclusive) disjunction is to replace AB by ∼A∼B, to replace A ⊃ B by ∼A B; and to interchange ≡ and +.
It can be shown that the following principles of duality hold in the propositional calculus (where A* and B* denote the duals of the formulas A and B respectively):
Special names have been given to certain particular theorems and forms of valid inference of the propositional calculus. Besides § 2 following, see:
absorption;
affirmation of the consequent;
assertion;
associative law;
commutative law;
composition;
contradiction, law of;
De Morgan's laws;
denial of the antecedent;
distributive law;
double negation, law of;
excluded middle, law of;
exportation;
Hauber's law;
identity, law of;
importation;
Peirce's law;
proof by cases;
reductio ad absurdum;
reflexivity;
tautology;
transitivity;
transposition.
Names given to particular theorems of the propositional calculus are usually thought of as applying to laws embodied in the theorems rather than to the theorems as formulas; hence, in particular, the same name is applied to theorems differing only by alphabetical changes of the variables appearing; and frequently the name used for a theorem is used also for one or more forms of valid inference associated with the theorem. Similar remarks apply to names given to particular theorems of the functional calculus of first order, etc.
The hypothetical syllogism has two kinds or moods. Modus ponens is the inference from a major premiss A ⊃ B and a minor premiss A to the conclusion B. Modus tollens is the inference from a major premiss A ⊃ B and a minor premiss ∼B to the conclusion ∼A.
The disjunctive syllogism has also two moods. Modus tollendo ponens is any one of the four following forms of inference:
from A ∨ B and ∼B to A;Modus ponendo tollens is either of the following forms of inference:
from A ∨ B and ∼A to B*
from A + B and ∼B to A;
from A + B and ∼A to B.
from A + B and A to ∼B;
from A + B and B to ∼A.
In each case the first premiss named is the major premiss and the second one the minor premiss.
Of the dilemma four kinds are distinguished. The simple constructive dilemma has two major premisses A ⊃ C and B ⊃ C, minor premiss A ∨ B, conclusion C. The simple destructive dilemma has two major premisses A ⊃ B and A ⊃ C, minor premiss ∼B ∨ ∼C, conclusion ∼A. The complex constructive dilemma has two major premisses A ⊃ B and C ⊃ D, minor premiss A ∨ C, conclusion B ∨ D. The complex destructive dilemma has two major premisses A ⊃ B and C ⊃ D, minor premiss ∼B ∨ ∼D, conclusion ∼A ∨ ∼C. (Since the conclusion of a complex dilemma must involve inclusive disjunction, it seems that the traditional account is best rendered by employing inclusive disjunction throughout.)
The inferences from A ⊃ B and C ⊃ A to C &sup B, and from A ⊃ B and C ⊃ ∼B to C ⊃ ∼A are called pure hypothetical syllogisms, and the above simpler forms of the hypothetical syllogism are then distinguished as mixed hypothetical. Some recent writers apply the names, modus ponens and modus tollens respectively, also to these two forms of the pure hypothetical syllogism. Other variations of usage or additional forms arc also found. Some writers include under these heads forms of inference which belong to the functional calculus of first order rather than to the propositional calculus.
3. THE FUNCTIONAL CALCULUS OF FIRST ORDER is the next discipline beyond the propositional calculus, according to the usual treatment. It is the first step towards the hierarchy of types (§ 6) and deals, in addition to unanalyzed propositions, with propositional functions (q. v.) of the lowest order. It employs the sentential connectives of § 1, and in addition the universal quantifier (q. v.), written (X) where X is any individual variable, and the existential quantifier, written (EX) where X is any individual variable. (The E denoting existential quantification is more often written inverted, as by Peano and WhiteheadRussell, but we here adopt the typographically more convenient usage, which also has sanction.)
For the interpretation of the calculus we must presuppose a certain domain of individuals. This may be any welldefined nonempty domain, within very wide limits. Different posslhle choices of the domain of individuals lead to different interpretations of the calculus.
In order to set the calculus up formally as a logistic system, we suppose that we have given four lists of symbols, as follows:
When (2) and (3) are complete  i.e., contain all the variables indicated above (an infinite number of propositional variables and for each positive integer n an infinite number of functional variables with subscript n)  and (4) is empty, we shall speak of the pure functional calculus of first order. When (2) and (3) are empty and (4) is not empty, we shall speak of a simple applied functional calculus of first order.
Functional variables and functional constants are together called functional symbols (the adjective functional being here understood to refer to propositional functions). Functional symbols are called nadic if they are either functional variables with subscript n or functional constants denoting nadic propositional functions of individuals. The formulas of the functional calculus of first order (relative to the given lists of symbols (1), (2), (3), (4)) are all the expressions determined by the eight following rules:
[A] ⊃_{x} [B] → (X)[[A] ⊃ [B]].
[A] ≡_{x} [B] → (X)[[A] ≡ [B]].
[A] ∧_{x} [B] → (EX)[[A][B]].
(Here A and B are any formulas, and X is any individual variable. Brackets may be omitted when superfluous.) If F and G denote monadic propositional functions, we say that F(X) ⊃_{x} G(X) expresses formal implication of the function G by the function F, and F(X) ≡_{x} G(X) expresses formal equivalence of the two functions (the adjective formal is perhaps not well chosen here but has become established in use).
A subformula of a given formula is a consecutive constituent part of the given formula which is itself a formula. An occurrence of an individual variable X in a formula is a bound occurrence of X if it is an occurrence in a subformula of either of the forms (X) [A] or (EX)[A]. Any other occurrence of a variable in a formula is a free occurrence. We may thus speak of the bound variables and the free variables of a formula. (Whitehead and Russell, following Peano, use the terms apparent variables and real variables, respectively, instead of bound variables and free variables.)
If A, B, C are any formulas, each of the seven following formulas is a primitive formula:
[A ∨ A] ⊃ A.If X is any individual variable, and A is any formula not containing a free occurrence of X, and B is any formula, each of the two following formulas is a primitive formula;
A ⊃ [B ⊃ AB].
A ⊃ [A ∨ B].
AB ⊃ A.
[A ∨ B] ⊃ [B ∨ A].
AB ⊃ B.
[A ⊃ B] ⊃ [[C ∨ A] ⊃ [C ∨ B]].
[A ⊃_{x} B] ⊃ [A⊃ (X)B].If X and Y are any individual variables (the same or different), and A is any formula such that no free occurrence of X in A is in a subformula of the form (Y) [C], and B is the formula resulting from the substitution of Y for all the free occurrences of X in A, each of the two following formulas is a primitive formula:
[B ⊃_{x} A] ⊃ [(EX)B ⊃ A].
(X)A ⊃ B.
B ⊃ (EX)A.
There are two primitive rules of inference:
The theorems of the functional calculus of first order are the formulas which can he derived from the primitive formulas by a succession of applications of the primitive rules of inference. An inference from premisses A_{1}, A_{2}, . . . , A_{n} to a conclusion B is a valid inference of the functional calculus of first order if B becomes a theorem upon adding A_{1}, A_{2}, . . . , A_{n} to the list of primitive formulas and at the same time restricting the rule of generalization by requiring that the variable generalized upon shall not be any one of the free individual variables of A_{1}, A_{2}, . . . . , A_{n}. It can be proved that the inference from A_{1}, A_{2}, . . . , A_{n} to B is a valid inference of the functional calculus of first order if (obviously), and only if (the deduction threorem), [A_{2} ⊃ [A_{2}⊃ . . . [A_{n} ⊃ B] . . . ]] is a theorem of the functional calculus of first order.
It can be proved that if A ≡ B is a theorem, and D is the result of replacing a particular occurrence of A by B in the formula C, then the inference from C to D is a valid inference.
The consistency of the functional calculus of first order can also be proved without great difficulty.
The dual of a formula is obtained by interchanging conjunction and (inclusive) disjunction throughout and at the same time interchanging universal quantification and existential quantification throughout. (In doing this the different symbols, e.g., functional constants, although they may consist of several characters in succession rather than a single character, shall be treated as units, and no change shall be made inside a symbol. A similar remark, applies at all places where we speak of occurrences of a particular symbol or sequence of symbols in a formula, and the like.) It can be shown that the following principles of duality hold (where A* and B* denote the duals of. the formulas A and B respectively):
A formula is said to be in prenex normal form if all the quantifiers which it contains stand together at the beginning, unseparated by negations (or other sentential connectives), and the scope of each quantifier (i.e., the extent of the bracket [ ] following the quantifier) is to the end of the entire formula. In the case of a formula in prenex normal form, the succession of quantifiers at the beginning is called the prefix; the remaining portion contains no quantifiers and is the matrix of the formula. It can be proved that for every formula A there is a formula B in prenex normal form such that A ≡ B is a theorem; and B is then called a prenex normal form of A.
A formula of the pure functional calculus of first order which contains no free individual variables is said to be satisfiable if it is possible to determine the underlying nonempty domain of individuals and to give meanings to the propositional and functional variables contained  namely to each propositional variable a meaning as a particular proposition and to each nadic functional variable a meaning as an nadic propositional function of individuals (of the domain in question)  in such a way that (under the accepted meanings of the sentential connectives, the quantifiers, and application of function to argument) the formula becomes true. The meaning of the last word, even for abstract, not excluding infinite, domains, must be presupposed  a respect in which this definition differs sharply from most others made in this article.
It is not difficult to find examples of formulas A, containing no free individual variables, such that both A and ∼A are satisfiaMe. A simple example is the formula (x)F(x). More instructive is the following example,
[(x)(y)(z)[[∼F{x,x)][F(x, y)F(y,z) ⊃ F(x,z)]]][(x)(Ey)F(x,y)],which is satisfiable in an infinite domain of individuals but not in any finite domain  the negation is satisfiable in any nonempty domain.
It can be shown that all theorems A of the pure functional calculus of first order which contain no free individual variables have the property that ∼A is not satisfiable. Hence the pure functional calculus of first order is not complete in the strong sense in which the pure propositional calculus is complete. Gödel has shown that the pure functional calculus of first order is complete in the weaker sense that if a formula A contains no free individual variables and ∼A is not satisfiable then A is a theorem.
The decision problem, of the pure functional calculus of first order has two forms
Church has proved that the decision problem of the pure functional calculus of first order is unsolvable. Solutions exist, however, for several important special cases. In particular a decision procedure is known for the case of formulas containing only monadic function variables (this would seem to cover substantially everything considered in traditional formal logic prior to the introduction of the modern logic of relations).
Finally we mention a variant form of the functional calculus of first order, the functional calculus of first order with equality, in which the list of functional constants includes the dyadic functional constant =, denoting equality or identity of individuals. The notation [X] = [Y] is introduced as an abbreviation for [=] (X, Y), and primitive formulas are added as follows to the list already given:
if X is any individual variable, X = X is a primitive formula;We speak of the pure functional calculus of first order with equality when the lists of propositional variables and functional variables are complete and the only functional constant is =; we speak of a simple applied functional calculus of first order with equality when the lists of propositional variables and functional variables are empty.
if X and Y are any individual variables, and B results from the substitution of Y for a particular free occurrence of X in A, which is not in a subformula of A of the form (Y)[C], then [X = Y] ⊃ [A ⊃ B] is a primitive formula.
The addition to the functional calculus of first order of individual constants (denoting particular individuals) is not often made  unless symbols for functions from individuals to individuals (socalled "mathematical" or "descriptive" functions) are to be added at the same time. Such an addition is, however, employed in the two following sections as a means of representing certain forms of inference of traditional logic. The addition is really nonessential, and requires only minor changes in the definition of a formula and the list of primitive formulas (allowing the alternative of individual constants at certain places where the above given formulation calls for free individual variables).
4. OPPOSITION, IMMEDIATE INFERENCE. The four traditional kinds of categorical propositions 
all S is P, customarily designated by the letters A, E, I, O respectively  may conveniently be represented in the functional calculus of first order (§ 3) by the four forms
no S is P,
some S is P,
some S is not P
S(x) ⊃_{x} P(x),S and P being taken as functional constants. (For brevity, we shall use the notations S, P, S(x) ⊃_{x} P(x), etc., alike for certain formulas and for the propositional functions or propositions expressed by these formulas.)
S(x) ⊃_{x} ∼P(x),
S(xr) ∧_{x} P(x),
S(x) ∧_{x} ∼P(x),
This representation does not reproduce faithfully all particulars of the traditional account. The fact is that the traditional doctrine, having grown up from various sources and under an inadequate formal analysis, is not altogether what seems to be the best representation, and simply note the four following points of divergence:
[(Ex)S(x)][S(x) ⊃_{x} P(x)]respectively. The question concerning the choice between these two interpretations is known as the problem of existential import of propositions. We prefer to introduce (Ex)S(x) as a separate premiss at those places where it is required.
and
[(Ex)S(x)][S(x) ⊃_{x} ∼P(x)]
Simple conversion of a proposition, A, E, I, or O, consists in interchanging S and P without other change. Thus the converse of S(x) ⊃_{x} P(x) is P(x) ⊃_{x} S(x), and the converse of S(x) ⊃_{x} ∼P(x) is P(x) ⊃_{x} ∼S(x). In mathematics the term converse is used primarily for the simple converse of a proposition A; loosely also for any one of a number of transformations similar to this (e.g., F(x)G(x) ⊃_{x} H (x) may be said to have the converse F(x)H(x) ⊃_{x} G(x)). Simple conversion of a proposition is a valid inference, in general, only in the case of E and I.
Conversion per accidens of a proposition A. i.e., of S(x) ⊃_{x} P(x), yields P(x) ∧_{x} S(x).
Obversion of a proposition A, E, I, or O consists in replacing P by a functional constant p which denotes the negation of the propositional function (property) denoted by P, and at the same time inserting ∼ if not already present or deleting it if present. Thus the obverse of S(x) ⊃_{x} P(x) is S(x) ⊃_{x} ∼p(x) (the obverse of "all men are mortal" is "no men are immortal"). The obverse of S(x) ⊃_{x} ∼P(x) is S(x) ⊃_{x} p(x); the obverse of S(x) ∧_{x} P(x) is S(x) ∧_{x} ∼p(x); the obverse of S(x) ∧_{x} ∼P(x) is S(x) ∧_{x} p(x).
The name immediate inference is given to certain inferences involving propositions A, E, I, O. These include obversion of A, E, I, or O, simple conversion of E or I, conversion per accidens of A, subalternation of A, E. The three last require the additional premiss (Ex)S(x). Other immediate inferences (for which the terminology is not wholly uniform among different writers) may be obtained by means of sequences of these: e.g., given that all men are mortal we may take the obverse of the converse of the obverse and so infer that all immortals are nonmen (called by some the contrapositive, by others the obverted contrapositive).
The immediate inferences not involving obversion can be represented as valid inferences in the functional calculus of first order, but obversion can be to represented only in an extended calculus embracing functional abstraction (q. v.). For the p used above in describing obversion is, in terms of abstraction,
λx[∼P(x)].
5. CATEGORICAL SYLLOGISM is the name given to certain forms of valid inference (of the functional calculus of first order) which involve as premisses two (formulas representing) categorical propositions, having a term in common  the middle term. Using S, M, P as minor term, middle term, and major term, respectively, we give the traditional classification into figures and moods. In each case we give the major premiss first, the minor premiss immediately after it, and the conclusion last; in some cases we give a third (existential) premiss which is suppressed in the traditional account. Because of the admission of singular propositions under the heads A, E, two different forms of valid inference appear in some cases under the same figure and mood  these singular forms are separately listed.
First Figure 
Second Figure 
Third Figure 
Fourth Figure 
Singular Forms in the First and Second Figures  


6. THEORY OF TYPES. In the functional calculus of first order, variables which appear as arguments of propositional functions or which are bound by quantifiers must be variables which are restricted to a certain limited range, the kinds of propositions about propositional functions which cannot be expressed in the calculus. The uncritical attempt to remove this restriction, by introducing variables of unlimited range (the range covering both nonfunctions and functions of whatever kind) and modifying accordingly the definition of a formula and the lists of primitive formulas and primitive rules of inference, leads to a system which is formally inconsistent through the possibility of deriving in it certain of the logical paradoxes (q. v.). The functional calculus of first order may, however, be extended in another way, which involves separating propositional functions into a certain array of categories (the hierarchy of types), excluding. propositional functions which do not fall into one of these categories, and  besides propositional and individual variables  admitting only variables having a particular one of these categories as range.
For convenience of statement, we confine attention to the pure functional calculus of first order. The first step in the extension consists in introducing quantifiers such as (F_{1}), (EF_{1}), (F_{2}), (EF_{3}), etc., binding nadic functional variables. Corresponding changes are made in the definition of a formula and in the lists of primitive formulas and primitive rules of inference, allowing for these new kinds of bound variables. The resulting system is the functional calculus of second order. Then the next step consists in introducing new kinds of functional variables; namely for every finite ordered set k, l, m, . . . , p of i nonnegative integers (i = 1, 2, 3, . . .) an infinite list of functional variables F^{klm . . .p}, G^{klm . . .p}, . . . , each of which denotes ambiguously any iadic propositional function for which the first argument may be any (k1)adic propositional function of individuals, the second argument any (l1)adic propositional function of individuals, etc. (if one of the integers k, l, m, . . . , p is 1 the corresponding argument is a proposition  if 0, an individual). Then quantifiers are introduced binding these new kinds of functional variables; and so on. The process of alternately introducing new kinds of functional variables (denoting propositional functions which take as arguments propositional functions of kinds for which variables have already been introduced) and quantifiers binding the new kinds of functional variables, with appropriate extension at each stage of the definition of a formula and the lists of primitive formulas and primitive rules of inference, may be continued to infinity. This leads to what we may call the functional calculus of order omega, embodying the (socalled simple) theory of types.
In the functional calculi of second and higher orders, we may introduce the definitions:
X = Y → (F)[F(X) ⊃ F(Y)],where X and Y are any two variables of the same type and F is a monadic functional variable of appropriate type. The notation X = Y may then be interpreted as denoting equality or identity.
The functional calculus of order omega (as just described) can be proved to be consistent by a straightforward generalization of the method employed by Hilbert and Ackermann to prove the consistency of the functional calculus of first order.
For many purposes, however, it is necessary to add to the functional calculus of order omega the axiom of infinity, requiring the domain of individuals to be infinite.  This is most conveniently done by adding a single additional primitive formula, which may be described by referring to § 3 above, taking the formula, which is there given as an example of a formula satisfiable in an infinite domain of individuals but not in any finite domain, and prefixing the quantifier (EF) with scope extending to the end of the formula. This form of the axiom of infinity, however, is considerably stronger (in the absence of the axiom of choice) than the "Infin ax" of Whitehead and Russell.
Other primitive formulas (possibly involving new primitive notations) which may be added correspond to the axiom of choice (q. v.) or are designed to introduce classes (q. v.) or descriptions (q. v.). Functional abstraction (q. v.) may also be Introduced by means of additional primitive formulas or primitive rules of inference, or it may be defined with the aid of descriptions. Whitehead and Russell employ the axiom of infinity and the axiom of choice but avoid the necessity of special primitive formulas in connection with classes and descriptions by introducing classes and descriptions as incomplete symbols.
With the aid of the axiom of infinity and a method of dealing with classes and descriptions, the nonnegative integers may be introduced in any one of various ways (e.g., following Frege and Russell, as finite cardinal numbers), and arithmetic (elementary number theory) derived formally within the system. With the further addition of the axiom of choice, analysis (real number theory) may be likewise derived.
No proof of consistency of the functional calculus of order omega (or even of lower order) wiih the axiom of infinity added is known, except by methods involving assumptions so strong as to destroy any major significance.
According to an important theorem of Gödel, the functional calculus of order omega with the axiom of infinity added, if consistent, is incomplete in the sense that there are formulas A containing no free variables, such that neither A nor ∼A is a theorem. The same thing holds of any logistic system obtained by adding new primitive formulas and primitive rules of inference, provided only that the effective (recursive) character of the formal construction of the system is retained. Thus the system is not only incomplete but, in the indicated sense, incompletable. The same thing holds also of a large variety of logistic systems which could be considered as acceptable substitutes for the functional calculus of order omega with axiom of infinity; in particular the Zermelo set theory (§ 9 below) is in the same sense incomplete and incompletable.
The formalization as a logistic system of the functional calculus of order omega with axiom of infinity leads, by a method which cannot be given here, to a (definite but quite complicated) proposition of arithmetic which is equivalent to  in a certain sense, expresses  the consistency of the system. This proposition of arithmetic can be represented within the system by a formula A containing no free variables, and the following second form of gödel's incompleteness theorem can then be proved: If the system is consistent, then the formula A, although its meaning is a true proposition of arithmetic, is not a theorem of the system. We might, of course, add A to the system as a new primitive formula  we would then have a new system, whose consistency would correspond to a new proposition of arithmetic, represented by a new formula B (containing no free variables), and we would still have in the new system, if consistent, that B was not a theorem.
7. ALGEBRA OF CLASSES deals with classes (q. v.) whose members are from a fixed nonempty class called the universe of discourse, and with the operations of complementation, logical sum, and logical product upon such classes. (The classes are to be thought of as determined by propositional functions having the universe of discourse as the range of the independent variable.) The universal class ∨ comprises the entire universe of discourse. The null (or empty) class ∧ has no members. The complement −a of a class a has as members all those elements of the universe of discourse which are not members of a (and those only). In particular the null class and the universal class are each the complement of the other. The logical sum a ∪ b of two classes a and b has as members all those elements which are members either of a or of b, not excluding elements which are members of both a and b (and those only). The logical product a ∩ b of two classes a and b has as members all those elements which are members of both a and b (and those only)  in other words the logical product of two classes is their common part. The expressions of the algebra of classes are built up out of class variables a, b, c, . . . and the symbols for the universal class and the null class by means of the notations for complementation, logical sum, and logical product (with parentheses). A formula of the algebra of classes consists of two expressions with one of the symbols = or ≠ between. (a = b means that a and b are the same class, a ≠ b that a and b are not the same class.)
While the algebra of classes can be set up as an independent logistic system, we shall here describe it instead by reference to the functional calculus of first order (§ 3), using two monadic functional constants, ∨ and ∧ and an infinite list of monadic functional variables F_{1}, G_{1}, H_{1}, . . . corresponding in order to the class variables a, b, c, . . . respectively. Given any expression A of the algebra of classes, the corresponding formula A‡ of the functional calculus is obtained by replacing complementation, logical sum, and logical product respectively by negation, inclusive disjunction, and conjunction, and at the same time replacing ∨, ∧, a, b, c, . . . respectively by ∨(x), ∧(x), F_{1}(x), G_{1}(x), H_{1}(x), . . . . Given any formula A = B of the algebra of classes the corresponding formula of the functional calculus is A‡ ≡_{x} B‡. Given any formula A ≠ B of the algebra of classes, the corresponding formula of the functional calculus is ∼[A‡ ≡_{x} B‡]. A formula C is a theorem of the algebra of classes if and only if the inference from (x)∨(x) and (x)∼∧(x) to C‡ (where C‡ corresponds to C) is a valid inference of the functional calculus. The inference from premisses D_{1}, D_{2}, . . ., D_{n} to a conclusion C is a valid inference of the algebra of classes if and only if the inference from (x)∨(x), (x)∼∧(x), D_{1}‡, D_{2}‡, . . . , D_{n}‡ to C‡ is a valid inference of the functional calculus.
This isomorphism between the algebra of classes and the indicated part of the functional calculus of first order can be taken as representing a parallelism of meaning. In fact, the meanings become identical if we wish to construe the functional calculus in extension, (see the article propositional function); or, inversely, if we wish to construe the algebra of classes in intension, instead of the usual construction.
If we deal only with formulas of the algebra of classes which are equations (i.e., which have the form A = B), the above description by reference to the functional calculus may be replaced by a simpler description using the applied propositional calculus (§ 1) whose fundamental proposittonal symbols are xε∨, xε∧, xεa, xεb, xεc, . . . . Given an equation, C of the algebra of classes, the corresponding formula C† of the propositional calculus is obtained by replacing equality ( = ) by the biconditional ( ≡ ), replacing complementation, logical sum, and logical product respectively by negation, inclusive disjunction, and conjunction, and at the same time replacing ∨, ∧, a, b, c, . . . respectively by xε∨, xε∧, xεa, xεb, xεc, . . . . An equation C is a theorem of the algbera of classes if and only if the inference from xε∨, ∼xε∧ to C† is a valid inference of the propositional calculus; analogously for valid inferences of the algebra of classes in which the formulas involved are equations.
As a corollary of this, every theorem of the pure propositional calculus (§ 1) of the form A ≡ B has a corresponding theorem of the algebra of classes obtained by replacing the principal occurrence of ≡ by =, elsewhere replacing negation, inclusive disjunction, and conjunction respectively by complementation, logical sum, and logical product, and at the same time replacing propositional variables by class variables. Likewise, every theorem A of the pure propositional calculus has a corresponding theorem B = ∨ of the algebra of classes, where B is obtained from A by replacing negation, inclusive disjunction, and conjunction respectively by complementation, logical sum, and logical product, and replacing propositional variables by class variables.
The dual of a formula or an expression of the algebra of classes is obtained by interchanging logical sum and logical product, and at the same time interchanging ∨ and ∧. The principle of duality holds, that the dual of every theorem is also a theorem.
The relation of class inclusion, ⊂, may be introduced by the definition:
A ⊂ B → A ? −B = A.
Instead of algebra of classes, the term Boolean algebra is used primarily when it is intended that the formal system shall remain uninterpreted or that interpretations other than that described above shall be admitted. For the related idea of a Boolean ring see the paper of Stone cited below.
8. ALGEBRA OF RELATIONS or algebra of relatives deals with relations (q. v.) in extension whose domains and converse domains are each contained in a fixed universe of discourse (which must be a class having at least two members), in a way similar to that in which the algebra of classes deals with classes. Fundamental ideas involved are those of the universal relation and the null relation; the relations of identity and diversity; the contrary and the converse of a relation; the logical sum, the logical product, the relative sum, and the relative product of two relations.
The universal relation ∨ can be described by saying that x∨y holds for every x and y in the universe of discourse. The null relation ∧ is such that x∧y holds for no x and y in the universe of discourse. The relation of identity I is such that xIx holds for every x in the universe of discourse and xIy fails if x is not identical with y. The relation of diversity J is such that xJx fails for every x in the universe of discourse and xJy holds if x is not identical with y.
The contrary −R of a relation R is the relation such that x −R y holds if and only if xRy fails (x and y being in the universe of discourse). In particular, the universal relation and the null relation are each the contrary of the other; and the relations of identity and diversity are each the contrary of the other.
The converse of a relation R is the relation S such that xSy if and only if yRx. The usual notation for the converse of a relation is obtained by placing a breve ? over the letter denoting the relation. A relation is said to be symmetric if it is the same as its converse. In particular, the universal relation, the null relation, and the relations of identity and diversity are symmetric.
The logical sum R ∪ S of two relations R and S is the relation such that x R∪S y holds if and only if at least one of xRy and xSy holds. The logical product R∩S of two relations R and S is the relation such that x R∩S y if and only if both xRy and xSy. The relative product RS of two relations R and S is a relation such that x RS y if and only if there is a z (in the universe of discourse) such that xRz and zSy. The relative sum of two relations R and S is the relation which holds between x and y if and only if for every z (in the universe of discourse) at least one of xRz and zSy holds. The square of a relation R is RR.
The signs = and ≠ are used to form equations and inequations in the same way as in the algebra of classes. An isomorphism between the algebra of relations and an appropriately chosen part of the functional calculus of first order can also be exhibited in the same way as was done in § 7 above for the algebra of classes. A principle of duality also holds, where duality consists in interchanging logical sum and logical product, relative sum and relative product, ∨ and ∧,  and J.
The portion of the algebra of relations which involves, besides relation variables, only the universal relation and the null relation, and the operations of contrary, logical sum, and logical product, and =, ≠, is isomorphic with (formally indistinguishable from) the algebra of classes.
Relative inclusion, ⊂, may be introduced by the definition:
R ⊂ S → R ∩ −S = ∧.When R ⊂ S, we say that R is contained in S, or that S contains R.
A relation is transitive if it contains its square, reflexive if it contains I, irreflexive if it is contained in J, asymmetric if its square is contained in J.
9. ZERMELO SET THEORY. The attempt to devise a system which deals with the logic of classes in a more comprehensive way than is done by the algebra of classes (§ 7), and which, in particular, takes account of the relation e between classes (see the article class), must be carried out with caution in order to avoid the Russell paradox and similar logical paradoxes (q. v.).
There are two methods of devising such a system which (so at least it is widely held or conjectured) do not lead to any inconsistency. One of these involves the theory of types, which was set forth in § 6 above, explicitly for propositional functions, and by implication for classes (classes being divided into types according to the types of the monadic propositional functions which determine them). The other method is the Zermelo set theory, which avoids this preliminary division of classes into types, but imposes restrictions in another direction.
Given the relation (dyadic propositional function) ε, the relations of equality and class inclusion may be introduced by the following definitions:
ZεY → ε(Z, Y).Here X, Y, and Z are to be taken as individual variables ("individual" in the technical sense of § 3), and X is to be determined according to an explicit rule so as to be different from Y and Z.
Z=Y → ZεX ⊃_{x} YεX.
Z⊂Y → XεZ ⊃_{x} XεY.
The Zermelo set theory may be formulated as a simple applied functional calculus of first order (in the sense of § 3), for which the domain of individuals is composed of classes, and the only functional constant is ε, primitive formulas (additional to those given in § 3) being added as follows:
[xεz ≡_{x} xεy] ⊃ z = y.  (Axiom of extensionality) 
(Et)[xεt ≡_{x} [x=y ∨ x=z]].  (Axiom of pairing) 
(Et)[xεt ≡_{x} (Ey)[xεy][yεz]]  (Axiom of summation) 
(Et)[xεt ≡_{x} x ⊂z].  (Axiom of the set of subsets) 
(Et)[xεt ≡_{x} [xεz]A].  (Axiom of subset formation) 
[yεz ⊃_{y} [y'εz ⊃_{y'} [[xεy][xεy'] ⊃_{x} y=y']]] ⊃ (Et)[yεz ⊃_{y} [x''εy ⊃_{x''} (Ex')[[xεy][xεt] ≡_{x} x=x']]].  (Axiom of choice) 
(Et)[zεt][xεt ⊃_{x'} (Ey)[yεt][xεy ≡_{x} x=x']].  (Axiom of infinity) 
[yεz ⊃_{x} (Ex')[A ≡_{x} x=x']] ⊃ (Et)[xεt ≡_{x} (Ey)[yεz]A].  (Axiom of replacement) 
In the axiom of subset formation, A is any formula not containing t as a free varibale (in general, A will contain x as a free variable). In the axiom of replacement, A is any formula which contains neither t nor x' as a free variable (in general, A will contain x and y as free variables). These two axioms are thus represented each by an infinite list of primitive formulas  the remaining axioms each by one primitive formula.
The axiom of extensionality as above stated has (incidentally to its principal purpose) the effect of excluding nonclasses entirely and assuming that everything is a class. This assumption can be avoided if desired, at the cost of complicating the axioms somewhat  one method would be to introduce an additional functional constant, expressing the property to be a class (or set), and to modify the axioms accordingly, the domain of individuals being thought of as possibly containing other things besides sets.
The treatment of sets in the Zermelo set theory differs from that of the theory of types in that all sets are "individuals" and the relation ε (of membership in a set) is significant as between any two sets  in particular, xεx is not forbidden. (We are here using the words set and class as synonymous.)
The restriction which is imposed in order to avoid paradox can be seen in connection with the axiom of subset formation. Instead of this axiom, an uncritical formulation of axioms for set theory might well have included (Et)[xεt ≡_{x} A], asserting the existence of a set t whose members are the sets x satisfying an arbitrary condition A expressible in the notation of the system. This, however, would lead at once to the Russell paradox by taking A to be ∼ xεx and then going through a process of inference which can be described briefly by saying that x is put equal to t. As actually proposed, however, the axiom of subset formation allows the use of the condition A only to obtain a set t whose members are the sets x which are members of a previously given set z and satisfy A. This is not known to lead to paradox.
The notion of an ordered pair can be introduced into the theory by definition, in a way which amounts to identifying the ordered pair (x, y) with the set a which has two and only two members, x' and y', x' being the set which has x as its only member, and y' being the set which has x and y as its only two members. (This is one of various similar possible methods.) Relations in extension may then be treated as sets of ordered pairs.
The Zermelo set theory has an adequacy to the logical development of mathematics comparable to that of the functional calculus of order omega (§ 6). Indeed, as here actually formulated, its adequacy for mathematics apparently exceeds that of the functional calculus; however, this should not be taken as an essential difference, since both systems are incomplete, in accordance with Gödel'a theorem (§ 6), but are capable of extension.
Besides the Zermelo set theory and the functional calculus (theory of types), there is a third method of obtaining a system adequate for mathematics and at the same time  it is hoped  consistent, proposed by Quine in his book cited below (1940).  The last word on these matters has almost certainly not yet been said.
Alonzo Church
Logical Positivism:See Scientific Empiricism.
The determination of the circumstances under which a sequence of formulas is a proof, or a proof as a consequence of a set of formulas, is usually made by means of:
A logistic system need not be given any meaning or interpretation, but may be put forward merely as a formal discipline of interest for its own sake; and in this case the words proof, theorem, valid inference, etc., are to be dissociated from their everyday meanings and taken purely as technical terms. Even when an interpretation of the system is intended, it is a requirement of rigor that no use shall be made of the interpretation (as such) in the determination whether a sequence of symbols is a formula, whether a sequence of formulas is a proof, etc.
The kind of an interpretation, or assignment of meaning, which is normally intended for a logistic system is indicated by the technical terminology employed. This is namely such an interpretation that the formulas, some or all of them, mean or express propositions; the theorems express true propositions; and the proofs and valid inferences represent proofs and valid inferences in the ordinary sense. (Formulas which do not mean propositions may be interpreted as names of things other than propositions, or may be interpreted as containing free variables and having only an ambiguous denotation  see variable.) A logistic system may thus be regarded as a device for obtaining  or, rather stating  an objective, external criterion for the validity of proofs and inferences (which are expressible in a given notation).
A logistic system which has an interpretation of the kind in question may be expected, in general, to have more than one such interpretation.
It is usually to be required that a logistic system shall provide an effective criterion for recognizing formulas, proofs, and proofs as a consequence of a set of formulas; i.e., it shall be a matter of direct observation, and of following a fixed set of directions for concrete operations with symbols, to determine whether a given finite sequence of primitive symbols is a formula, or whether a given finite sequence of formulas is a proof, or is a proof as a conseqence of a given set of formulas. If this requirement is not satisfied, it may be necessary  e.g.  given a particular finite sequence of formulas, to seek by some argument adapted to the special case to prove or disprove that it satisfies the conditions to be a proof (in the technical sense); i.e., the criterion for formal recognition of proofs then presupposes, in actual application, that we already know what a valid deduction is (in a sense which is stronger than that merely of the ability to follow concrete directions in a particular case). See further on this point logic, formal, § 1.
The requirement of effectiveness does not compel the lists of primitive symbols, primitive formulas, and primitive rules of inference to be finite. It is sufficient if there are effective criteria for recognizing formulas, for recognizing primitive formulas, for recognizing applications of primitive rules of inference, and (if separately needed) for recognizing such restricted applications of the primitive rules of inference as are admitted in proofs as a consequence of a given set of formulas.
With the aid of Gödel's device of representing sequences of primitive symbols and sequences of formulas by means of numbers, it is possible to give a more exact definition of the notion of effectiveness by making it correspond to that of recursiveness (q. v.) of numerical functions. E.g., a criterion for recognizing primitive formulas is effective if it determines a general recursive monadic function of natural numbers whose value is 0 when the argument is the number of a primitive formula, 1 for any other natural number as argument. The adequacy of this technical definition to represent the intuitive notion of effectiveness as described above is not immediately clear, but is placed beyond any real doubt by developments for details of which the reader is referred to HilbertBernays and Turing (see references below).
The requirement of effectiveness plays an important role in connection with logistic systems, but the necessity of the requirement depends on the purpose in hand and it may for some purposes be abandoned. Various writers have proposed noneffective, or nonconstructive, logistic systems; in some of these the requirement of finiteness of length of formulas is also abandoned and certain infinite sequences of primitive symbols are admitted as formulas.
For particular examples of logistic systems (all of which satisfy the requirement of effectiveness) see the article logic, formal, especially §§1, 3, 9.
Alonzo Church
There follows the existence of an interpretation of the Zermelo set theory (see Logic, formal, § 9)  consistency of the theory assumed  according to which the domain of sets is only enumerable; although there are theorems of the Zermelo set theory which, under the usual interpretation, assert the existence of the nonenumerable infinite.
A like result may be obtained for the functional calculus of order omega (theory of types) by utilizing a representation of it within the Zermelo set theory. It is thus in a certain sense impossible to postulate the nonenumerable infinite: any set of postulates designed to do so will have an unintended interpretation within the enumerable. Usual sets of mathematical postulates for the real number system (see number) have an appearance to the contrary only because they are incompletely formalized (i.e., the mathematical concepts are formalized, while the underlying logic remains unformalized and indefinite).
The situation described in the preceding paragraph is sometimes called Skolem's paradox, although it is not a paradox in the sense of formal selfcontradiction, but only in the sense of being unexpected or at variance with preconceived ideas.  A.C.
The phrase "natural light of reason" occurs also in the scientific writings of Galileo (q.v.) and Descartes (q.v.)  P.P.W.
b. Identified with art in general because it symbolizes expression of sentiment (Croce).  L.V.