Principia Mathematica

1884:

yet obtainable. Dr Leon Chwistek took the heroic course of dispensing with the axiom without adopting any substitute; from his work it is clear that this course compels us to sacrifice a great deal of ordinary mathematics. There is another course, recommended by Wittgenstein† (†Tractatus Logico-Philosophicus, *5.54ff) for philosophical reasons. This is to assume that functions of propositions are always truth-functions, and that a function can only occur in a proposition through its values. (...) ... the theory of inductive cardinals and ordinals survives; but it seems that the theory of infinite Dedekindian and well-ordered series largely collapses, so that irrationals, and real numbers generally, can no longer be adequately dealt with. Also Cantor's proof that 2n > n breaks down unless n is finite.

2052:". However the position of the matching right or left parenthesis is not indicated explicitly in the notation but has to be deduced from some rules that are complex and at times ambiguous. Moreover, when the dots stand for a logical symbol ∧ its left and right operands have to be deduced using similar rules. First one has to decide based on context whether the dots stand for a left or right parenthesis or a logical symbol. Then one has to decide how far the other corresponding parenthesis is: here one carries on until one meets either a larger number of dots, or the same number of dots next that have equal or greater "force", or the end of the line. Dots next to the signs ⊃, ≡,∨, =Df have greater force than dots next to ( 361: 4328:, *5.54ff) for philosophical reasons. This is to assume that functions of propositions are always truth-functions, and that a function can only occur in a proposition through its values. (...) it appears that everything in Vol. I remains true (though often new proofs are required); the theory of inductive cardinals and ordinals survives; but it seems that the theory of infinite Dedekindian and well-ordered series largely collapses, so that irrationals, and real numbers generally, can no longer be adequately dealt with. Also Cantor's proof that 2 > 499:: The rule that allows the theory to "detach" a "conclusion" from the "premises" that led up to it, and thereafter to discard the "premises" (symbols to the left of the line │, or symbols above the line if horizontal). If this were not the case, then substitution would result in longer and longer strings that have to be carried forward. Indeed, after the application of modus ponens, nothing is left but the conclusion, the rest disappears forever. Contemporary theories often specify as their first axiom the classical or 47: 8093: 5936: 8163: 4515:+1) as different functions on grounds that the computer programs for evaluating them are different). The functions in ZFC given by sets of ordered pairs correspond to what PM call "matrices", and the more general functions in PM are coded by quantifying over some variables. In particular PM distinguishes between functions defined using quantification and functions not defined using quantification, whereas ZFC does not make this distinction. 6177: 59: 4460:, where a cardinal is a special sort of von Neumann ordinal). Each type has its own collection of cardinals associated with it, and there is a considerable amount of bookkeeping necessary for comparing cardinals of different types. PM define addition, multiplication and exponentiation of cardinals, and compare different definitions of finite and infinite cardinals. ✱120.03 is the Axiom of infinity. 4422:) that it represents in this respect a considerable step backwards as compared with Frege. What is missing, above all, is a precise statement of the syntax of the formalism. Syntactical considerations are omitted even in cases where they are necessary for the cogency of the proofs ... The matter is especially doubtful for the rule of substitution and of replacing defined symbols by their 4546:. One strange quirk of PM is that they do not have an ordinal corresponding to 1, which causes numerous unnecessary complications in their theorems. The definition of ordinal exponentiation α in PM is not equivalent to the usual definition in ZFC and has some rather undesirable properties: for example, it is not continuous in β and is not well ordered (so is not even an ordinal). 1751:=0 (so there are no σs) these propositional functions are called predicative functions or matrices. This can be confusing because modern mathematical practice does not distinguish between predicative and non-predicative functions, and in any case PM never defines exactly what a "predicative function" actually is: this is taken as a primitive notion. 231:. The theory of types adopts grammatical restrictions on formulas that rules out the unrestricted comprehension of classes, properties, and functions. The effect of this is that formulas such as would allow the comprehension of objects like the Russell set turn out to be ill-formed: they violate the grammatical restrictions of the system of 1484:(not-AND). In the revised theory, the Introduction presents the notion of "atomic proposition", a "datum" that "belongs to the philosophical part of logic". These have no parts that are propositions and do not contain the notions "all" or "some". For example: "this is red", or "this is earlier than that". Such things can exist 2120:(In practice, these outermost parentheses, which enclose an entire formula, are usually suppressed.) The first of the single dots, standing between two propositional variables, represents conjunction. It belongs to the third group and has the narrowest scope. Here it is replaced by the modern symbol for conjunction "∧", thus 4096:'s "Logicist Foundations of Mathematics", Russell wanted a theory that could plausibly be said to derive all of mathematics from purely logical axioms. However, Principia Mathematica required, in addition to the basic axioms of type theory, three further axioms that seemed to not be true as mere matters of logic, namely the 4108:. Since the first two were existential axioms, Russell phrased mathematical statements depending on them as conditionals. But reducibility was required to be sure that the formal statements even properly express statements of real analysis, so that statements depending on it could not be reformulated as conditionals. 1788:), which causes the hierarchy of ramified types to collapse down to simple type theory. (Strictly speaking, PM allows two propositional functions to be different even if they take the same values on all arguments; this differs from modern mathematical practice where one normally identifies two such functions.) 966:: The notion of "proposition" was significantly modified in the second edition, including the introduction of "atomic" propositions linked by logical signs to form "molecular" propositions, and the use of substitution of molecular propositions into atomic or molecular propositions to create new expressions. 4563:

A 54-page introduction by Russell describing the changes they would have made had they had more time and energy. The main change he suggests is the removal of the controversial axiom of reducibility, though he admits that he knows no satisfactory substitute for it. He also seems more favorable to the

4284:

This new proposal resulted in a dire outcome. An "extensional stance" and restriction to a second-order predicate logic means that a propositional function extended to all individuals such as "All 'x' are blue" now has to list all of the 'x' that satisfy (are true in) the proposition, listing them in

2136:

The two remaining single dots pick out the main connective of the whole formula. They illustrate the utility of the dot notation in picking out those connectives which are relatively more important than the ones which surround them. The one to the left of the "⊃" is replaced by a pair of parentheses,

4506:

In ZFC functions are normally coded as sets of ordered pairs. In PM functions are treated rather differently. First of all, "function" means "propositional function", something taking values true or false. Second, functions are not determined by their values: it is possible to have several different

2099:

The two dots standing together immediately following the assertion-sign indicate that what is asserted is the entire line: since there are two of them, their scope is greater than that of any of the single dots to their right. They are replaced by a left parenthesis standing where the dots are and a

1905:

One author observes that "The notation in that work has been superseded by the subsequent development of logic during the 20th century, to the extent that the beginner has trouble reading PM at all"; while much of the symbolic content can be converted to modern notation, the original notation itself

79:

I can remember Bertrand Russell telling me of a horrible dream. He was in the top floor of the University Library, about A.D. 2100. A library assistant was going round the shelves carrying an enormous bucket, taking down books, glancing at them, restoring them to the shelves or dumping them into the

4502:

The most obvious difference between PM and set theory is that in PM all objects belong to one of a number of disjoint types. This means that everything gets duplicated for each (infinite) type: for example, each type has its own ordinals, cardinals, real numbers, and so on. This results in a lot of

4477:

This covers series, which is PM's term for what is now called a totally ordered set. In particular it covers complete series, continuous functions between series with the order topology (though of course they do not use this terminology), well-ordered series, and series without "gaps" (those with a

4173:

of the axioms. However, this is not the stronger sense of completeness desired for Principia Mathematica, since a given system of axioms (such as those of Principia Mathematica) may have many models, in some of which a given statement is true and in others of which that statement is false, so that

1889:

It might be possible to sacrifice infinite well-ordered series to logical rigour, but the theory of real numbers is an integral part of ordinary mathematics, and can hardly be the subject of reasonable doubt. We are therefore justified (sic) in supposing that some logical axioms which is true will

1883:

One point in regard to which improvement is obviously desirable is the axiom of reducibility ... . This axiom has a purely pragmatic justification ... but it is clearly not the sort of axiom with which we can rest content. On this subject, however, it cannot be said that a satisfactory solution is

4533:

In PM, cardinals are defined as classes of similar classes, whereas in ZFC cardinals are special ordinals. In PM there is a different collection of cardinals for each type with some complicated machinery for moving cardinals between types, whereas in ZFC there is only 1 sort of cardinal. Since PM

563:

has both significant similarities, and similar differences, to a contemporary formal theory. Kleene states that "this deduction of mathematics from logic was offered as intuitive axiomatics. The axioms were intended to be believed, or at least to be accepted as plausible hypotheses concerning the

4525:

PM emphasizes relations as a fundamental concept, whereas in modern mathematical practice it is functions rather than relations that are treated as more fundamental; for example, category theory emphasizes morphisms or functions rather than relations. (However, there is an analogue of categories

4258:

This change is connected with the new axiom that functions can occur in propositions only "through their values", i.e., extensionally (...) quite unobjectionable even from the constructive standpoint (...) provided that quantifiers are always restricted to definite orders". This change from a

4385:

can only be used in practice with very small numbers. To calculate using large numbers (e.g., billions), the formulae would become too long, and some short-cut method would have to be used, which would no doubt rely on everyday techniques such as counting (or else on non-fundamental and hence

4558:

Apart from corrections of misprints, the main text of PM is unchanged between the first and second editions. The main text in Volumes 1 and 2 was reset, so that it occupies fewer pages in each. In the second edition, Volume 3 was not reset, being photographically reprinted with the same page

334:

embeds the notions of "truth" and "falsity" in the notion "primitive proposition". A raw (pure) formalist theory would not provide the meaning of the symbols that form a "primitive proposition"—the symbols themselves could be absolutely arbitrary and unfamiliar. The theory would specify only

4468:

A "relation-number" is an equivalence class of isomorphic relations. PM defines analogues of addition, multiplication, and exponentiation for arbitrary relations. The addition and multiplication is similar to the usual definition of addition and multiplication of ordinals in ZFC, though the

2149:

The dot to the right of the "⊃" is replaced by a left parenthesis which goes where the dot is and a right parenthesis which goes as far to the right as it can without going beyond the scope already established by a group of dots of greater force (in this case the two dots which followed the

190:... But as we advanced, it became increasingly evident that the subject is a very much larger one than we had supposed; moreover on many fundamental questions which had been left obscure and doubtful in the former work, we have now arrived at what we believe to be satisfactory solutions." 1912:

was harshly critical of the notation: "What is missing, above all, is a precise statement of the syntax of the formalism. Syntactical considerations are omitted even in cases where they are necessary for the cogency of the proofs." This is reflected in the example below of the symbols

480:: The theory specifies the rules of syntax (rules of grammar) usually as a recursive definition that starts with "0" and specifies how to build acceptable strings or "well-formed formulas" (wffs). This includes a rule for "substitution" of strings for the symbols called "variables". 2827:

is a man". Given a collection of individuals, one can evaluate the above formula for truth or falsity. For example, given the restricted collection of individuals { Socrates, Plato, Russell, Zeus } the above evaluates to "true" if we allow for Zeus to be a man. But it fails for:

2265:

Logical implication is represented by Peano's "Ɔ" simplified to "⊃", logical negation is symbolised by an elongated tilde, i.e., "~" (contemporary "~" or "¬"), the logical OR by "v". The symbol "=" together with "Df" is used to indicate "is defined as", whereas in sections

4923:

sparked interest in symbolic logic and advanced the subject by popularizing it; it showcased the powers and capacities of symbolic logic; and it showed how advances in philosophy of mathematics and symbolic logic could go hand-in-hand with tremendous fruitfulness.

1795:

set theory one can model the ramified type theory of PM as follows. One picks a set ι to be the type of individuals. For example, ι might be the set of natural numbers, or the set of atoms (in a set theory with atoms) or any other set one is interested in. Then if

1616:). In particular there is a type () of propositions, and there may be a type ι (iota) of "individuals" from which other types are built. Russell and Whitehead's notation for building up types from other types is rather cumbersome, and the notation here is due to 4494:

This section compares the system in PM with the usual mathematical foundations of ZFC. The system of PM is roughly comparable in strength with Zermelo set theory (or more precisely a version of it where the axiom of separation has all quantifiers bounded).

529:

are "stand-ins" for strings; this form of notation is called an "axiom schema" (i.e., there is a countable number of specific forms the notation could take). This can be read in a manner similar to IF-THEN but with a difference: given symbol string IF

4187:

could be both consistent and complete for arithmetic statements. (As mentioned above, Principia itself was already known to be incomplete for some non-arithmetic statements.) According to the theorem, within every sufficiently powerful recursive

5198:' " (p. 452). And Bernstein ended his 1926 review with the comment that "This distinction between the propositional logic as a mathematical system and as a language must be made, if serious errors are to be avoided; this distinction the 2601:(Appendix A). This new section eliminates the first edition's distinction between real and apparent variables, and it eliminates "the primitive idea 'assertion of a propositional function'. To add to the complexity of the treatment, 3316:). These are to be distinguished from the "primitive ideas" that include the assertion sign "⊢", negation "~", logical OR "V", the notions of "elementary proposition" and "elementary propositional function"; these are as close as 1547:

The new introduction keeps the notation for "there exists" (now recast as "sometimes true") and "for all" (recast as "always true"). Appendix A strengthens the notion of "matrix" or "predicative function" (a "primitive idea",

4413:

It is to be regretted that this first comprehensive and thorough-going presentation of a mathematical logic and the derivation of mathematics from it so greatly lacking in formal precision in the foundations (contained in

2035:

s dots are used in a manner similar to parentheses. Each dot (or multiple dot) represents either a left or right parenthesis or the logical symbol ∧. More than one dot indicates the "depth" of the parentheses, for example,

4541:

In PM ordinals are treated as equivalence classes of well-ordered sets, and as with cardinals there is a different collection of ordinals for each type. In ZFC there is only one collection of ordinals, usually defined as

4580:

In 1962, Cambridge University Press published a shortened paperback edition containing parts of the second edition of Volume 1: the new introduction (and the old), the main text up to *56, and Appendices A and C..

1945:

of what this symbol-string means in terms of other symbols; in contemporary treatments the "formation rules" (syntactical rules leading to "well formed formulas") would have prevented the formation of this string.

4369:

It purports to reveal the fundamental basis for arithmetic. However, it is our everyday arithmetical practices such as counting which are fundamental; for if a persistent discrepancy arose between counting and

4349:

In other words, the fact that an infinite list cannot realistically be specified means that the concept of "number" in the infinite sense (i.e. the continuum) cannot be described by the new theory proposed in

351:

symbol set below, the "interpretation" of what the symbols commonly mean, and by implication how they end up being used, is given in parentheses, e.g., "¬ (not)". But this is not a pure Formalist theory.

3817:

can tell the reader how these fictitious objects behave, because "A class is wholly determinate when its membership is known, that is, there cannot be two different classes having the same membership" (

2137:

the right one goes where the dot is and the left one goes as far to the left as it can without crossing a group of dots of greater force, in this case the two dots which follow the assertion-sign, thus

5815: 2150:

assertion-sign). So the right parenthesis which replaces the dot to the right of the "⊃" is placed in front of the right parenthesis which replaced the two dots following the assertion-sign, thus

1876:. (One can vary this slightly by allowing the σs to be quantified in any order, or allowing them to occur before some of the τs, but this makes little difference except to the bookkeeping.) 5402:

Wiener 1914 "A simplification of the logic of relations" (van Heijenoort 1967:224ff) disposed of the second of these when he showed how to reduce the theory of relations to that of classes

3242:(i.e., in its matrix) is (logically) equivalent ("≡") to some "predicative" function of the same variables. The one-variable definition is given below as an illustration of the notation ( 70: 66: 8777: 550:

for further use). But the symbols have no "interpretation" (e.g., no "truth table" or "truth values" or "truth functions") and modus ponens proceeds mechanistically, by grammar alone.

4169:

showed that first-order predicate logic itself was complete in a much weaker sense—that is, any sentence that is unprovable from a given set of axioms must actually be false in some

4486:

This section constructs the ring of integers, the fields of rational and real numbers, and "vector-families", which are related to what are now called torsors over abelian groups.

4559:

numbering; corrections were still made. The total number of pages (excluding the endpapers) in the first edition is 1,996; in the second, 2,000. Volume 1 has five new additions:

84:. He took down one of the volumes, turned over a few pages, seemed puzzled for a moment by the curious symbolism, closed the volume, balanced it in his hand and hesitated.... 6472: 1758:, saying that for every non-predicative function there is a predicative function taking the same values. In practice this axiom essentially means that the elements of type (τ 1754:

Russell and Whitehead found it impossible to develop mathematics while maintaining the difference between predicative and non-predicative functions, so they introduced the

186:

states, this became an unworkable suggestion for practical and philosophical reasons: "The present work was originally intended by us to be comprised in a second volume of

1952:: Chapter I "Preliminary Explanations of Ideas and Notations" begins with the source of the elementary parts of the notation (the symbols =⊃≡−ΛVε and the system of dots): 3453:... Note that the second sign of equality in the above definition is combined with "Df", and thus is not really the same symbol as the sign of equality which is defined". 2250:

and following, braces "{ }" appear. Whether these symbols have specific meanings or are just for visual clarification is unclear. Unfortunately the single dot (but also "

196:, according to its introduction, had three aims: (1) to analyze to the greatest possible extent the ideas and methods of mathematical logic and to minimize the number of 5808: 8627: 7147: 6213: 4153:.) Russell and Whitehead suspected that the system in PM is incomplete: for example, they pointed out that it does not seem powerful enough to show that the cardinal ℵ 1826:, which can also be thought of informally as the set of (propositional predicative) functions from this product to a 2-element set {true,false}. The ramified type (τ 6131: 4112:

tried to argue that Russell's ramification of the theory of types was unnecessary, so that reducibility could be removed, but these arguments seemed inconclusive.

2792:

gives the example: φ is a function that indicates "is a Greek", and ψ indicates "is a man", and χ indicates "is a mortal" these functions then apply to a variable

8822: 4271:

to the second order, i.e. functions of functions: "We can decide that mathematics is to confine itself to functions of functions which obey the above assumption".

593:: "the Contradictory Function" symbolised by "~" and the "Logical Sum or Disjunctive Function" symbolised by "∨" being taken as primitive and logical implication 31: 1906:

is "a subject of scholarly dispute", and some notation "embodies substantive logical doctrines so that it cannot simply be replaced by contemporary symbolism".

73:, accompanied by the comment, "The above proposition is occasionally useful." They go on to say "It is used at least three times, in ✱113.66 and ✱120.123.472.") 977:: This and the next two sections were modified or abandoned in the second edition. In particular, the distinction between the concepts defined in sections 15. 4499:

The system of propositional logic and predicate calculus in PM is essentially the same as that used now, except that the notation and terminology has changed.

3621:

introduce many of the symbols still in contemporary usage. These include the symbols "ε", "⊂", "∩", "∪", "–", "Λ", and "V": "ε" signifies "is an element of" (

7230: 6371: 6163: 5801: 3220:" indicates "individuals" (e.g., a row in a truth table); this distinction is necessary because of the matrix/extensional nature of propositional functions. 2274:). Logical equivalence is represented by "≡" (contemporary "if and only if"); "elementary" propositional functions are written in the customary way, e.g., " 4219: 5846: 914:' will occur if it is desired to put it on record. The process of the inference cannot be reduced to symbols. Its sole record is the occurrence of '⊦ 8817: 4962:, whether for the historical reason of understanding the text or its authors, or for furthering insight into the formalizations of math and logic. 1499:

The new introduction defines "elementary propositions" as atomic and molecular positions together. It then replaces all the primitive propositions

6113: 5991: 5002: 1972:

PM changed Peano's Ɔ to ⊃, and also adopted a few of Peano's later symbols, such as ℩ and ι, and Peano's practice of turning letters upside down.

7544: 4456:

This covers the definition and basic properties of cardinals. A cardinal is defined to be an equivalence class of similar classes (as opposed to

4549:

The constructions of the integers, rationals and real numbers in ZFC have been streamlined considerably over time since the constructions in PM.

6023: 4409:

offered a "critical but sympathetic discussion of the logicistic order of ideas" in his 1944 article "Russell's Mathematical Logic". He wrote:

7702: 5883: 5739: 5702: 5569: 4905: 4897: 4889: 3725:

asserts that no new primitive ideas are necessary to define what is meant by "a class", and only two new "primitive propositions" called the

6490: 4937: 4177: 8316: 8129: 7557: 6880: 5999: 5393:

The "⊂" sign has a dot inside it, and the intersection sign "∩" has a dot above it; these are not available in the "Arial Unicode MS" font.

6305: 4840:——————————; ———————— (1997) . 2270:

and following, "=" is defined as (mathematically) "identical with", i.e., contemporary mathematical "equality" (cf. discussion in section

4793:——————————; ———————— (1927). 4746:——————————; ———————— (1927). 4701:——————————; ———————— (1925). 4666:——————————; ———————— (1913). 4631:——————————; ———————— (1912). 5755: 770:

usage is not specified and appears sporadically; parentheses do play an important role in symbol strings, however, e.g., the notation "(

8644: 7142: 3212:" represents any value of a first-order function. If a circumflex "^" is placed over a variable, then this is an "individual" value of 8812: 7562: 7552: 7289: 6495: 6284: 6181: 4814: 4767: 4720: 7040: 6486: 4166: 3641:) signifies negation of a class (set); "Λ" signifies the null class; and "V" signifies the universal class or universe of discourse. 7698: 6247: 6158: 5667: 5633: 5541: 5515: 5444: 4857: 1900: 1492:

then "advance to molecular propositions" that are all linked by "the stroke". Definitions give equivalences for "~", "∨", "⊃", and "

2413:: Various authors use alternate symbols, so no definitive translation can be given. However, because of criticisms such as that of 4440:

This section describes the propositional and predicate calculus, and gives the basic properties of classes, relations, and types.

2239:

where the double dot represents the logical symbol ∧ and can be viewed as having the higher priority as a non-logical single dot.

7795: 7539: 6364: 6095: 5587: 2417:

below, the best contemporary treatments will be very precise with respect to the "formation rules" (the syntax) of the formulas.

65:: "From this proposition it will follow, when arithmetical addition has been defined, that 1 + 1 = 2." – Volume I, 1st edition, 8622: 7100: 6793: 6534: 4948: 4457: 8792: 8787: 8782: 8216: 6199: 6107: 6101: 6039: 5619: 4995: 2873:

can create formulas to express the following: "If all Greeks are men and if all men are mortals then all Greeks are mortals". (

312:

has no "precise statement of the syntax of the formalism". Furthermore in the theory, it is almost immediately observable that

5891: 1890:

justify it. The axiom required may be more restricted than the axiom of reducibility, but if so, it remains to be discovered.

8056: 7758: 7521: 7516: 7341: 6762: 6446: 6330: 6125: 6089: 4312: 4226:

extending basic arithmetic can be used to prove its own consistency. Thus, the statement "there are no contradictions in the

281:

were not included, but by the end of the third volume it was clear to experts that a large amount of known mathematics could

4378:(e.g., that Principia did not characterise numbers or addition correctly), not as evidence of an error in everyday counting. 3346:. (and vice versa, hence logical equivalence)". In other words: given a matrix determined by property φ applied to variable 4016:. Consequently there is no longer any reason to distinguish between functions classes, for we have, in virtue of the above, 3644:

Small Greek letters (other than "ε", "ι", "π", "φ", "ψ", "χ", and "θ") represent classes (e.g., "α", "β", "γ", "δ", etc.) (

69:(p. 362 in 2nd edition; p. 360 in abridged version). (The proof is actually completed in Volume II, 1st edition, 8396: 8275: 8051: 7834: 7751: 7464: 7395: 7272: 6514: 6206: 5951: 5466: 1627:

of PM all objects are elements of various disjoint ramified types. Ramified types are implicitly built up as follows. If τ

178: 46: 38: 8639: 7122: 5854: 4534:

does not have any equivalent of the axiom of replacement, it is unable to prove the existence of cardinals greater than ℵ

2991:

that satisfies function φ' is defined by the symbols representing the assertion 'It's not true that, given all values of

7976: 7802: 7488: 6721: 6047: 6031: 5555: 4109: 94: 8632: 7127: 572:

sense, and the "assertion of truth" almost immediately as the fifth and sixth elements in the structure of the theory (

8270: 8233: 7459: 7198: 6456: 6357: 3026:

to the logical operator. Contemporary notation would have simply used parentheses outside of the equality ("=") sign:

1576:

In simple type theory objects are elements of various disjoint "types". Types are implicitly built up as follows. If τ

7854: 7849: 5916: 4150: 212:

using the most convenient notation that precise expression allows; (3) to solve the paradoxes that plagued logic and

4522:, though this is of little practical importance as this axiom is used very little in mathematics outside set theory. 2262:", etc.) is also used to symbolise "logical product" (contemporary logical AND often symbolised by "&" or "∧"). 1445:

Together with the "Introduction to the Second Edition", the second edition's Appendix A abandons the entire section

7783: 7373: 6767: 6735: 6426: 6337: 6323: 5975: 5625: 5561: 5533: 4597: 4527: 141: 119: 6500: 360: 8321: 8206: 8194: 8189: 8073: 8022: 7919: 7417: 7378: 6855: 6148: 3677:) is practically almost indispensable, since otherwise the notation rapidly becomes intolerably cumbrous. Thus ' 678:

equivalence, not arithmetic equivalence: "≡" given as a demonstration of how the symbols are used, i.e., "Thus '

7914: 6529: 2018:(Observe that, as in the original, the left dot is square and of greater size than the full stop on the right.) 105:

He said once, after some contact with the Chinese language, that he was horrified to find that the language of

8807: 8802: 8797: 8122: 7844: 7383: 7235: 7218: 6941: 6421: 6298: 6007: 5659: 324:

for the behaviour of the symbols "⊢" (assertion of truth), "~" (logical not), and "V" (logical inclusive OR).

241:

sparked interest in symbolic logic and advanced the subject, popularizing it and demonstrating its power. The

8741: 8659: 8534: 8486: 8300: 8223: 7746: 7723: 7684: 7570: 7511: 7157: 7077: 6921: 6865: 6478: 5611: 5507: 305: 114: 5681: 4157:

exists. However, one can ask if some recursively axiomatizable extension of it is complete and consistent.

80:

bucket. At last he came to three large volumes which Russell could recognize as the last surviving copy of

8693: 8574: 8386: 8199: 8036: 7763: 7741: 7708: 7601: 7447: 7432: 7405: 7356: 7240: 7175: 7000: 6966: 6961: 6835: 6666: 6643: 6222: 5869: 5190:

Grattan-Guinness 2000:454ff discusses the American logicians' critical reception of the second edition of

4131: 2633: 145: 8523: 8443: 8423: 8401: 7966: 7819: 7329: 7065: 6971: 6830: 6815: 6696: 6671: 5525: 5102: 4105: 3726: 3228: 1755: 1488:, i.e., even an "infinite enumeration" of them to replace "generality" (i.e., the notion of "for all"). 1135:

edition (see discussion relative to the second edition, below) begins with a definition of the sign "⊃"

8092: 152:

and published in 1910, 1912, and 1913. In 1925–1927, it appeared in a second edition with an important

4564:

idea that a function should be determined by its values (as is usual in modern mathematical practice).

2737:", i.e., "(Ǝx)", i.e., the contemporary "∃x". The typical notation would be similar to the following: 8683: 8673: 8507: 8438: 8391: 8331: 8211: 7939: 7901: 7778: 7582: 7422: 7346: 7324: 7152: 7110: 7009: 6976: 6840: 6628: 6539: 5983: 5921: 4985: 4576:

An 8-page list of definitions at the end, giving a much-needed index to the 500 or so notations used.

4519: 4135: 217: 5248: 292:

had been planned, but the authors admitted to intellectual exhaustion upon completion of the third.

8678: 8589: 8502: 8497: 8492: 8306: 8248: 8179: 8115: 8068: 7959: 7944: 7924: 7881: 7768: 7718: 7644: 7589: 7526: 7319: 7314: 7262: 7030: 7019: 6691: 6591: 6519: 6510: 6506: 6441: 6436: 6257: 6083: 6065: 6015: 5935: 5864: 5767: 5723: 5651: 5579: 5458: 5073: 5054: 4916: 4543: 4448:

This part covers various properties of relations, especially those needed for cardinal arithmetic.

4307: 4142: 348: 5687: 5615: 564:

world". Indeed, unlike a Formalist theory that manipulates symbols according to rules of grammar,

383:

from these beginning symbols. A starting set might be the following set derived from Kleene 1952:

285:

be developed in the adopted formalism. It was also clear how lengthy such a development would be.

8601: 8596: 8381: 8336: 8243: 8097: 7866: 7829: 7814: 7807: 7790: 7576: 7442: 7368: 7351: 7304: 7117: 7026: 6860: 6845: 6805: 6757: 6742: 6730: 6686: 6661: 6431: 6380: 6291: 3338:, their evaluations in function φ (i.e., resulting their matrix) is logically equivalent to some 2282:)", but later the function sign appears directly before the variable without parenthesis e.g., "φ 209: 7594: 7050: 5077: 4469:

definition of exponentiation of relations in PM is not equivalent to the usual one used in ZFC.

2575:

An introduction to the notation of "Section B Theory of Apparent Variables" (formulas ✱8–✱14.34)

8458: 8295: 8287: 8258: 8228: 8152: 8032: 7839: 7649: 7639: 7531: 7412: 7247: 7223: 7004: 6988: 6893: 6870: 6747: 6716: 6681: 6576: 6411: 5735: 5698: 5663: 5629: 5599: 5591: 5565: 5537: 5511: 5478: 5470: 5440: 4973:

23rd in their list of the top 100 English-language nonfiction books of the twentieth century.

4901: 4893: 4885: 4853: 4828: 4810: 4781: 4763: 4734: 4716: 4689: 4654: 4619: 4254:

to a new axiom (although he does not state it as such). Gödel 1944:126 describes it this way:

4097: 1960:, and the following explanations are to some extent modeled on those which he prefixes to his 521:

The symbol "│" is usually written as a horizontal line, here "⊃" means "implies". The symbols

249:

23rd in their list of the top 100 English-language nonfiction books of the twentieth century.

58: 4844:. Cambridge Mathematical Library (abridged ed.). Cambridge: Cambridge University Press. 8746: 8736: 8721: 8716: 8584: 8238: 8046: 8041: 7934: 7891: 7713: 7674: 7669: 7654: 7480: 7437: 7334: 7132: 7082: 6656: 6618: 6119: 6077: 5896: 5824: 5499: 5428: 4871: 4845: 4820: 4800: 4773: 4753: 4726: 4706: 4681: 4671: 4646: 4636: 4611: 4601: 4530:

that models relations rather than functions, and is quite similar to the type system of PM.)

4205: 3376:: This is a definition that uses the sign in two different ways, as noted by the quote from 266: 197: 149: 5762: 5643: 4867: 1111:

is true," where the alternatives are to be not mutually exclusive, will be represented by "

8615: 8553: 8371: 8184: 8027: 8017: 7971: 7954: 7909: 7871: 7773: 7693: 7500: 7427: 7400: 7388: 7294: 7208: 7182: 7137: 7105: 6906: 6708: 6651: 6601: 6566: 6524: 6277: 5859: 5639: 5486: 5048: 4990: 4875: 4863: 4824: 4777: 4730: 4685: 4650: 4615: 4268: 4101: 2580: 1980: 270: 224: 3877:"This last is the distinguishing characteristic of classes, and justifies us in treating 1431:

are elementary propositional functions which take elementary propositions as arguments, φ

5332:

The original typography is a square of a heavier weight than the conventional full stop.

4947:

was not widely adopted, possibly because its foundations are often considered a form of

4012:

in a function gives the same truth-value to the truth-function as the substitution of ψ

8751: 8548: 8529: 8433: 8418: 8375: 8311: 8253: 8012: 7991: 7949: 7929: 7824: 7679: 7277: 7267: 7257: 7252: 7186: 7060: 6936: 6825: 6820: 6798: 6399: 5436: 4966: 4794: 4747: 4189: 2651: 2606: 1957: 1481: 1461: 242: 205: 4676: 4641: 4606: 8771: 8756: 8726: 8558: 8472: 8467: 7986: 7664: 7171: 6956: 6946: 6916: 6901: 6571: 5731: 5454: 5290:

For comparison, see the translated portion of Peano 1889 in van Heijenoort 1967:81ff.

4805: 4758: 4711: 4406: 4223: 4124: 4116: 3495:

employs two new symbols, a forward "E" and an inverted iota "℩". Here is an example:

2414: 2025:

An introduction to the notation of "Section A Mathematical Logic" (formulas ✱1–✱5.71)

1909: 1870:

quantifiers (∀ or ∃) indicating which quantifier should be applied to each variable σ

1792: 1617: 793: 471: 301: 278: 4570:

Appendix B, numbered as *89, discussing induction without the axiom of reducibility.

8706: 8701: 8519: 8448: 8406: 8265: 8162: 7886: 7733: 7634: 7626: 7506: 7454: 7363: 7299: 7282: 7213: 7072: 6931: 6633: 6416: 6153: 6071: 5715: 5677: 4238:

contradictions in the system (in which case it can be proven both true and false).

4170: 3610: 3313: 2177:

Example 3, with a double dot indicating a logical symbol (from volume 1, page 10):

500: 317: 274: 960:: the axioms or postulates. This was significantly modified in the second edition. 368:

The following formalist theory is offered as contrast to the logicistic theory of

5772: 5692: 3022:. Both are abbreviations for universality (i.e., for all) that bind the variable 2165:. ⊢ : : (∃x). φx . ⊃ . q : ⊃ : . (∃x). φx . v . r : ⊃ . q v r 8731: 8366: 7996: 7876: 7055: 7045: 6992: 6676: 6596: 6581: 6461: 6406: 5959: 5551: 4212:

is provable, then it is false, and the system is therefore inconsistent; and if

3191: 2637: 2060:) and so on, which have greater force than dots indicating a logical product ∧. 89: 4932:, the view on which all mathematical truths are logical truths. Though flawed, 3907:

and replaces it with the notion: "All functions of functions are extensional" (

8711: 8579: 8482: 8138: 6926: 6781: 6752: 6558: 5380:

See the ten postulates of Huntington, in particular postulates IIa and IIb at

3606: 863:

is true'. The first of these does not necessarily involve the truth either of

262: 213: 5783: 4849: 4145:

itself was known to be consistent, but the same had not been established for

8514: 8477: 8428: 8326: 8078: 7981: 7034: 6951: 6911: 6875: 6811: 6623: 6613: 6586: 4306:∧ . . .. Ironically, this change came about as the result of criticism from 1464:("|") to symbolise "incompatibility" (i.e., if both elementary propositions 5603: 5490: 5482: 5465:. The Library of Living Philosophers. Vol. 5 (1st ed.). Chicago: 4183:

Gödel's first incompleteness theorem showed that no recursive extension of

4134:

which could neither be proven nor disproven in the system (the question of

3715:, the symbols "⊂", "∩", "∪", and "–" acquire a dot: for example: "⊍", "∸". 3330:

This means: "We assert the truth of the following: There exists a function

1964:. His use of dots as brackets is adopted, and so are many of his symbols" ( 4216:

is not provable, then it is true, and the system is therefore incomplete.

4123:

whether a contradiction could be derived from the axioms (the question of

3305:

1962:12, i.e., contemporary "axioms"), adding to the 7 defined in section

8063: 7861: 7309: 7014: 6608: 6191: 5787: 5196:

In order to give an account of logic, we must presuppose and employ logic

4929: 4426:... it is chiefly the rule of substitution which would have to be proved. 2987:

means "The symbols representing the assertion 'There exists at least one

379:: This set is the starting set, and other symbols can appear but only by 289: 4936:

would be influential in several later advances in meta-logic, including

3445:

are to be called identical when every predicative function satisfied by

3165:

applies this symbolism to two variables. Thus the following notations: ⊃

568:

introduces the notion of "truth-values", i.e., truth and falsity in the

7659: 6451: 4316:. As described by Russell in the Introduction to the Second Edition of 3633:) signifies the intersection (logical product) of classes (sets); "∪" ( 2420:

The first formula might be converted into modern symbolism as follows:

1707:) that can be thought of as the classes of propositional functions of τ 3899:

Perhaps the above can be made clearer by the discussion of classes in

8539: 8361: 6349: 4799:. Vol. 3 (2nd ed.). Cambridge: Cambridge University Press. 4752:. Vol. 2 (2nd ed.). Cambridge: Cambridge University Press. 4705:. Vol. 1 (2nd ed.). Cambridge: Cambridge University Press. 4670:. Vol. 3 (1st ed.). Cambridge: Cambridge University Press. 4635:. Vol. 2 (1st ed.). Cambridge: Cambridge University Press. 4507:

functions all taking the same values (for example, one might regard 2

4093: 3321: 3301:

is a "Primitive proposition" ("Propositions assumed without proof") (

1596:) that can be thought of as the class of propositional functions of τ 487: 17: 3697:

The union of a set and its inverse is the universal (completed) set.

5793: 5656:

From Frege to Gödel: A Source book in Mathematical Logic, 1879–1931

4119:, one can ask the following questions about any system such as PM: 3821:

1962:26). This is symbolised by the following equality (similar to

3589:

Introduction to the notation of the theory of classes and relations

2782:✱10, ✱11, ✱12: Properties of a variable extended to all individuals 2733:", and it uses a backwards serifed E to represent "there exists an 1647:

are ramified types then as in simple type theory there is a type (τ

1507:

with a single primitive proposition framed in terms of the stroke:

8411: 8171: 7203: 6549: 6394: 4398:

may nonetheless make some aspects of everyday arithmetic clearer.

3705:

The intersection of a set and its inverse is the null (empty) set.

2021:

Most of the rest of the notation in PM was invented by Whitehead.

359: 201: 57: 45: 4693: 4658: 4623: 4473:

Part V Series. Volume II ✱200 to ✱234 and volume III ✱250 to ✱276

3194:), the notion of logical types, and in particular the notions of 2589:

NB: As a result of criticism and advances, the second edition of

5595: 5474: 5177:

Quote from Kleene 1952:45. See discussion LOGICISM at pp. 43–46.

4832: 4785: 4738: 3457:

The not-equals sign "≠" makes its appearance as a definition at

1956:"The notation adopted in the present work is based upon that of 1460:

The revised theory is made difficult by the introduction of the

490:

that specify the behaviours of the symbols and symbol sequences.

372:. A contemporary formal system would be constructed as follows: 8111: 6353: 6195: 5797: 4958:

is great and ongoing, and mathematicians continue to work with

4567:

Appendix A, numbered as *8, 15 pages, about the Sheffer stroke.

4444:

Part II Prolegomena to cardinal arithmetic. Volume I ✱50 to ✱97

4068:

goes on to state that will continue to hang onto the notation "

3231:: a function of one or two variables (two being sufficient for 5103:"The Modern Library's Top 100 Nonfiction Books of the Century" 30:

For Isaac Newton's book containing basic laws of physics, see

8107: 5078:"Principia Mathematica (Stanford Encyclopedia of Philosophy)" 1174:. Anything implied by a true elementary proposition is true. 3637:) signifies the union (logical sum) of classes (sets); "–" ( 5350:

p. xiii of 1927 appearing in the 1962 paperback edition to

5341:

The first example comes from plato.stanford.edu (loc.cit.).

4884:

The first edition was reprinted in 2009 by Merchant Books,

3960:

This has the reasonable meaning that "IF for all values of

2297:

introduces the definition of "logical product" as follows:

1606:(which in set theory is essentially the set of subsets of τ 4359:

Lectures on the Foundations of Mathematics, Cambridge 1939

4064:

Observe the change to the equality "=" sign on the right.

2605:

introduces the notion of substituting a "matrix", and the

1552:

1962:164) and presents four new Primitive propositions as

3487:

is some function satisfied by one and only one argument."

3358:

is logically equivalent to the matrix. Or: every matrix φ

337:

how the symbols behave based on the grammar of the theory

27:

Book on the foundations of mathematics (1910–13, 1925–27)

4573:

Appendix C, 8 pages, discussing propositional functions.

4503:

bookkeeping to relate the various types with each other.

4344:

2nd edition reprinted 1962:xiv, also cf. new Appendix C)

4324:

There is another course, recommended by Wittgenstein† (†

208:; (2) to precisely express mathematical propositions in 2788:

introduces the notion of "a property" of a "variable".

223:

This third aim motivated the adoption of the theory of

4180:

cast unexpected light on these two related questions.

3658:"The use of single letter in place of symbols such as 3629:) signifies "is contained in", "is a subset of"; "∩" ( 2644:

truth-values of a propositional or predicate function.

2571:), and these two are not logically equivalent either. 2173:((((∃x)(φx)) ⊃ (q)) ⊃ ((((∃x) (φx)) v (r)) ⊃ (q v r))) 470:: The theory will build "strings" of these symbols by 5080:. Metaphysics Research Lab, CSLI, Stanford University 4998:– first computational demonstration of theorems in PM 4954:

Scholarly, historical, and philosophical interest in

2547:

But note that this is not (logically) equivalent to (

2411:

Translation of the formulas into contemporary symbols

4452:

Part III Cardinal arithmetic. Volume II ✱100 to ✱126

2725:)" to represent the contemporary symbolism "for all 2158:

Example 2, with double, triple, and quadruple dots:

936:: These use the "=" sign with "Df" at the right end. 347:

of what the formulas are saying. Thus in the formal

8692: 8655: 8567: 8457: 8345: 8286: 8170: 8145: 8005: 7900: 7732: 7625: 7477: 7170: 7093: 6987: 6891: 6780: 6707: 6642: 6557: 6548: 6470: 6387: 6315: 6269: 6229: 6141: 6058: 5943: 5909: 5882: 5845: 5838: 5658:(3rd printing ed.). Cambridge, Massachusetts: 5047:Whitehead, Alfred North; Russell, Bertrand (1963). 4592:Whitehead, Alfred North; Russell, Bertrand (1910). 4464:

Part IV Relation-arithmetic. Volume II ✱150 to ✱186

4374:, this would be treated as evidence of an error in 2404:

This definition serves merely to abbreviate proofs.

2100:right parenthesis at the end of the formula, thus: 983:

Propositions connecting real and apparent variables

5683:Handbook of Whiteheadian Process Thought, Volume 1 5504:Collected Works, Volume II, Publications 1938–1974 5299:This work can be found at van Heijenoort 1967:1ff. 5053:. Cambridge: Cambridge University Press. pp. 4386:questionable methods such as induction). So again 3737:feels it necessary to create a peculiar notation " 3190:reintroduces the notion of "matrix" (contemporary 2507:The second formula might be converted as follows: 1050:: introduces the notions of "truth" and "falsity". 597:(the following example also used to illustrate 9. 4204:cannot be proved." Such a statement is a sort of 3972:are equivalent, THEN the function ƒ of a given φ 3733:1962:25). But before this notion can be defined, 1879:The introduction to the second edition cautions: 5833:British philosopher, logician, and social critic 5261:– via Stanford Encyclopedia of Philosophy. 5247:Linsky, Bernard (2018). Zalta, Edward N. (ed.). 4478:member strictly between any two given members). 3605:. "Relations" are what is known in contemporary 2583:, and predicate logic with identity (equality). 1978:adopts the assertion sign "⊦" from Frege's 1879 1778:) can be identified with the elements of type (τ 1717:obtained from propositional functions of type (τ 871:, while the second involves the truth of both" ( 8778:Large-scale mathematical formalization projects 6132:Henrietta Stanley, Baroness Stanley of Alderley 5253:. Metaphysics Research Lab, Stanford University 4411: 4390:depends on everyday techniques, not vice versa. 4322: 4256: 4174:the statement is left undecided by the axioms. 3988:"This is obvious, since φ can only occur in ƒ(φ 2847:because Russell is not Greek. And it fails for 1667:) of "predicative" propositional functions of τ 103: 77: 3320:comes to rules of notational formation, i.e., 2715:✱10: The existential and universal "operators" 1925:" and "⊃" that can be formed into the string " 1846:) can be modeled as the product of the type (τ 8123: 6365: 6207: 5809: 5586:(6th reprint ed.). Amsterdam, New York: 5270: 5268: 4436:Part I Mathematical logic. Volume I ✱1 to ✱43 942:: brief discussion of the primitive ideas "~ 8: 5728:Major Works: Selected Philosophical Writings 4928:was in part brought about by an interest in 3719:The notion, and notation, of "a class" (set) 3334:with the property that: given all values of 2654:(NOT-AND), i.e., "incompatibility", meaning: 2579:These sections concern what is now known as 1572:Ramified types and the axiom of reducibility 356:Contemporary construction of a formal theory 176:was conceived as a sequel to Russell's 1903 41:– another book of Russell published in 1903. 5530:The Search for Mathematical Roots 1870–1940 5457:(1944). "Russell's Mathematical Logic". In 5105:. The New York Times Company. 30 April 1999 1687:. However, there are also ramified types (τ 1449:. This includes six primitive propositions 766:Notice the appearance of parentheses. This 300:As noted in the criticism of the theory by 32:Philosophiæ Naturalis Principia Mathematica 8130: 8116: 8108: 7191: 6786: 6554: 6372: 6358: 6350: 6214: 6200: 6192: 5906: 5879: 5842: 5816: 5802: 5794: 5034: 3572:exists," which holds when, and only when φ 1457:together with the Axioms of reducibility. 1004:Various descriptive functions of relations 718:identifies a "meta"-notation with " ... ": 4804: 4757: 4710: 4675: 4640: 4605: 4596:. Vol. 1 (1st ed.). Cambridge: 4482:Part VI Quantity. Volume III ✱300 to ✱375 3992:) by the substitution of values of φ for 3787:is a member of the class determined by (φ 3745:)" that it calls a "fictitious object". ( 3158:attributes the first symbolism to Peano. 1068:is any proposition, the proposition "not- 989:Formal implication and formal equivalence 975:Ambiguous assertion and the real variable 813:may be read 'it is true that' ... thus '⊦ 784:: "The 'Truth-value' of a proposition is 591:The fundamental functions of propositions 364:List of propositions referred to by names 5318:Bertrand Russell (1959). "Chapter VII". 5152: 5140: 4394:Wittgenstein did, however, concede that 3729:for classes and relations respectively ( 6114:Katharine Russell, Viscountess Amberley 5992:Introduction to Mathematical Philosophy 5435:(2nd ed.). San Diego, California: 5250:The Stanford Encyclopedia of Philosophy 5194:. For instance Sheffer "puzzled that ' 5015: 5003:Introduction to Mathematical Philosophy 4200:that essentially reads, "The statement 1095:are any propositions, the proposition " 970:The range of values and total variation 792:if it is false" (this phrase is due to 720:Logical equivalence appears again as a 6024:In Praise of Idleness and Other Essays 5411: 5165: 5136: 5124: 4285:a possibly infinite conjunction: e.g. 4076:)", but this is merely equivalent to φ 3597:directly to the foundational sections 3183:could all appear in a single formula. 2246:, brackets "" appear, and in sections 1185:was abandoned in the second edition.) 343:of "values", a model would specify an 288:A fourth volume on the foundations of 216:at the turn of the 20th century, like 144:written by mathematician–philosophers 8823:Books about philosophy of mathematics 5680:; Desmond, William Jr., eds. (2008). 5278: 5274: 5068: 5066: 5064: 5022: 4220:Gödel's second incompleteness theorem 3711:When applied to relations in section 3223:Now equipped with the matrix notion, 2691:evaluate as true, then and only then 1055:Assertion of a propositional function 7: 6000:Free Thought and Official Propaganda 5433:A Mathematical Introduction to Logic 5308:And see footnote, both at PM 1927:92 5097: 5095: 4080:, and this is a class. (all quotes: 2772:" means "for some value of variable 2753:" means "for all values of variable 1988:"(I)t may be read 'it is true that'" 1480:is false), the contemporary logical 1076:is false," will be represented by "~ 1041:Elementary propositions of functions 985:was abandoned in the second edition. 954:" and "⊦" prefixed to a proposition. 6182:Category: Works by Bertrand Russell 5756:Stanford Encyclopedia of Philosophy 5363:The original typography employs an 5211:This idea is due to Wittgenstein's 4279:2nd edition p. 401, Appendix C 4115:Beyond the status of the axioms as 2699:evaluates as false." After section 1816:) is the power set of the product τ 1543:. This is a primitive proposition." 1523:are elementary propositions, given 1028:1962:90–94, for the first edition: 5463:The Philosophy of Bertrand Russell 5384:1962:205 and discussion at p. 206. 5127:, p. 69 substituting → for ⊃. 3901:Introduction to the Second Edition 3475:is a phrase of the form "the term 3342:evaluated at those same values of 2819:The notation above means "for all 154:Introduction to the Second Edition 25: 3362:can be represented by a function 2703:the Sheffer stroke sees no usage. 2679:is incompatible with proposition 1901:Glossary of Principia Mathematica 1586:are types then there is a type (τ 8161: 8091: 6176: 6175: 6096:Conrad Russell, 5th Earl Russell 5934: 5588:North-Holland Publishing Company 4230:system" cannot be proven in the 979:Definition and the real variable 427:"∙" (arithmetic multiplication), 392:"→" (implies, IF-THEN, and "⊃"), 140:) is a three-volume work on the 50:The title page of the shortened 8818:Works by Alfred North Whitehead 6108:John Russell, Viscount Amberley 6102:Frank Russell, 2nd Earl Russell 6040:A History of Western Philosophy 5584:Introduction to Metamathematics 4996:Information Processing Language 4938:Gödel's incompleteness theorems 4178:Gödel's incompleteness theorems 3885:) as the class determined by ψ 3685:is a member of the class α'". ( 3603:✱21 GENERAL THEORY OF RELATIONS 3374:✱13: The identity operator "=" 2776:, function φ evaluates to true" 2757:, function φ evaluates to true" 1866:) with the set of sequences of 1385:is an elementary proposition, ~ 940:Summary of preceding statements 494:Rule of inference, detachment, 6331:Contemporary Whitehead Studies 6126:John Russell, 1st Earl Russell 6090:John Russell, 4th Earl Russell 5367:with a circumflex rather than 4326:Tractatus Logico-Philosophicus 4313:Tractatus Logico-Philosophicus 3240:where all its values are given 2942:Another example: the formula: 2866:because Zeus is not a mortal. 2683:", i.e., if both propositions 2650:: Is the contemporary logical 1439:is an elementary proposition. 1414:is an elementary proposition. 1389:is an elementary proposition. 634:and logical product defined as 1: 8052:History of mathematical logic 5952:The Principles of Mathematics 5467:Northwestern University Press 4365:on various grounds, such as: 4149:s axioms of set theory. (See 3599:✱20 GENERAL THEORY OF CLASSES 3576:is satisfied by one value of 3437:"This definition states that 3227:can assert its controversial 2800:can now write, and evaluate: 1992:Thus to assert a proposition 1406:are elementary propositions, 308:, the "logicistic" theory of 179:The Principles of Mathematics 39:The Principles of Mathematics 7977:Primitive recursive function 6048:My Philosophical Development 6032:Power: A New Social Analysis 5320:My Philosophical Development 5277:, p. 126 (reprinted in 4842:Principia Mathematica to ✱56 4554:Differences between editions 4196:), there exists a statement 4167:Gödel's completeness theorem 3968:of the functions φ and ψ of 3593:The text leaps from section 3202:functions and propositions. 2869:Equipped with this notation 2346:" is the logical product of 1009:Plural descriptive functions 503:or "the rule of detachment": 320:) are presented in terms of 6164:Professorship of Philosophy 5786:in a more modern notation ( 4949:Zermelo–Fraenkel set theory 4381:The calculating methods in 3984:asserts this is "obvious": 8839: 8628:von Neumann–Bernays–Gödel 7041:Schröder–Bernstein theorem 6768:Monadic predicate calculus 6427:Foundations of mathematics 6338:Whitehead Research Project 6324:Center for Process Studies 5976:The Problems of Philosophy 5892:Russell–Einstein Manifesto 5626:Cambridge University Press 5562:Cambridge University Press 5534:Princeton University Press 4677:2027/miun.aat3201.0001.001 4642:2027/miun.aat3201.0001.001 4607:2027/miun.aat3201.0001.001 4598:Cambridge University Press 4518:PM has no analogue of the 4490:Comparison with set theory 4250:, Russell had removed his 4088:Consistency and criticisms 3354:that, when applied to the 3350:, there exists a function 1898: 907:)' have occurred, then '⊦ 774:)" for the contemporary "∀ 424:"+" (arithmetic addition), 142:foundations of mathematics 109:was an Indo-European one. 36: 29: 8813:Books by Bertrand Russell 8429:One-to-one correspondence 8159: 8087: 8074:Philosophy of mathematics 8023:Automated theorem proving 7194: 7148:Von Neumann–Bernays–Gödel 6789: 6172: 5932: 5831: 5557:A Mathematician's Apology 5532:. Princeton, New Jersey: 5188:Groping towards metalogic 5164:This is the word used by 4806:loc.rbc/General.15133v3.1 4759:loc.rbc/General.15133v2.1 4712:loc.rbc/General.15133v1.1 4246:By the second edition of 3996:in a function, and, if φ 3713:✱23 CALCULUS OF RELATIONS 3580:and by no other value." ( 2995:, there are no values of 2621:: In contemporary usage, 1472:are true, their "stroke" 1282:principle of permutation 830:' means 'it is true that 253:Scope of foundations laid 188:Principles of Mathematics 95:A Mathematician's Apology 6299:Tensor product of graphs 6008:Why I Am Not a Christian 5855:Copleston–Russell debate 5660:Harvard University Press 5215:. See the discussion at 5202:does not make" (p. 454). 4943:The logical notation in 4850:10.1017/CBO9780511623585 4151:Hilbert's second problem 3903:, which disposes of the 3137:Contemporary notation: ∀ 3075:Contemporary notation: ∀ 2659:"Given two propositions 710:1962:7). Notice that to 52:Principia Mathematica to 37:Not to be confused with 7724:Self-verifying theories 7545:Tarski's axiomatization 6496:Tarski's undefinability 6491:incompleteness theorems 5621:Littlewood's Miscellany 5508:Oxford University Press 5123:This set is taken from 4242:Wittgenstein 1919, 1939 4130:whether there exists a 4004:, the substitution of φ 3791:)' is equivalent to ' 3721:: In the first edition 2634:propositional functions 1737:) by quantifying over σ 1562:. Multiplicative axiom 1375:principle of summation 1216:principle of tautology 1034:Elementary propositions 964:Propositional functions 586:Uses of various letters 277:. Deeper theorems from 120:Littlewood's Miscellany 115:John Edensor Littlewood 8793:1913 non-fiction books 8788:1912 non-fiction books 8783:1910 non-fiction books 8387:Constructible universe 8207:Constructibility (V=L) 8098:Mathematics portal 7709:Proof of impossibility 7357:propositional variable 6667:Propositional calculus 6223:Alfred North Whitehead 6149:Appointment court case 6134:(maternal grandmother) 6128:(paternal grandfather) 5917:Peano–Russell notation 5870:Theory of descriptions 5526:Grattan-Guinness, Ivor 5502:; et al. (eds.). 5371:; this continues below 4428: 4347: 4282: 4267:stance also restricts 4132:mathematical statement 3727:axioms of reducibility 3560:This has the meaning: 2154:⊢ ((p ∧ q) ⊃ (p ⊃ q)). 2095:⊢ ((p ∧ q) ⊃ (p ⊃ q)). 1962:Formulario Mathematico 1950:Source of the notation 1892: 1886: 1806:are types, the type (τ 1326:associative principle 1247:principle of addition 1127:Primitive propositions 958:Primitive propositions 484:Transformation rule(s) 365: 146:Alfred North Whitehead 111: 86: 74: 55: 8610:Principia Mathematica 8444:Transfinite induction 8303:(i.e. set difference) 7967:Kolmogorov complexity 7920:Computably enumerable 7820:Model complete theory 7612:Principia Mathematica 6672:Propositional formula 6501:Banach–Tarski paradox 6306:Theory of gravitation 6239:Principia Mathematica 5968:Principia Mathematica 5775:Principia Mathematica 5763:Principia Mathematica 5186:In his section 8.5.4 5050:Principia Mathematica 4796:Principia Mathematica 4749:Principia Mathematica 4703:Principia Mathematica 4668:Principia Mathematica 4633:Principia Mathematica 4594:Principia Mathematica 4252:axiom of reducibility 4222:(1931) shows that no 4106:axiom of reducibility 3905:Axiom of Reducibility 3449:is also satisfied by 3229:axiom of reducibility 2675:' means "proposition 1887: 1881: 1756:axiom of reducibility 999:Classes and relations 363: 131:Principia Mathematica 107:Principia Mathematica 82:Principia Mathematica 61: 49: 8684:Burali-Forti paradox 8439:Set-builder notation 8392:Continuum hypothesis 8332:Symmetric difference 7915:Church–Turing thesis 7902:Computability theory 7111:continuum hypothesis 6629:Square of opposition 6487:Gödel's completeness 5778:– by Bernard Linsky. 5724:Wittgenstein, Ludwig 5652:van Heijenoort, Jean 5580:Kleene, Stephen Cole 5498:Gödel, Kurt (1990). 5469:. pp. 123–153. 5459:Schilpp, Paul Arthur 5429:Enderton, Herbert B. 4986:Axiomatic set theory 4544:von Neumann ordinals 4520:axiom of replacement 4357:Wittgenstein in his 4234:system unless there 2063:Example 1. The line 1625:ramified type theory 1568:. Axiom of infinity 8645:Tarski–Grothendieck 8069:Mathematical object 7960:P versus NP problem 7925:Computable function 7719:Reverse mathematics 7645:Logical consequence 7522:primitive recursive 7517:elementary function 7290:Free/bound variable 7143:Tarski–Grothendieck 6662:Logical connectives 6592:Logical equivalence 6442:Logical consequence 6285:Point-free geometry 6258:Process and Reality 6084:Edith Finch Russell 6066:Alys Pearsall Smith 6016:Marriage and Morals 5847:Views on philosophy 4332:breaks down unless 4308:Ludwig Wittgenstein 4143:Propositional logic 3911:1962:xxxix), i.e., 859:is true; therefore 788:if it is true, and 407:"∃" (there exists); 134:(often abbreviated 8234:Limitation of size 7867:Transfer principle 7830:Semantics of logic 7815:Categorical theory 7791:Non-standard model 7305:Logical connective 6432:Information theory 6381:Mathematical logic 6292:Process philosophy 5784:Proposition ✱54.43 4263:stance to a fully 3980:are equivalent." 3370:, and vice versa. 366: 304:(below), unlike a 75: 56: 8765: 8764: 8674:Russell's paradox 8623:Zermelo–Fraenkel 8524:Dedekind-infinite 8397:Diagonal argument 8296:Cartesian product 8153:Set (mathematics) 8105: 8104: 8037:Abstract category 7840:Theories of truth 7650:Rule of inference 7640:Natural deduction 7621: 7620: 7166: 7165: 6871:Cartesian product 6776: 6775: 6682:Many-valued logic 6657:Boolean functions 6540:Russell's paradox 6515:diagonal argument 6412:First-order logic 6347: 6346: 6189: 6188: 6068:(wife, 1894–1921) 5930: 5929: 5922:Russell's paradox 5905: 5904: 5878: 5877: 5741:978-0-06-155024-9 5704:978-3-938793-92-3 5612:Littlewood, J. E. 5571:978-0-521-42706-7 5500:Feferman, Solomon 5074:Irvine, Andrew D. 4906:978-1-60386-184-7 4898:978-1-60386-183-0 4890:978-1-60386-182-3 4352:PM Second Edition 4098:axiom of infinity 3681:ε α' will mean ' 3479:which satisfies φ 3465:✱14: Descriptions 3205:New symbolism "φ 3149:)) (or a variant) 3087:)) (or a variant) 2632:is (at least for 2242:Later in section 546:(and retain only 436:individual symbol 339:. Then later, by 316:(in the sense of 296:Theoretical basis 218:Russell's paradox 198:primitive notions 16:(Redirected from 8830: 8747:Bertrand Russell 8737:John von Neumann 8722:Abraham Fraenkel 8717:Richard Dedekind 8679:Suslin's problem 8590:Cantor's theorem 8307:De Morgan's laws 8165: 8132: 8125: 8118: 8109: 8096: 8095: 8047:History of logic 8042:Category of sets 7935:Decision problem 7714:Ordinal analysis 7655:Sequent calculus 7553:Boolean algebras 7493: 7492: 7467: 7438:logical/constant 7192: 7178: 7101:Zermelo–Fraenkel 6852:Set operations: 6787: 6724: 6555: 6535:Löwenheim–Skolem 6422:Formal semantics 6374: 6367: 6360: 6351: 6340: 6333: 6326: 6308: 6301: 6294: 6287: 6280: 6262: 6250: 6243: 6216: 6209: 6202: 6193: 6179: 6178: 6159:Peace Foundation 6120:John Stuart Mill 6078:Patricia Russell 5938: 5907: 5897:Russell Tribunal 5884:Views on society 5880: 5865:Russell's teapot 5843: 5825:Bertrand Russell 5818: 5811: 5804: 5795: 5773:The Notation in 5745: 5719: 5713: 5711: 5696: 5673: 5647: 5607: 5575: 5547: 5521: 5494: 5450: 5415: 5409: 5403: 5400: 5394: 5391: 5385: 5378: 5372: 5361: 5355: 5348: 5342: 5339: 5333: 5330: 5324: 5323: 5315: 5309: 5306: 5300: 5297: 5291: 5288: 5282: 5272: 5263: 5262: 5260: 5258: 5244: 5238: 5235: 5229: 5226: 5220: 5209: 5203: 5184: 5178: 5175: 5169: 5162: 5156: 5150: 5144: 5134: 5128: 5121: 5115: 5114: 5112: 5110: 5099: 5090: 5089: 5087: 5085: 5070: 5059: 5058: 5044: 5038: 5032: 5026: 5020: 4917:Andrew D. Irvine 4879: 4836: 4808: 4789: 4761: 4742: 4714: 4697: 4679: 4662: 4644: 4627: 4609: 4345: 4280: 4161:Gödel 1930, 1931 3625:1962:188); "⊂" ( 3237: 3216:, meaning that " 3002:The symbolisms ⊃ 2999:satisfying φ'". 2627: 2593:(1927) replaces 2034: 1539:), we can infer 1103:, i.e., "either 887: 686:' stands for '( 474:(juxtaposition). 430:"'" (successor); 419:function symbols 413:predicate symbol 306:formalist theory 267:cardinal numbers 150:Bertrand Russell 124: 99: 21: 8838: 8837: 8833: 8832: 8831: 8829: 8828: 8827: 8808:1913 in science 8803:1912 in science 8798:1910 in science 8768: 8767: 8766: 8761: 8688: 8667: 8651: 8616:New Foundations 8563: 8453: 8372:Cardinal number 8355: 8341: 8282: 8166: 8157: 8141: 8136: 8106: 8101: 8090: 8083: 8028:Category theory 8018:Algebraic logic 8001: 7972:Lambda calculus 7910:Church encoding 7896: 7872:Truth predicate 7728: 7694:Complete theory 7617: 7486: 7482: 7478: 7473: 7465: 7185: and 7181: 7176: 7162: 7138:New Foundations 7106:axiom of choice 7089: 7051:Gödel numbering 6991: and 6983: 6887: 6772: 6722: 6703: 6652:Boolean algebra 6638: 6602:Equiconsistency 6567:Classical logic 6544: 6525:Halting problem 6513: and 6489: and 6477: and 6476: 6471:Theorems ( 6466: 6383: 6378: 6348: 6343: 6336: 6329: 6322: 6311: 6304: 6297: 6290: 6283: 6278:Inert knowledge 6276: 6265: 6255: 6246: 6236: 6225: 6220: 6190: 6185: 6168: 6137: 6086:(wife, 1952–70) 6080:(wife, 1936–51) 6074:(wife, 1921–35) 6054: 5939: 5926: 5901: 5874: 5860:Logical atomism 5834: 5827: 5822: 5752: 5742: 5722: 5709: 5707: 5705: 5690: 5686:. Heusenstamm: 5676: 5670: 5650: 5636: 5610: 5578: 5572: 5550: 5544: 5524: 5518: 5497: 5453: 5447: 5427: 5424: 5419: 5418: 5410: 5406: 5401: 5397: 5392: 5388: 5379: 5375: 5362: 5358: 5349: 5345: 5340: 5336: 5331: 5327: 5317: 5316: 5312: 5307: 5303: 5298: 5294: 5289: 5285: 5281:, p. 120). 5273: 5266: 5256: 5254: 5246: 5245: 5241: 5236: 5232: 5227: 5223: 5210: 5206: 5185: 5181: 5176: 5172: 5163: 5159: 5151: 5147: 5135: 5131: 5122: 5118: 5108: 5106: 5101: 5100: 5093: 5083: 5081: 5072: 5071: 5062: 5046: 5045: 5041: 5035:Littlewood 1986 5033: 5029: 5021: 5017: 5012: 4991:Boolean algebra 4982: 4976: 4914: 4882: 4860: 4839: 4817: 4792: 4770: 4745: 4723: 4700: 4665: 4630: 4591: 4587: 4556: 4537: 4492: 4484: 4475: 4466: 4454: 4446: 4438: 4433: 4404: 4346: 4340: 4304: 4297: 4290: 4281: 4275: 4269:predicate logic 4244: 4163: 4156: 4102:axiom of choice 4090: 4028: 3924: 3803:) is true.'". ( 3591: 3542: 3309:(starting with 3276: 3246:1962:166–167): 3235: 3182: 3176: 3170: 3104: 3042: 3013: 3007: 2625: 2581:predicate logic 2577: 2526: 2491: 2463: 2435: 2091:corresponds to 2032: 2027: 1981:Begriffsschrift 1903: 1897: 1875: 1865: 1859: 1855: 1849: 1845: 1839: 1835: 1829: 1825: 1819: 1815: 1809: 1805: 1799: 1787: 1781: 1777: 1771: 1767: 1761: 1746: 1740: 1736: 1730: 1726: 1720: 1716: 1710: 1706: 1700: 1696: 1690: 1686: 1680: 1676: 1670: 1666: 1660: 1656: 1650: 1646: 1640: 1636: 1630: 1615: 1609: 1605: 1599: 1595: 1589: 1585: 1579: 1574: 1129: 1122:(cf. section B) 1022: 1020:Primitive ideas 929:The use of dots 885: 765: 725: 719: 635: 633: 602: 557: 520: 478:Formation rules 415:: "=" (equals); 387:logical symbols 358: 314:interpretations 298: 271:ordinal numbers 255: 206:inference rules 126: 113: 101: 88: 42: 35: 28: 23: 22: 15: 12: 11: 5: 8836: 8834: 8826: 8825: 8820: 8815: 8810: 8805: 8800: 8795: 8790: 8785: 8780: 8770: 8769: 8763: 8762: 8760: 8759: 8754: 8752:Thoralf Skolem 8749: 8744: 8739: 8734: 8729: 8724: 8719: 8714: 8709: 8704: 8698: 8696: 8690: 8689: 8687: 8686: 8681: 8676: 8670: 8668: 8666: 8665: 8662: 8656: 8653: 8652: 8650: 8649: 8648: 8647: 8642: 8637: 8636: 8635: 8620: 8619: 8618: 8606: 8605: 8604: 8593: 8592: 8587: 8582: 8577: 8571: 8569: 8565: 8564: 8562: 8561: 8556: 8551: 8546: 8537: 8532: 8527: 8517: 8512: 8511: 8510: 8505: 8500: 8490: 8480: 8475: 8470: 8464: 8462: 8455: 8454: 8452: 8451: 8446: 8441: 8436: 8434:Ordinal number 8431: 8426: 8421: 8416: 8415: 8414: 8409: 8399: 8394: 8389: 8384: 8379: 8369: 8364: 8358: 8356: 8354: 8353: 8350: 8346: 8343: 8342: 8340: 8339: 8334: 8329: 8324: 8319: 8314: 8312:Disjoint union 8309: 8304: 8298: 8292: 8290: 8284: 8283: 8281: 8280: 8279: 8278: 8273: 8262: 8261: 8259:Martin's axiom 8256: 8251: 8246: 8241: 8236: 8231: 8226: 8224:Extensionality 8221: 8220: 8219: 8209: 8204: 8203: 8202: 8197: 8192: 8182: 8176: 8174: 8168: 8167: 8160: 8158: 8156: 8155: 8149: 8147: 8143: 8142: 8137: 8135: 8134: 8127: 8120: 8112: 8103: 8102: 8088: 8085: 8084: 8082: 8081: 8076: 8071: 8066: 8061: 8060: 8059: 8049: 8044: 8039: 8030: 8025: 8020: 8015: 8013:Abstract logic 8009: 8007: 8003: 8002: 8000: 7999: 7994: 7992:Turing machine 7989: 7984: 7979: 7974: 7969: 7964: 7963: 7962: 7957: 7952: 7947: 7942: 7932: 7930:Computable set 7927: 7922: 7917: 7912: 7906: 7904: 7898: 7897: 7895: 7894: 7889: 7884: 7879: 7874: 7869: 7864: 7859: 7858: 7857: 7852: 7847: 7837: 7832: 7827: 7825:Satisfiability 7822: 7817: 7812: 7811: 7810: 7800: 7799: 7798: 7788: 7787: 7786: 7781: 7776: 7771: 7766: 7756: 7755: 7754: 7749: 7742:Interpretation 7738: 7736: 7730: 7729: 7727: 7726: 7721: 7716: 7711: 7706: 7696: 7691: 7690: 7689: 7688: 7687: 7677: 7672: 7662: 7657: 7652: 7647: 7642: 7637: 7631: 7629: 7623: 7622: 7619: 7618: 7616: 7615: 7607: 7606: 7605: 7604: 7599: 7598: 7597: 7592: 7587: 7567: 7566: 7565: 7563:minimal axioms 7560: 7549: 7548: 7547: 7536: 7535: 7534: 7529: 7524: 7519: 7514: 7509: 7496: 7494: 7475: 7474: 7472: 7471: 7470: 7469: 7457: 7452: 7451: 7450: 7445: 7440: 7435: 7425: 7420: 7415: 7410: 7409: 7408: 7403: 7393: 7392: 7391: 7386: 7381: 7376: 7366: 7361: 7360: 7359: 7354: 7349: 7339: 7338: 7337: 7332: 7327: 7322: 7317: 7312: 7302: 7297: 7292: 7287: 7286: 7285: 7280: 7275: 7270: 7260: 7255: 7253:Formation rule 7250: 7245: 7244: 7243: 7238: 7228: 7227: 7226: 7216: 7211: 7206: 7201: 7195: 7189: 7172:Formal systems 7168: 7167: 7164: 7163: 7161: 7160: 7155: 7150: 7145: 7140: 7135: 7130: 7125: 7120: 7115: 7114: 7113: 7108: 7097: 7095: 7091: 7090: 7088: 7087: 7086: 7085: 7075: 7070: 7069: 7068: 7061:Large cardinal 7058: 7053: 7048: 7043: 7038: 7024: 7023: 7022: 7017: 7012: 6997: 6995: 6985: 6984: 6982: 6981: 6980: 6979: 6974: 6969: 6959: 6954: 6949: 6944: 6939: 6934: 6929: 6924: 6919: 6914: 6909: 6904: 6898: 6896: 6889: 6888: 6886: 6885: 6884: 6883: 6878: 6873: 6868: 6863: 6858: 6850: 6849: 6848: 6843: 6833: 6828: 6826:Extensionality 6823: 6821:Ordinal number 6818: 6808: 6803: 6802: 6801: 6790: 6784: 6778: 6777: 6774: 6773: 6771: 6770: 6765: 6760: 6755: 6750: 6745: 6740: 6739: 6738: 6728: 6727: 6726: 6713: 6711: 6705: 6704: 6702: 6701: 6700: 6699: 6694: 6689: 6679: 6674: 6669: 6664: 6659: 6654: 6648: 6646: 6640: 6639: 6637: 6636: 6631: 6626: 6621: 6616: 6611: 6606: 6605: 6604: 6594: 6589: 6584: 6579: 6574: 6569: 6563: 6561: 6552: 6546: 6545: 6543: 6542: 6537: 6532: 6527: 6522: 6517: 6505:Cantor's 6503: 6498: 6493: 6483: 6481: 6468: 6467: 6465: 6464: 6459: 6454: 6449: 6444: 6439: 6434: 6429: 6424: 6419: 6414: 6409: 6404: 6403: 6402: 6391: 6389: 6385: 6384: 6379: 6377: 6376: 6369: 6362: 6354: 6345: 6344: 6342: 6341: 6334: 6327: 6319: 6317: 6313: 6312: 6310: 6309: 6302: 6295: 6288: 6281: 6273: 6271: 6267: 6266: 6264: 6263: 6253: 6252: 6251: 6233: 6231: 6227: 6226: 6221: 6219: 6218: 6211: 6204: 6196: 6187: 6186: 6173: 6170: 6169: 6167: 6166: 6161: 6156: 6151: 6145: 6143: 6139: 6138: 6136: 6135: 6129: 6123: 6117: 6111: 6105: 6099: 6093: 6087: 6081: 6075: 6069: 6062: 6060: 6056: 6055: 6053: 6052: 6044: 6036: 6028: 6020: 6012: 6004: 5996: 5988: 5980: 5972: 5964: 5956: 5947: 5945: 5941: 5940: 5933: 5931: 5928: 5927: 5925: 5924: 5919: 5913: 5911: 5903: 5902: 5900: 5899: 5894: 5888: 5886: 5876: 5875: 5873: 5872: 5867: 5862: 5857: 5851: 5849: 5840: 5836: 5835: 5832: 5829: 5828: 5823: 5821: 5820: 5813: 5806: 5798: 5792: 5791: 5781: 5780: 5779: 5770: 5751: 5750:External links 5748: 5747: 5746: 5740: 5720: 5703: 5674: 5668: 5648: 5634: 5616:Bollobás, Béla 5608: 5576: 5570: 5548: 5542: 5522: 5516: 5495: 5451: 5445: 5437:Academic Press 5423: 5420: 5417: 5416: 5404: 5395: 5386: 5373: 5356: 5343: 5334: 5325: 5310: 5301: 5292: 5283: 5264: 5239: 5230: 5221: 5204: 5179: 5170: 5157: 5145: 5139:, p. 71, 5129: 5116: 5091: 5076:(1 May 2003). 5060: 5039: 5037:, p. 130. 5027: 5014: 5013: 5011: 5008: 5007: 5006: 4999: 4993: 4988: 4981: 4978: 4967:Modern Library 4913: 4910: 4881: 4880: 4858: 4837: 4816:978-0521067911 4815: 4790: 4769:978-0521067911 4768: 4743: 4722:978-0521067911 4721: 4698: 4663: 4628: 4588: 4586: 4583: 4578: 4577: 4574: 4571: 4568: 4565: 4555: 4552: 4551: 4550: 4547: 4539: 4535: 4531: 4523: 4516: 4504: 4500: 4491: 4488: 4483: 4480: 4474: 4471: 4465: 4462: 4453: 4450: 4445: 4442: 4437: 4434: 4432: 4429: 4403: 4400: 4392: 4391: 4379: 4338: 4302: 4295: 4288: 4273: 4243: 4240: 4190:logical system 4162: 4159: 4154: 4140: 4139: 4128: 4117:logical truths 4089: 4086: 4062: 4061: 4024: 4017: 3958: 3957: 3920: 3897: 3896: 3895: 3894: 3811: 3810: 3809: 3808: 3709: 3708: 3707: 3706: 3700: 3699: 3698: 3692: 3691: 3690: 3590: 3587: 3586: 3585: 3558: 3557: 3538: 3489: 3488: 3455: 3454: 3431: 3430: 3328: 3327: 3326: 3325: 3272: 3178: 3172: 3166: 3153: 3152: 3151: 3150: 3100: 3090: 3089: 3088: 3038: 3009: 3003: 2985: 2984: 2940: 2939: 2864: 2863: 2845: 2844: 2817: 2816: 2778: 2777: 2758: 2711: 2710: 2709: 2708: 2707: 2706: 2705: 2704: 2656: 2655: 2648:Sheffer stroke 2645: 2611: 2610: 2607:Sheffer stroke 2576: 2573: 2545: 2544: 2524: 2502: 2501: 2489: 2474: 2473: 2461: 2446: 2445: 2433: 2408: 2407: 2406: 2405: 2357: 2356: 2355: 2237: 2236: 2205: 2204: 2175: 2174: 2167: 2166: 2156: 2155: 2147: 2146: 2134: 2133: 2118: 2117: 2097: 2096: 2089: 2088: 2026: 2023: 2016: 2015: 1990: 1989: 1970: 1969: 1899:Main article: 1896: 1893: 1871: 1861: 1857: 1851: 1847: 1841: 1837: 1831: 1827: 1821: 1817: 1811: 1807: 1801: 1797: 1783: 1779: 1773: 1769: 1763: 1759: 1742: 1738: 1732: 1728: 1722: 1718: 1712: 1708: 1702: 1698: 1692: 1688: 1682: 1678: 1672: 1668: 1662: 1658: 1652: 1648: 1642: 1638: 1632: 1628: 1611: 1607: 1601: 1597: 1591: 1587: 1581: 1577: 1573: 1570: 1545: 1544: 1462:Sheffer stroke 1128: 1125: 1124: 1123: 1120: 1081: 1058: 1051: 1044: 1037: 1021: 1018: 1017: 1016: 1011: 1006: 1001: 996: 991: 986: 972: 967: 961: 955: 937: 931: 926: 876: 804:Assertion-sign 801: 779: 669: 588: 583: 559:The theory of 556: 553: 552: 551: 504: 491: 481: 475: 468:Symbol strings 465: 464: 463: 457: 439: 433: 432: 431: 428: 425: 416: 410: 409: 408: 405: 404:"∀" (for all), 402: 399: 396: 395:"&" (and), 393: 357: 354: 345:interpretation 297: 294: 254: 251: 243:Modern Library 210:symbolic logic 160:that replaced 102: 76: 26: 24: 14: 13: 10: 9: 6: 4: 3: 2: 8835: 8824: 8821: 8819: 8816: 8814: 8811: 8809: 8806: 8804: 8801: 8799: 8796: 8794: 8791: 8789: 8786: 8784: 8781: 8779: 8776: 8775: 8773: 8758: 8757:Ernst Zermelo 8755: 8753: 8750: 8748: 8745: 8743: 8742:Willard Quine 8740: 8738: 8735: 8733: 8730: 8728: 8725: 8723: 8720: 8718: 8715: 8713: 8710: 8708: 8705: 8703: 8700: 8699: 8697: 8695: 8694:Set theorists 8691: 8685: 8682: 8680: 8677: 8675: 8672: 8671: 8669: 8663: 8661: 8658: 8657: 8654: 8646: 8643: 8641: 8640:Kripke–Platek 8638: 8634: 8631: 8630: 8629: 8626: 8625: 8624: 8621: 8617: 8614: 8613: 8612: 8611: 8607: 8603: 8600: 8599: 8598: 8595: 8594: 8591: 8588: 8586: 8583: 8581: 8578: 8576: 8573: 8572: 8570: 8566: 8560: 8557: 8555: 8552: 8550: 8547: 8545: 8543: 8538: 8536: 8533: 8531: 8528: 8525: 8521: 8518: 8516: 8513: 8509: 8506: 8504: 8501: 8499: 8496: 8495: 8494: 8491: 8488: 8484: 8481: 8479: 8476: 8474: 8471: 8469: 8466: 8465: 8463: 8460: 8456: 8450: 8447: 8445: 8442: 8440: 8437: 8435: 8432: 8430: 8427: 8425: 8422: 8420: 8417: 8413: 8410: 8408: 8405: 8404: 8403: 8400: 8398: 8395: 8393: 8390: 8388: 8385: 8383: 8380: 8377: 8373: 8370: 8368: 8365: 8363: 8360: 8359: 8357: 8351: 8348: 8347: 8344: 8338: 8335: 8333: 8330: 8328: 8325: 8323: 8320: 8318: 8315: 8313: 8310: 8308: 8305: 8302: 8299: 8297: 8294: 8293: 8291: 8289: 8285: 8277: 8276:specification 8274: 8272: 8269: 8268: 8267: 8264: 8263: 8260: 8257: 8255: 8252: 8250: 8247: 8245: 8242: 8240: 8237: 8235: 8232: 8230: 8227: 8225: 8222: 8218: 8215: 8214: 8213: 8210: 8208: 8205: 8201: 8198: 8196: 8193: 8191: 8188: 8187: 8186: 8183: 8181: 8178: 8177: 8175: 8173: 8169: 8164: 8154: 8151: 8150: 8148: 8144: 8140: 8133: 8128: 8126: 8121: 8119: 8114: 8113: 8110: 8100: 8099: 8094: 8086: 8080: 8077: 8075: 8072: 8070: 8067: 8065: 8062: 8058: 8055: 8054: 8053: 8050: 8048: 8045: 8043: 8040: 8038: 8034: 8031: 8029: 8026: 8024: 8021: 8019: 8016: 8014: 8011: 8010: 8008: 8004: 7998: 7995: 7993: 7990: 7988: 7987:Recursive set 7985: 7983: 7980: 7978: 7975: 7973: 7970: 7968: 7965: 7961: 7958: 7956: 7953: 7951: 7948: 7946: 7943: 7941: 7938: 7937: 7936: 7933: 7931: 7928: 7926: 7923: 7921: 7918: 7916: 7913: 7911: 7908: 7907: 7905: 7903: 7899: 7893: 7890: 7888: 7885: 7883: 7880: 7878: 7875: 7873: 7870: 7868: 7865: 7863: 7860: 7856: 7853: 7851: 7848: 7846: 7843: 7842: 7841: 7838: 7836: 7833: 7831: 7828: 7826: 7823: 7821: 7818: 7816: 7813: 7809: 7806: 7805: 7804: 7801: 7797: 7796:of arithmetic 7794: 7793: 7792: 7789: 7785: 7782: 7780: 7777: 7775: 7772: 7770: 7767: 7765: 7762: 7761: 7760: 7757: 7753: 7750: 7748: 7745: 7744: 7743: 7740: 7739: 7737: 7735: 7731: 7725: 7722: 7720: 7717: 7715: 7712: 7710: 7707: 7704: 7703:from ZFC 7700: 7697: 7695: 7692: 7686: 7683: 7682: 7681: 7678: 7676: 7673: 7671: 7668: 7667: 7666: 7663: 7661: 7658: 7656: 7653: 7651: 7648: 7646: 7643: 7641: 7638: 7636: 7633: 7632: 7630: 7628: 7624: 7614: 7613: 7609: 7608: 7603: 7602:non-Euclidean 7600: 7596: 7593: 7591: 7588: 7586: 7585: 7581: 7580: 7578: 7575: 7574: 7572: 7568: 7564: 7561: 7559: 7556: 7555: 7554: 7550: 7546: 7543: 7542: 7541: 7537: 7533: 7530: 7528: 7525: 7523: 7520: 7518: 7515: 7513: 7510: 7508: 7505: 7504: 7502: 7498: 7497: 7495: 7490: 7484: 7479:Example 7476: 7468: 7463: 7462: 7461: 7458: 7456: 7453: 7449: 7446: 7444: 7441: 7439: 7436: 7434: 7431: 7430: 7429: 7426: 7424: 7421: 7419: 7416: 7414: 7411: 7407: 7404: 7402: 7399: 7398: 7397: 7394: 7390: 7387: 7385: 7382: 7380: 7377: 7375: 7372: 7371: 7370: 7367: 7365: 7362: 7358: 7355: 7353: 7350: 7348: 7345: 7344: 7343: 7340: 7336: 7333: 7331: 7328: 7326: 7323: 7321: 7318: 7316: 7313: 7311: 7308: 7307: 7306: 7303: 7301: 7298: 7296: 7293: 7291: 7288: 7284: 7281: 7279: 7276: 7274: 7271: 7269: 7266: 7265: 7264: 7261: 7259: 7256: 7254: 7251: 7249: 7246: 7242: 7239: 7237: 7236:by definition 7234: 7233: 7232: 7229: 7225: 7222: 7221: 7220: 7217: 7215: 7212: 7210: 7207: 7205: 7202: 7200: 7197: 7196: 7193: 7190: 7188: 7184: 7179: 7173: 7169: 7159: 7156: 7154: 7151: 7149: 7146: 7144: 7141: 7139: 7136: 7134: 7131: 7129: 7126: 7124: 7123:Kripke–Platek 7121: 7119: 7116: 7112: 7109: 7107: 7104: 7103: 7102: 7099: 7098: 7096: 7092: 7084: 7081: 7080: 7079: 7076: 7074: 7071: 7067: 7064: 7063: 7062: 7059: 7057: 7054: 7052: 7049: 7047: 7044: 7042: 7039: 7036: 7032: 7028: 7025: 7021: 7018: 7016: 7013: 7011: 7008: 7007: 7006: 7002: 6999: 6998: 6996: 6994: 6990: 6986: 6978: 6975: 6973: 6970: 6968: 6967:constructible 6965: 6964: 6963: 6960: 6958: 6955: 6953: 6950: 6948: 6945: 6943: 6940: 6938: 6935: 6933: 6930: 6928: 6925: 6923: 6920: 6918: 6915: 6913: 6910: 6908: 6905: 6903: 6900: 6899: 6897: 6895: 6890: 6882: 6879: 6877: 6874: 6872: 6869: 6867: 6864: 6862: 6859: 6857: 6854: 6853: 6851: 6847: 6844: 6842: 6839: 6838: 6837: 6834: 6832: 6829: 6827: 6824: 6822: 6819: 6817: 6813: 6809: 6807: 6804: 6800: 6797: 6796: 6795: 6792: 6791: 6788: 6785: 6783: 6779: 6769: 6766: 6764: 6761: 6759: 6756: 6754: 6751: 6749: 6746: 6744: 6741: 6737: 6734: 6733: 6732: 6729: 6725: 6720: 6719: 6718: 6715: 6714: 6712: 6710: 6706: 6698: 6695: 6693: 6690: 6688: 6685: 6684: 6683: 6680: 6678: 6675: 6673: 6670: 6668: 6665: 6663: 6660: 6658: 6655: 6653: 6650: 6649: 6647: 6645: 6644:Propositional 6641: 6635: 6632: 6630: 6627: 6625: 6622: 6620: 6617: 6615: 6612: 6610: 6607: 6603: 6600: 6599: 6598: 6595: 6593: 6590: 6588: 6585: 6583: 6580: 6578: 6575: 6573: 6572:Logical truth 6570: 6568: 6565: 6564: 6562: 6560: 6556: 6553: 6551: 6547: 6541: 6538: 6536: 6533: 6531: 6528: 6526: 6523: 6521: 6518: 6516: 6512: 6508: 6504: 6502: 6499: 6497: 6494: 6492: 6488: 6485: 6484: 6482: 6480: 6474: 6469: 6463: 6460: 6458: 6455: 6453: 6450: 6448: 6445: 6443: 6440: 6438: 6435: 6433: 6430: 6428: 6425: 6423: 6420: 6418: 6415: 6413: 6410: 6408: 6405: 6401: 6398: 6397: 6396: 6393: 6392: 6390: 6386: 6382: 6375: 6370: 6368: 6363: 6361: 6356: 6355: 6352: 6339: 6335: 6332: 6328: 6325: 6321: 6320: 6318: 6314: 6307: 6303: 6300: 6296: 6293: 6289: 6286: 6282: 6279: 6275: 6274: 6272: 6268: 6260: 6259: 6254: 6249: 6245: 6244: 6241: 6240: 6235: 6234: 6232: 6228: 6224: 6217: 6212: 6210: 6205: 6203: 6198: 6197: 6194: 6184: 6183: 6171: 6165: 6162: 6160: 6157: 6155: 6152: 6150: 6147: 6146: 6144: 6140: 6133: 6130: 6127: 6124: 6121: 6118: 6115: 6112: 6109: 6106: 6103: 6100: 6097: 6094: 6091: 6088: 6085: 6082: 6079: 6076: 6073: 6070: 6067: 6064: 6063: 6061: 6057: 6050: 6049: 6045: 6042: 6041: 6037: 6034: 6033: 6029: 6026: 6025: 6021: 6018: 6017: 6013: 6010: 6009: 6005: 6002: 6001: 5997: 5994: 5993: 5989: 5986: 5985: 5984:Why Men Fight 5981: 5978: 5977: 5973: 5970: 5969: 5965: 5962: 5961: 5957: 5954: 5953: 5949: 5948: 5946: 5942: 5937: 5923: 5920: 5918: 5915: 5914: 5912: 5908: 5898: 5895: 5893: 5890: 5889: 5887: 5885: 5881: 5871: 5868: 5866: 5863: 5861: 5858: 5856: 5853: 5852: 5850: 5848: 5844: 5841: 5837: 5830: 5826: 5819: 5814: 5812: 5807: 5805: 5800: 5799: 5796: 5789: 5785: 5782: 5777: 5776: 5771: 5769: 5765: 5764: 5760: 5759: 5757: 5754: 5753: 5749: 5743: 5737: 5733: 5732:HarperCollins 5729: 5725: 5721: 5717: 5706: 5700: 5694: 5689: 5685: 5684: 5679: 5678:Weber, Michel 5675: 5671: 5669:0-674-32449-8 5665: 5661: 5657: 5653: 5649: 5645: 5641: 5637: 5635:0-521-33058-0 5631: 5627: 5624:. Cambridge: 5623: 5622: 5617: 5613: 5609: 5605: 5601: 5597: 5593: 5589: 5585: 5581: 5577: 5573: 5567: 5563: 5560:. Cambridge: 5559: 5558: 5553: 5549: 5545: 5543:0-691-05857-1 5539: 5535: 5531: 5527: 5523: 5519: 5517:0-19-503972-6 5513: 5509: 5505: 5501: 5496: 5492: 5488: 5484: 5480: 5476: 5472: 5468: 5464: 5460: 5456: 5452: 5448: 5446:0-12-238452-0 5442: 5438: 5434: 5430: 5426: 5425: 5421: 5414:, p. 46. 5413: 5408: 5405: 5399: 5396: 5390: 5387: 5383: 5377: 5374: 5370: 5366: 5360: 5357: 5353: 5347: 5344: 5338: 5335: 5329: 5326: 5321: 5314: 5311: 5305: 5302: 5296: 5293: 5287: 5284: 5280: 5276: 5271: 5269: 5265: 5252: 5251: 5243: 5240: 5234: 5231: 5225: 5222: 5218: 5214: 5208: 5205: 5201: 5197: 5193: 5189: 5183: 5180: 5174: 5171: 5168:, p. 78. 5167: 5161: 5158: 5155:, p. 16. 5154: 5153:Enderton 2001 5149: 5146: 5143:, p. 15. 5142: 5141:Enderton 2001 5138: 5133: 5130: 5126: 5120: 5117: 5104: 5098: 5096: 5092: 5079: 5075: 5069: 5067: 5065: 5061: 5056: 5052: 5051: 5043: 5040: 5036: 5031: 5028: 5025:, p. 83. 5024: 5019: 5016: 5009: 5005: 5004: 5000: 4997: 4994: 4992: 4989: 4987: 4984: 4983: 4979: 4977: 4974: 4972: 4968: 4963: 4961: 4957: 4952: 4950: 4946: 4941: 4939: 4935: 4931: 4927: 4922: 4918: 4911: 4909: 4907: 4903: 4899: 4895: 4891: 4887: 4877: 4873: 4869: 4865: 4861: 4859:0-521-62606-4 4855: 4851: 4847: 4843: 4838: 4834: 4830: 4826: 4822: 4818: 4812: 4807: 4802: 4798: 4797: 4791: 4787: 4783: 4779: 4775: 4771: 4765: 4760: 4755: 4751: 4750: 4744: 4740: 4736: 4732: 4728: 4724: 4718: 4713: 4708: 4704: 4699: 4695: 4691: 4687: 4683: 4678: 4673: 4669: 4664: 4660: 4656: 4652: 4648: 4643: 4638: 4634: 4629: 4625: 4621: 4617: 4613: 4608: 4603: 4599: 4595: 4590: 4589: 4584: 4582: 4575: 4572: 4569: 4566: 4562: 4561: 4560: 4553: 4548: 4545: 4540: 4532: 4529: 4524: 4521: 4517: 4514: 4510: 4505: 4501: 4498: 4497: 4496: 4489: 4487: 4481: 4479: 4472: 4470: 4463: 4461: 4459: 4451: 4449: 4443: 4441: 4435: 4430: 4427: 4425: 4421: 4417: 4410: 4408: 4401: 4399: 4397: 4389: 4384: 4380: 4377: 4373: 4368: 4367: 4366: 4364: 4360: 4355: 4353: 4343: 4337: 4335: 4331: 4327: 4321: 4319: 4315: 4314: 4309: 4305: 4298: 4291: 4278: 4272: 4270: 4266: 4262: 4255: 4253: 4249: 4241: 4239: 4237: 4233: 4229: 4225: 4224:formal system 4221: 4217: 4215: 4211: 4207: 4203: 4199: 4195: 4191: 4186: 4181: 4179: 4175: 4172: 4168: 4160: 4158: 4152: 4148: 4144: 4137: 4133: 4129: 4126: 4125:inconsistency 4122: 4121: 4120: 4118: 4113: 4111: 4107: 4103: 4099: 4095: 4092:According to 4087: 4085: 4084:1962:xxxix). 4083: 4079: 4075: 4071: 4067: 4059: 4055: 4051: 4047: 4043: 4039: 4035: 4032: 4027: 4022: 4018: 4015: 4011: 4007: 4003: 3999: 3995: 3991: 3987: 3986: 3985: 3983: 3979: 3975: 3971: 3967: 3963: 3955: 3951: 3947: 3943: 3939: 3935: 3931: 3928: 3923: 3918: 3914: 3913: 3912: 3910: 3906: 3902: 3892: 3888: 3884: 3880: 3876: 3875: 3874: 3870: 3866: 3863: 3859: 3855: 3851: 3847: 3843: 3839: 3835: 3831: 3828: 3827: 3826: 3824: 3820: 3816: 3806: 3802: 3799:),' or to '(φ 3798: 3794: 3790: 3786: 3782: 3781: 3779: 3775: 3771: 3767: 3763: 3759: 3756: 3752: 3751: 3750: 3748: 3744: 3740: 3736: 3732: 3728: 3724: 3720: 3716: 3714: 3704: 3703: 3701: 3696: 3695: 3693: 3688: 3684: 3680: 3676: 3673: 3669: 3665: 3661: 3657: 3656: 3654: 3651: 3650: 3649: 3647: 3642: 3640: 3636: 3632: 3628: 3624: 3620: 3616: 3612: 3611:ordered pairs 3608: 3604: 3600: 3596: 3588: 3584:1967:173–174) 3583: 3579: 3575: 3571: 3567: 3563: 3562: 3561: 3555: 3552: 3548: 3545: 3541: 3536: 3533: 3529: 3525: 3521: 3517: 3513: 3509: 3505: 3501: 3498: 3497: 3496: 3494: 3486: 3482: 3478: 3474: 3470: 3469: 3468: 3466: 3462: 3460: 3452: 3448: 3444: 3440: 3436: 3435: 3434: 3429: 3426: 3423: 3419: 3415: 3412: 3409: 3405: 3401: 3397: 3394: 3390: 3386: 3383: 3382: 3381: 3379: 3375: 3371: 3369: 3365: 3361: 3357: 3353: 3349: 3345: 3341: 3337: 3333: 3323: 3319: 3315: 3312: 3308: 3304: 3300: 3297: 3296: 3295: 3294: 3293: 3291: 3288: 3285: 3282: 3279: 3275: 3270: 3267: 3263: 3259: 3255: 3251: 3247: 3245: 3241: 3234: 3230: 3226: 3221: 3219: 3215: 3211: 3208: 3203: 3201: 3197: 3193: 3189: 3184: 3181: 3175: 3169: 3164: 3159: 3157: 3148: 3144: 3140: 3136: 3135: 3134: 3131: 3127: 3123: 3119: 3115: 3111: 3108: 3103: 3098: 3094: 3091: 3086: 3082: 3078: 3074: 3073: 3072: 3069: 3065: 3061: 3057: 3053: 3049: 3046: 3041: 3036: 3032: 3029: 3028: 3027: 3025: 3021: 3017: 3012: 3006: 3000: 2998: 2994: 2990: 2982: 2979: 2975: 2971: 2967: 2963: 2960: 2956: 2952: 2948: 2945: 2944: 2943: 2938: 2934: 2930: 2926: 2922: 2918: 2915: 2911: 2907: 2903: 2899: 2896: 2892: 2888: 2884: 2880: 2879: 2878: 2876: 2872: 2867: 2862: 2858: 2854: 2850: 2849: 2848: 2843: 2839: 2835: 2831: 2830: 2829: 2826: 2822: 2815: 2811: 2807: 2803: 2802: 2801: 2799: 2795: 2791: 2787: 2783: 2775: 2771: 2767: 2763: 2759: 2756: 2752: 2748: 2744: 2740: 2739: 2738: 2736: 2732: 2728: 2724: 2720: 2716: 2702: 2698: 2694: 2690: 2686: 2682: 2678: 2674: 2670: 2666: 2662: 2658: 2657: 2653: 2649: 2646: 2643: 2639: 2635: 2631: 2624: 2620: 2617: 2616: 2615: 2614: 2613: 2612: 2608: 2604: 2600: 2596: 2592: 2588: 2587: 2586: 2585: 2584: 2582: 2574: 2572: 2570: 2566: 2562: 2558: 2554: 2550: 2542: 2538: 2534: 2530: 2522: 2518: 2514: 2510: 2509: 2508: 2505: 2499: 2495: 2487: 2483: 2479: 2478: 2477: 2471: 2467: 2459: 2455: 2451: 2450: 2449: 2443: 2439: 2431: 2427: 2423: 2422: 2421: 2418: 2416: 2412: 2403: 2402: 2400: 2397: 2393: 2390: 2387: 2383: 2380: 2376: 2373: 2369: 2365: 2361: 2358: 2353: 2349: 2345: 2342: 2339: 2335: 2334: 2332: 2328: 2324: 2320: 2316: 2313: 2310: 2307: 2303: 2300: 2299: 2298: 2296: 2291: 2289: 2285: 2281: 2277: 2273: 2269: 2263: 2261: 2257: 2253: 2249: 2245: 2240: 2234: 2230: 2226: 2222: 2218: 2214: 2210: 2209: 2208: 2203: 2199: 2195: 2191: 2187: 2183: 2180: 2179: 2178: 2172: 2171: 2170: 2164: 2161: 2160: 2159: 2153: 2152: 2151: 2144: 2141:⊢ ((p ∧ q) ⊃ 2140: 2139: 2138: 2131: 2127: 2123: 2122: 2121: 2115: 2111: 2107: 2103: 2102: 2101: 2094: 2093: 2092: 2086: 2082: 2078: 2074: 2070: 2066: 2065: 2064: 2061: 2059: 2055: 2051: 2047: 2043: 2039: 2031: 2024: 2022: 2019: 2013: 2009: 2006: 2002: 2001: 2000: 1998: 1995: 1987: 1986: 1985: 1983: 1982: 1977: 1973: 1967: 1963: 1959: 1955: 1954: 1953: 1951: 1947: 1944: 1940: 1936: 1932: 1928: 1924: 1920: 1916: 1911: 1907: 1902: 1894: 1891: 1885: 1880: 1877: 1874: 1869: 1864: 1854: 1844: 1834: 1824: 1814: 1804: 1794: 1789: 1786: 1776: 1766: 1757: 1752: 1750: 1745: 1735: 1725: 1715: 1705: 1695: 1685: 1675: 1665: 1655: 1645: 1635: 1626: 1621: 1619: 1614: 1604: 1594: 1584: 1571: 1569: 1567: 1563: 1561: 1557: 1555: 1551: 1542: 1538: 1534: 1530: 1526: 1522: 1518: 1514: 1510: 1509: 1508: 1506: 1502: 1497: 1495: 1491: 1487: 1483: 1479: 1475: 1471: 1467: 1463: 1458: 1456: 1452: 1448: 1443: 1442: 1438: 1434: 1430: 1426: 1422: 1418: 1417: 1413: 1409: 1405: 1401: 1397: 1393: 1392: 1388: 1384: 1380: 1376: 1374: 1370: 1366: 1363: 1359: 1356: 1352: 1349: 1345: 1342: 1338: 1335: 1331: 1327: 1325: 1321: 1317: 1313: 1310: 1306: 1302: 1298: 1294: 1291: 1287: 1283: 1281: 1277: 1273: 1270: 1266: 1263: 1259: 1256: 1252: 1248: 1246: 1242: 1238: 1235: 1231: 1228: 1225: 1221: 1217: 1215: 1211: 1208: 1204: 1201: 1197: 1194: 1190: 1186: 1184: 1179: 1178:modus ponens 1177: 1173: 1169: 1167: 1163: 1159: 1155: 1151: 1148: 1144: 1140: 1136: 1134: 1126: 1121: 1118: 1114: 1110: 1106: 1102: 1098: 1094: 1090: 1086: 1082: 1079: 1075: 1071: 1067: 1063: 1059: 1056: 1052: 1049: 1045: 1042: 1038: 1035: 1031: 1030: 1029: 1027: 1019: 1015: 1012: 1010: 1007: 1005: 1002: 1000: 997: 995: 992: 990: 987: 984: 980: 976: 973: 971: 968: 965: 962: 959: 956: 953: 949: 945: 941: 938: 935: 932: 930: 927: 924: 920: 917: 913: 910: 906: 902: 898: 895: 891: 888:s version of 884: 880: 877: 874: 870: 866: 862: 858: 854: 851: 847: 844: 841: 838:', whereas '⊦ 837: 833: 829: 826: 822: 819: 816: 812: 809: 805: 802: 799: 795: 794:Gottlob Frege 791: 787: 783: 780: 777: 773: 769: 763: 759: 755: 751: 747: 743: 739: 735: 732: 728: 723: 717: 713: 709: 705: 701: 697: 693: 689: 685: 681: 677: 673: 670: 667: 663: 659: 655: 651: 647: 644: 641: 638: 631: 627: 624: 620: 616: 612: 609: 605: 600: 596: 592: 589: 587: 584: 582: 579: 578: 577: 575: 571: 567: 562: 554: 549: 545: 541: 537: 533: 528: 524: 519: 515: 511: 507: 502: 498: 495: 492: 489: 485: 482: 479: 476: 473: 472:concatenation 469: 466: 461: 458: 455: 451: 447: 443: 440: 437: 434: 429: 426: 423: 422: 420: 417: 414: 411: 406: 403: 400: 397: 394: 391: 390: 388: 385: 384: 382: 378: 375: 374: 373: 371: 362: 355: 353: 350: 346: 342: 338: 333: 329: 325: 323: 319: 315: 311: 307: 303: 295: 293: 291: 286: 284: 280: 279:real analysis 276: 272: 268: 264: 261:covered only 260: 252: 250: 248: 244: 240: 236: 234: 230: 226: 221: 219: 215: 211: 207: 203: 199: 195: 191: 189: 185: 181: 180: 175: 171: 167: 163: 159: 155: 151: 147: 143: 139: 138: 133: 132: 125: 122: 121: 116: 110: 108: 100: 97: 96: 91: 85: 83: 72: 68: 64: 60: 53: 48: 44: 40: 33: 19: 8707:Georg Cantor 8702:Paul Bernays 8633:Morse–Kelley 8609: 8608: 8541: 8540:Subset 8487:hereditarily 8449:Venn diagram 8407:ordered pair 8322:Intersection 8266:Axiom schema 8089: 7887:Ultraproduct 7734:Model theory 7699:Independence 7635:Formal proof 7627:Proof theory 7611: 7610: 7583: 7540:real numbers 7512:second-order 7423:Substitution 7300:Metalanguage 7241:conservative 7214:Axiom schema 7158:Constructive 7128:Morse–Kelley 7094:Set theories 7073:Aleph number 7066:inaccessible 6972:Grothendieck 6856:intersection 6743:Higher-order 6731:Second-order 6677:Truth tables 6634:Venn diagram 6417:Formal proof 6256: 6238: 6237: 6174: 6154:Earl Russell 6072:Dora Russell 6046: 6038: 6030: 6022: 6014: 6006: 5998: 5990: 5982: 5974: 5967: 5966: 5958: 5950: 5774: 5768:A. D. Irvine 5761: 5730:. New York: 5727: 5716:Academia.edu 5714:– via 5710:13 September 5708:. Retrieved 5688:Ontos Verlag 5682: 5655: 5620: 5583: 5556: 5552:Hardy, G. H. 5529: 5506:. New York: 5503: 5462: 5432: 5407: 5398: 5389: 5381: 5376: 5368: 5364: 5359: 5351: 5346: 5337: 5328: 5319: 5313: 5304: 5295: 5286: 5255:. Retrieved 5249: 5242: 5233: 5224: 5219:1962:xiv–xv) 5216: 5212: 5207: 5199: 5195: 5191: 5187: 5182: 5173: 5160: 5148: 5132: 5119: 5107:. Retrieved 5082:. Retrieved 5049: 5042: 5030: 5018: 5001: 4975: 4970: 4964: 4959: 4955: 4953: 4944: 4942: 4933: 4925: 4920: 4915: 4883: 4841: 4795: 4748: 4702: 4667: 4632: 4593: 4579: 4557: 4512: 4508: 4493: 4485: 4476: 4467: 4455: 4447: 4439: 4423: 4419: 4415: 4412: 4405: 4395: 4393: 4387: 4382: 4375: 4371: 4362: 4358: 4356: 4351: 4348: 4341: 4333: 4329: 4325: 4323: 4317: 4311: 4310:in his 1919 4300: 4293: 4286: 4283: 4276: 4264: 4260: 4257: 4251: 4247: 4245: 4235: 4231: 4227: 4218: 4213: 4209: 4201: 4197: 4193: 4184: 4182: 4176: 4164: 4146: 4141: 4136:completeness 4114: 4110:Frank Ramsey 4091: 4081: 4077: 4073: 4069: 4065: 4063: 4057: 4053: 4049: 4045: 4041: 4037: 4033: 4030: 4025: 4020: 4013: 4009: 4005: 4001: 3997: 3994:p, q, r, ... 3993: 3989: 3981: 3977: 3973: 3969: 3966:truth-values 3965: 3961: 3959: 3953: 3949: 3945: 3941: 3937: 3933: 3929: 3926: 3921: 3916: 3908: 3904: 3900: 3898: 3890: 3886: 3882: 3878: 3872: 3868: 3864: 3861: 3857: 3853: 3849: 3845: 3841: 3837: 3833: 3829: 3822: 3818: 3814: 3812: 3804: 3800: 3796: 3795:satisfies (φ 3792: 3788: 3784: 3777: 3773: 3769: 3765: 3761: 3757: 3754: 3746: 3742: 3738: 3734: 3730: 3722: 3718: 3717: 3712: 3710: 3686: 3682: 3678: 3674: 3671: 3667: 3663: 3659: 3652: 3645: 3643: 3638: 3634: 3630: 3626: 3622: 3618: 3614: 3602: 3598: 3594: 3592: 3581: 3577: 3573: 3569: 3568:satisfying φ 3565: 3559: 3553: 3550: 3546: 3543: 3539: 3534: 3531: 3527: 3523: 3519: 3515: 3511: 3507: 3503: 3499: 3492: 3490: 3484: 3480: 3476: 3472: 3464: 3463: 3458: 3456: 3450: 3446: 3442: 3438: 3432: 3427: 3424: 3421: 3417: 3413: 3410: 3407: 3403: 3399: 3395: 3392: 3388: 3384: 3377: 3373: 3372: 3367: 3363: 3359: 3355: 3351: 3347: 3343: 3339: 3335: 3331: 3329: 3317: 3314:modus ponens 3310: 3306: 3302: 3298: 3289: 3286: 3283: 3280: 3277: 3273: 3268: 3265: 3261: 3257: 3253: 3249: 3248: 3243: 3239: 3232: 3224: 3222: 3217: 3213: 3209: 3206: 3204: 3200:second-order 3199: 3195: 3187: 3185: 3179: 3173: 3167: 3162: 3160: 3155: 3154: 3146: 3142: 3138: 3132: 3129: 3125: 3121: 3117: 3113: 3109: 3106: 3101: 3096: 3092: 3084: 3080: 3076: 3070: 3067: 3063: 3059: 3055: 3051: 3047: 3044: 3039: 3034: 3030: 3023: 3019: 3015: 3014:" appear at 3010: 3004: 3001: 2996: 2992: 2988: 2986: 2980: 2977: 2973: 2969: 2965: 2961: 2958: 2954: 2950: 2946: 2941: 2936: 2932: 2928: 2924: 2920: 2916: 2913: 2909: 2905: 2901: 2897: 2894: 2890: 2886: 2882: 2874: 2870: 2868: 2865: 2860: 2856: 2852: 2846: 2841: 2837: 2833: 2824: 2820: 2818: 2813: 2809: 2805: 2797: 2793: 2789: 2785: 2781: 2779: 2773: 2769: 2765: 2761: 2754: 2750: 2746: 2742: 2734: 2730: 2726: 2722: 2718: 2714: 2712: 2700: 2696: 2692: 2688: 2684: 2680: 2676: 2672: 2668: 2664: 2660: 2647: 2641: 2629: 2622: 2618: 2602: 2598: 2594: 2590: 2578: 2568: 2564: 2560: 2559:)) nor to (( 2556: 2552: 2548: 2546: 2540: 2536: 2532: 2528: 2520: 2516: 2512: 2506: 2503: 2497: 2493: 2485: 2481: 2476:alternately 2475: 2469: 2465: 2457: 2453: 2448:alternately 2447: 2441: 2437: 2429: 2425: 2419: 2410: 2409: 2398: 2395: 2391: 2388: 2385: 2381: 2378: 2374: 2371: 2367: 2363: 2359: 2351: 2347: 2343: 2340: 2337: 2330: 2326: 2322: 2318: 2314: 2311: 2308: 2305: 2301: 2294: 2292: 2287: 2283: 2279: 2275: 2271: 2267: 2264: 2259: 2255: 2251: 2247: 2243: 2241: 2238: 2232: 2228: 2224: 2220: 2216: 2212: 2206: 2201: 2197: 2193: 2189: 2185: 2181: 2176: 2168: 2162: 2157: 2148: 2142: 2135: 2129: 2125: 2119: 2113: 2109: 2105: 2098: 2090: 2084: 2080: 2076: 2072: 2068: 2062: 2057: 2053: 2049: 2045: 2041: 2037: 2029: 2028: 2020: 2017: 2011: 2007: 2004: 1996: 1993: 1991: 1979: 1975: 1974: 1971: 1965: 1961: 1949: 1948: 1942: 1938: 1934: 1930: 1926: 1922: 1918: 1914: 1908: 1904: 1888: 1882: 1878: 1872: 1867: 1862: 1852: 1842: 1832: 1822: 1812: 1802: 1790: 1784: 1774: 1764: 1753: 1748: 1743: 1733: 1723: 1713: 1703: 1693: 1683: 1673: 1663: 1653: 1643: 1633: 1624: 1622: 1612: 1602: 1592: 1582: 1575: 1565: 1564: 1559: 1558: 1553: 1549: 1546: 1540: 1536: 1532: 1528: 1524: 1520: 1516: 1512: 1504: 1500: 1498: 1493: 1489: 1485: 1477: 1473: 1469: 1465: 1459: 1454: 1450: 1446: 1444: 1440: 1436: 1432: 1428: 1424: 1420: 1419: 1415: 1411: 1407: 1403: 1399: 1395: 1394: 1390: 1386: 1382: 1378: 1377: 1372: 1368: 1364: 1361: 1357: 1354: 1350: 1347: 1343: 1340: 1336: 1333: 1329: 1328: 1323: 1319: 1315: 1311: 1308: 1304: 1300: 1296: 1292: 1289: 1285: 1284: 1279: 1275: 1271: 1268: 1264: 1261: 1257: 1254: 1250: 1249: 1244: 1240: 1236: 1233: 1229: 1226: 1223: 1219: 1218: 1213: 1209: 1206: 1202: 1199: 1195: 1192: 1188: 1187: 1182: 1180: 1175: 1171: 1170: 1165: 1161: 1157: 1153: 1149: 1146: 1142: 1138: 1137: 1132: 1130: 1116: 1112: 1108: 1104: 1100: 1096: 1092: 1088: 1084: 1077: 1073: 1069: 1065: 1061: 1054: 1047: 1040: 1033: 1025: 1023: 1014:Unit classes 1013: 1008: 1003: 998: 993: 988: 982: 978: 974: 969: 963: 957: 951: 947: 943: 939: 933: 928: 922: 918: 915: 911: 908: 904: 900: 896: 893: 890:modus ponens 889: 882: 878: 872: 868: 864: 860: 856: 852: 849: 845: 842: 839: 835: 831: 827: 824: 820: 817: 814: 810: 807: 803: 797: 789: 785: 782:Truth-values 781: 775: 771: 767: 761: 757: 753: 749: 745: 741: 737: 733: 730: 726: 721: 715: 711: 707: 703: 699: 695: 691: 687: 683: 679: 675: 671: 665: 661: 657: 653: 649: 645: 642: 639: 636: 629: 625: 622: 618: 614: 610: 607: 603: 598: 594: 590: 585: 580: 576:1962:4–36): 573: 569: 565: 560: 558: 555:Construction 547: 543: 539: 535: 531: 526: 522: 517: 513: 509: 505: 501:modus ponens 497: 496:modus ponens 493: 483: 477: 467: 462:"(" and ")". 459: 456:", etc.; and 453: 449: 445: 441: 435: 418: 412: 386: 380: 377:Symbols used 376: 369: 367: 344: 340: 336: 331: 328:Truth-values 327: 326: 322:truth-values 321: 318:model theory 313: 309: 299: 287: 283:in principle 282: 275:real numbers 258: 256: 246: 238: 237: 232: 228: 222: 193: 192: 187: 183: 177: 173: 169: 165: 161: 157: 153: 136: 135: 130: 129: 127: 118: 112: 106: 104: 93: 87: 81: 78: 62: 51: 43: 8732:Thomas Jech 8575:Alternative 8554:Uncountable 8508:Ultrafilter 8367:Cardinality 8271:replacement 8212:Determinacy 7997:Type theory 7945:undecidable 7877:Truth value 7764:equivalence 7443:non-logical 7056:Enumeration 7046:Isomorphism 6993:cardinality 6977:Von Neumann 6942:Ultrafilter 6907:Uncountable 6841:equivalence 6758:Quantifiers 6748:Fixed-point 6717:First-order 6597:Consistency 6582:Proposition 6559:Traditional 6530:Lindström's 6520:Compactness 6462:Type theory 6407:Cardinality 6242:(1910–1913) 6122:(godfather) 5971:(1910–1913) 5960:On Denoting 5910:Mathematics 5691: [ 5455:Gödel, Kurt 5412:Kleene 1952 5237:PM 1927:xlv 5228:PM 1927:xiv 5166:Kleene 1952 5137:Kleene 1952 5125:Kleene 1952 4361:criticised 4336:is finite." 4265:extensional 4261:intensional 3956:1962:xxxix) 3702:α ∩ –α = Λ 3694:α ∪ –α = V 3648:1962:188): 3613:. Sections 3609:as sets of 3473:description 3366:applied to 3196:first-order 3192:truth table 2729:" i.e., " ∀ 2638:truth table 2597:with a new 2207:stands for 2169:stands for 1941:requires a 1107:is true or 1085:Disjunction 934:Definitions 768:grammatical 714:a notation 672:Equivalence 460:parentheses 438:"0" (zero); 164:with a new 90:G. H. Hardy 8772:Categories 8727:Kurt Gödel 8712:Paul Cohen 8549:Transitive 8317:Identities 8301:Complement 8288:Operations 8249:Regularity 8217:projective 8180:Adjunction 8139:Set theory 7808:elementary 7501:arithmetic 7369:Quantifier 7347:functional 7219:Expression 6937:Transitive 6881:identities 6866:complement 6799:hereditary 6782:Set theory 5839:Philosophy 5422:References 5279:Gödel 1990 5275:Gödel 1944 5023:Hardy 2004 4919:says that 4876:0877.01042 4825:53.0038.02 4778:53.0038.02 4731:51.0046.06 4686:44.0068.01 4651:43.0093.03 4616:41.0083.02 4528:allegories 4402:Gödel 1944 4299:∧ . . . ∧ 4147:Principia' 4104:, and the 3976:and ƒ of ψ 3749:1962:188) 3607:set theory 3491:From this 2877:1962:138) 2784:: section 2415:Kurt Gödel 1943:definition 1910:Kurt Gödel 1554:✱8.1–✱8.13 1486:ad finitum 899:' and '⊦ ( 855:' means ' 722:definition 599:Definition 570:real-world 401:"¬" (not), 381:definition 341:assignment 302:Kurt Gödel 263:set theory 214:set theory 170:Appendix C 166:Appendix B 158:Appendix A 8660:Paradoxes 8580:Axiomatic 8559:Universal 8535:Singleton 8530:Recursive 8473:Countable 8468:Amorphous 8327:Power set 8244:Power set 8195:dependent 8190:countable 8079:Supertask 7982:Recursion 7940:decidable 7774:saturated 7752:of models 7675:deductive 7670:axiomatic 7590:Hilbert's 7577:Euclidean 7558:canonical 7481:axiomatic 7413:Signature 7342:Predicate 7231:Extension 7153:Ackermann 7078:Operation 6957:Universal 6947:Recursive 6922:Singleton 6917:Inhabited 6902:Countable 6892:Types of 6876:power set 6846:partition 6763:Predicate 6709:Predicate 6624:Syllogism 6614:Soundness 6587:Inference 6577:Tautology 6479:paradoxes 6104:(brother) 5554:(2004) . 5431:(2001) . 5213:Tractatus 5200:Principia 5010:Footnotes 4694:a11002789 4659:a11002789 4624:a11002789 4511:+2 and 2( 4424:definiens 4420:Principia 4396:Principia 4388:Principia 4383:Principia 4376:Principia 4372:Principia 4363:Principia 4232:Principia 4228:Principia 4194:Principia 4192:(such as 4185:Principia 4165:In 1930, 3893:1962:188) 3813:At least 3783:"i.e., ' 3689:1962:188) 3483:, where φ 2780:Sections 2667:, then ' 2535:) & ( 2293:Example, 2124:⊢ (p ∧ q 1048:Assertion 879:Inference 875:1962:92). 790:falsehood 764:1962:12), 601:below) as 581:Variables 442:variables 398:"V" (or), 259:Principia 182:, but as 8664:Problems 8568:Theories 8544:Superset 8520:Infinite 8349:Concepts 8229:Infinity 8146:Overview 8064:Logicism 8057:timeline 8033:Concrete 7892:Validity 7862:T-schema 7855:Kripke's 7850:Tarski's 7845:semantic 7835:Strength 7784:submodel 7779:spectrum 7747:function 7595:Tarski's 7584:Elements 7571:geometry 7527:Robinson 7448:variable 7433:function 7406:spectrum 7396:Sentence 7352:variable 7295:Language 7248:Relation 7209:Automata 7199:Alphabet 7183:language 7037:-jection 7015:codomain 7001:Function 6962:Universe 6932:Infinite 6836:Relation 6619:Validity 6609:Argument 6507:theorem, 6270:Concepts 6248:glossary 6116:(mother) 6110:(father) 5788:Metamath 5726:(2009). 5654:(1967). 5614:(1986). 5596:53001848 5582:(1952). 5528:(2000). 5491:6467049M 5475:44006786 5109:5 August 5084:5 August 4980:See also 4930:logicism 4833:25015133 4786:25015133 4739:25015133 4585:Editions 4431:Contents 4339:— 4274:— 4206:Catch-22 3807:1962:25) 3186:Section 3161:Section 2713:Section 2640:, i.e., 2290:", etc. 2014:1927:92) 1999:writes: 1968:1927:4). 1895:Notation 1453:through 1062:Negation 994:Identity 925:1962:9). 834:implies 800:1962:7). 668:1962:12) 632:1962:11) 538:implies 290:geometry 8602:General 8597:Zermelo 8503:subbase 8485: ( 8424:Forcing 8402:Element 8374: ( 8352:Methods 8239:Pairing 8006:Related 7803:Diagram 7701: ( 7680:Hilbert 7665:Systems 7660:Theorem 7538:of the 7483:systems 7263:Formula 7258:Grammar 7174: ( 7118:General 6831:Forcing 6816:Element 6736:Monadic 6511:paradox 6452:Theorem 6388:General 6142:Related 5644:0872858 5618:(ed.). 5604:9296141 5483:2007378 5461:(ed.). 4969:placed 4868:1700771 4526:called 3948:) ≡ ƒ(ψ 3825:above: 3433:means: 3238:s use) 3145:) ↔︎ ψ( 2721:adds "( 2336:where " 2132:p ⊃ q). 2116:p ⊃ q). 1793:Zermelo 1747:. When 1623:In the 1072:", or " 981:and 16 946:" and " 712:discuss 676:Logical 595:defined 245:placed 71:page 86 8493:Filter 8483:Finite 8419:Family 8362:Almost 8200:global 8185:Choice 8172:Axioms 7769:finite 7532:Skolem 7485: 7460:Theory 7428:Symbol 7418:String 7401:atomic 7278:ground 7273:closed 7268:atomic 7224:ground 7187:syntax 7083:binary 7010:domain 6927:Finite 6692:finite 6550:Logics 6509: 6457:Theory 6261:(1929) 6180: 6059:Family 6051:(1959) 6043:(1945) 6035:(1938) 6027:(1935) 6019:(1929) 6011:(1927) 6003:(1922) 5995:(1919) 5987:(1916) 5979:(1912) 5963:(1905) 5955:(1903) 5738: 5701: 5666: 5642: 5632: 5602: 5594: 5568: 5540: 5514: 5489: 5481: 5473: 5443: 4912:Legacy 4904: 4896: 4888: 4874: 4866: 4856: 4831: 4823: 4813: 4784: 4776: 4766: 4737: 4729: 4719: 4692: 4684: 4657: 4649: 4622: 4614: 4416:✱1–✱21 4259:quasi- 4127:), and 4100:, the 4094:Carnap 3823:✱13.01 3639:✱22.03 3635:✱22.03 3631:✱22.02 3627:✱22.01 3500:✱14.02 3459:✱13.02 3385:✱13.01 3322:syntax 3093:✱10.03 3083:) → ψ( 3031:✱10.02 3020:✱10.03 3016:✱10.02 3008:and "≡ 2947:✱10.01 2630:matrix 2619:Matrix 2456:& 2428:& 2219:) ∧ (( 2163:✱9.521 2145:p ⊃ q) 2044:" or " 1860:,...,σ 1850:,...,τ 1840:,...,σ 1830:,...,τ 1820:×...×τ 1810:,...,τ 1800:,...,τ 1782:,...,τ 1772:,...,σ 1762:,...,τ 1741:,...,σ 1731:,...,σ 1721:,...,τ 1701:,...,σ 1691:,...,τ 1681:,...,σ 1671:,...,τ 1661:,...,σ 1651:,...,τ 1641:,...,σ 1631:,...,τ 1618:Church 1610:×...×τ 1600:,...,τ 1590:,...,τ 1580:,...,τ 1423:. If φ 1087:: "If 1064:: "If 892:. " '⊦ 867:or of 706:)'." ( 488:axioms 486:: The 349:Kleene 273:, and 204:, and 202:axioms 123:(1986) 117:, 98:(1940) 92:, 67:p. 379 63:✱54.43 8585:Naive 8515:Fuzzy 8478:Empty 8461:types 8412:tuple 8382:Class 8376:large 8337:Union 8254:Union 7759:Model 7507:Peano 7364:Proof 7204:Arity 7133:Naive 7020:image 6952:Fuzzy 6912:Empty 6861:union 6806:Class 6447:Model 6437:Lemma 6395:Axiom 6316:Study 6230:Books 6098:(son) 6092:(son) 5944:Works 5766:– by 5695:] 5257:1 May 4407:Gödel 4208:: if 4171:model 3666:) or 3564:"The 3250:✱12.1 3236:' 2636:), a 2626:' 2504:etc. 2360:✱3.02 2302:✱3.01 2286:", "χ 2104:⊢ (p 2087:p ⊃ q 2056:), (∃ 2033:' 1958:Peano 1711:,...τ 1505:✱1.72 1455:✱9.15 1427:and ψ 1421:✱1.72 1398:. If 1396:✱1.71 1381:. If 1183:✱1.11 1139:✱1.01 1133:first 921:' " ( 886:' 806:: "'⊦ 786:truth 542:THEN 225:types 156:, an 18:1+1=2 8498:base 7882:Type 7685:list 7489:list 7466:list 7455:Term 7389:rank 7283:open 7177:list 6989:Maps 6894:sets 6753:Free 6723:list 6473:list 6400:list 5736:ISBN 5712:2023 5699:ISBN 5664:ISBN 5630:ISBN 5600:OCLC 5592:LCCN 5566:ISBN 5538:ISBN 5512:ISBN 5479:OCLC 5471:LCCN 5441:ISBN 5259:2018 5111:2009 5086:2009 4965:The 4902:ISBN 4894:ISBN 4886:ISBN 4854:ISBN 4829:LCCN 4811:ISBN 4782:LCCN 4764:ISBN 4735:LCCN 4717:ISBN 4690:LCCN 4655:LCCN 4620:LCCN 4008:for 3964:the 3889:." ( 3836:) = 3655:ε α 3617:and 3601:and 3510:) (φ 3502:. E 3441:and 3311:✱1.1 3198:and 3180:x, y 3018:and 2949:. (Ǝ 2687:and 2663:and 2652:NAND 2567:) → 2492:(¬(¬ 2464:(¬(¬ 2436:(~(~ 2350:and 2258:", " 2254:", " 2071:. ⊢ 2048:", " 2040:", " 2010:." ( 1921:", " 1917:", " 1566:✱120 1527:and 1511:"If 1501:✱1.2 1482:NAND 1468:and 1402:and 1379:✱1.7 1330:✱1.6 1314:∨ ( 1295:∨ ( 1286:✱1.5 1251:✱1.4 1220:✱1.3 1189:✱1.2 1172:✱1.1 1131:The 1119:" ". 1091:and 1083:(6) 1080:" ". 1060:(5) 1053:(4) 1046:(3) 1039:(2) 1032:(1) 1024:Cf. 534:and 525:and 452:", " 448:", " 257:The 168:and 148:and 128:The 8459:Set 7569:of 7551:of 7499:of 7031:Sur 7005:Map 6812:Ur- 6794:Set 5352:✱56 4872:Zbl 4846:doi 4821:JFM 4801:hdl 4774:JFM 4754:hdl 4727:JFM 4707:hdl 4682:JFM 4672:hdl 4647:JFM 4637:hdl 4612:JFM 4602:hdl 4458:ZFC 4418:of 4236:are 4000:≡ ψ 3952:) ( 3944:ƒ(φ 3670:(φ 3619:✱22 3615:✱20 3595:✱14 3522:( Ǝ 3506:( ℩ 3471:"A 3402:(φ) 3256:(Ǝ 3188:✱12 3177:, ⊃ 3171:, ⊃ 3163:✱11 3141:(φ( 3128:≡ ψ 3079:(φ( 3066:⊃ ψ 2935:⊃ χ 2912:⊃ χ 2893:⊃ ψ 2786:✱10 2760:"(Ǝ 2642:all 2551:→ ( 2523:) = 2496:v ¬ 2488:) = 2468:v ¬ 2460:) = 2440:v ~ 2432:) = 2325:v ~ 2321:~(~ 2272:✱13 2268:✱13 2248:✱20 2244:✱14 2227:)⊃( 2196:.⊃. 2069:3.4 1937:". 1791:In 1560:✱88 1503:to 1496:". 1435:∨ ψ 1332:. ⊦ 1322:). 1288:. ⊦ 1253:. ⊦ 1222:. ⊦ 1191:. ⊦ 1099:or 796:) ( 760:) ( 664:. ( 656:∨ ~ 652:~(~ 628:. ( 227:in 54:✱56 8774:: 7955:NP 7579:: 7573:: 7503:: 7180:), 7035:Bi 7027:In 5758:: 5734:. 5697:. 5693:de 5662:. 5640:MR 5638:. 5628:. 5598:. 5590:. 5564:. 5536:. 5510:. 5487:OL 5485:. 5477:. 5439:. 5382:PM 5267:^ 5217:PM 5192:PM 5094:^ 5063:^ 4971:PM 4960:PM 4956:PM 4951:. 4945:PM 4940:. 4934:PM 4926:PM 4921:PM 4908:. 4900:, 4892:, 4870:. 4864:MR 4862:. 4852:. 4827:. 4819:. 4809:. 4780:. 4772:. 4762:. 4733:. 4725:. 4715:. 4688:. 4680:. 4653:. 4645:. 4618:. 4610:. 4600:. 4354:. 4342:PM 4320:: 4318:PM 4292:∧ 4277:PM 4248:PM 4138:). 4082:PM 4072:(φ 4066:PM 4060:". 4052:= 3982:PM 3954:PM 3909:PM 3891:PM 3881:(ψ 3848:≡ 3844:) 3840:(ψ 3832:(φ 3819:PM 3815:PM 3805:PM 3780:) 3776:(φ 3768:) 3764:(φ 3760:ε 3747:PM 3741:(φ 3735:PM 3731:PM 3723:PM 3687:PM 3662:(φ 3646:PM 3623:PM 3582:PM 3554:Df 3549:= 3514:) 3493:PM 3467:: 3461:. 3428:Df 3420:φ 3416:⊃ 3406:φ 3391:= 3387:. 3380:: 3378:PM 3318:PM 3307:✱1 3303:PM 3299:Pp 3292:; 3290:Pp 3244:PM 3233:PM 3225:PM 3156:PM 3133:Df 3071:Df 2981:Df 2976:~φ 2972:) 2968:~( 2964:= 2927:) 2885:) 2875:PM 2871:PM 2855:) 2836:) 2823:, 2808:) 2798:PM 2796:. 2790:PM 2764:) 2745:) 2741:"( 2719:PM 2717:: 2701:✱8 2695:| 2671:| 2628:s 2623:PM 2603:✱8 2599:✱8 2595:✱9 2591:PM 2563:→ 2555:→ 2539:→ 2531:→ 2525:df 2519:→ 2515:→ 2500:)) 2490:df 2484:∧ 2472:)) 2462:df 2444:)) 2434:df 2401:. 2399:Df 2394:⊃ 2384:⊃ 2370:⊃ 2366:⊃ 2362:. 2333:. 2331:Df 2329:) 2304:. 2295:PM 2260::: 2256::. 2235:)) 2128:⊃ 2112:⊃ 2108:q 2083:⊃ 2079:q 2075:p 2050::: 2046::. 2030:PM 2012:PM 2003:"⊦ 1997:PM 1984:: 1976:PM 1966:PM 1939:PM 1933:⊃ 1929:⊃ 1856:,σ 1836:|σ 1768:|σ 1727:,σ 1697:|σ 1677:,σ 1657:,σ 1637:,σ 1620:. 1556:. 1550:PM 1531:|( 1519:, 1515:, 1490:PM 1476:| 1451:✱9 1447:✱9 1441:Pp 1416:Pp 1410:∨ 1391:Pp 1373:Pp 1371:. 1367:∨ 1353:∨ 1339:⊃ 1334::. 1324:Pp 1318:∨ 1303:) 1299:∨ 1280:Pp 1278:. 1274:∨ 1260:∨ 1245:Pp 1243:. 1239:∨ 1214:Pp 1212:. 1198:∨ 1176:Pp 1168:. 1166:Df 1164:. 1160:∨ 1156:~ 1145:⊃ 1141:. 1115:∨ 1026:PM 950:∨ 923:PM 903:⊃ 883:PM 881:: 873:PM 848:⊃⊦ 798:PM 778:". 762:PM 756:⊃ 752:( 748:) 744:⊃ 740:( 729:≡ 716:PM 708:PM 702:⊃ 698:( 694:) 690:⊃ 682:≡ 674:: 666:PM 662:Df 660:) 630:PM 626:Df 621:∨ 617:~ 606:⊃ 574:PM 566:PM 561:PM 518:B 516:| 512:⊃ 508:, 421:: 389:: 370:PM 332:PM 330:: 310:PM 269:, 265:, 247:PM 239:PM 235:. 233:PM 229:PM 220:. 200:, 194:PM 184:PM 174:PM 172:. 162:✱9 137:PM 8542:· 8526:) 8522:( 8489:) 8378:) 8131:e 8124:t 8117:v 8035:/ 7950:P 7705:) 7491:) 7487:( 7384:∀ 7379:! 7374:∃ 7335:= 7330:↔ 7325:→ 7320:∧ 7315:∨ 7310:¬ 7033:/ 7029:/ 7003:/ 6814:) 6810:( 6697:∞ 6687:3 6475:) 6373:e 6366:t 6359:v 6215:e 6208:t 6201:v 5817:e 5810:t 5803:v 5790:) 5744:. 5718:. 5672:. 5646:. 5606:. 5574:. 5546:. 5520:. 5493:. 5449:. 5369:ŷ 5365:x 5354:. 5322:. 5113:. 5088:. 5057:. 5055:1 4878:. 4848:: 4835:. 4803:: 4788:. 4756:: 4741:. 4709:: 4696:. 4674:: 4661:. 4639:: 4626:. 4604:: 4538:. 4536:ω 4513:x 4509:x 4334:n 4330:n 4303:n 4301:x 4296:2 4294:x 4289:1 4287:x 4214:G 4210:G 4202:G 4198:G 4155:ω 4078:ẑ 4074:z 4070:ẑ 4058:ẑ 4056:ψ 4054:. 4050:ẑ 4048:φ 4046:. 4044:) 4042:x 4040:( 4038:. 4036:⊃ 4034:. 4031:x 4029:ψ 4026:x 4023:≡ 4021:x 4019:φ 4014:x 4010:p 4006:x 4002:x 3998:x 3990:ẑ 3978:ẑ 3974:ẑ 3970:x 3962:x 3950:ẑ 3946:ẑ 3942:: 3940:) 3938:x 3936:( 3934:. 3932:⊃ 3930:. 3927:x 3925:ψ 3922:x 3919:≡ 3917:x 3915:φ 3887:ẑ 3883:z 3879:ẑ 3873:x 3871:ψ 3869:. 3867:≡ 3865:. 3862:x 3860:φ 3858:: 3856:) 3854:x 3852:( 3850:: 3846:. 3842:z 3838:ẑ 3834:z 3830:ẑ 3801:x 3797:ẑ 3793:x 3789:ẑ 3785:x 3778:x 3774:. 3772:≡ 3770:. 3766:z 3762:ẑ 3758:x 3755:: 3753:⊢ 3743:z 3739:ẑ 3683:x 3679:x 3675:z 3672:! 3668:ẑ 3664:z 3660:ẑ 3653:x 3578:y 3574:ŷ 3570:ŷ 3566:y 3556:. 3551:b 3547:y 3544:. 3540:y 3537:≡ 3535:. 3532:y 3530:φ 3528:: 3526:) 3524:b 3520:: 3518:= 3516:. 3512:y 3508:y 3504:! 3485:ŷ 3481:ŷ 3477:y 3451:y 3447:x 3443:y 3439:x 3425:y 3422:! 3418:. 3414:. 3411:x 3408:! 3404:: 3400:: 3398:= 3396:. 3393:y 3389:x 3368:x 3364:f 3360:x 3356:x 3352:f 3348:x 3344:x 3340:f 3336:x 3332:f 3324:. 3287:x 3284:! 3281:f 3278:. 3274:x 3271:≡ 3269:. 3266:x 3264:φ 3262:: 3260:) 3258:f 3254:: 3252:⊢ 3218:ŷ 3214:y 3210:x 3207:! 3174:y 3168:x 3147:x 3143:x 3139:x 3130:x 3126:x 3124:φ 3122:. 3120:) 3118:x 3116:( 3114:. 3112:= 3110:. 3107:x 3105:ψ 3102:x 3099:≡ 3097:x 3095:φ 3085:x 3081:x 3077:x 3068:x 3064:x 3062:φ 3060:. 3058:) 3056:x 3054:( 3052:. 3050:= 3048:. 3045:x 3043:ψ 3040:x 3037:⊃ 3035:x 3033:φ 3024:x 3011:x 3005:x 2997:x 2993:x 2989:x 2983:. 2978:x 2974:. 2970:x 2966:. 2962:. 2959:x 2957:φ 2955:. 2953:) 2951:x 2937:x 2933:x 2931:φ 2929:. 2925:x 2923:( 2921:: 2919:⊃ 2917:: 2914:x 2910:x 2908:ψ 2906:. 2904:) 2902:x 2900:( 2898:: 2895:x 2891:x 2889:φ 2887:. 2883:x 2881:( 2861:x 2859:χ 2857:. 2853:x 2851:( 2842:x 2840:φ 2838:. 2834:x 2832:( 2825:x 2821:x 2814:x 2812:ψ 2810:. 2806:x 2804:( 2794:x 2774:x 2770:x 2768:φ 2766:. 2762:x 2755:x 2751:x 2749:φ 2747:. 2743:x 2735:x 2731:x 2727:x 2723:x 2697:q 2693:p 2689:q 2685:p 2681:q 2677:p 2673:q 2669:p 2665:q 2661:p 2609:: 2569:r 2565:q 2561:p 2557:r 2553:q 2549:p 2543:) 2541:r 2537:q 2533:q 2529:p 2527:( 2521:r 2517:q 2513:p 2511:( 2498:q 2494:p 2486:q 2482:p 2480:( 2470:q 2466:p 2458:q 2454:p 2452:( 2442:q 2438:p 2430:q 2426:p 2424:( 2396:r 2392:q 2389:. 2386:q 2382:p 2379:. 2377:= 2375:. 2372:r 2368:q 2364:p 2354:. 2352:q 2348:p 2344:q 2341:. 2338:p 2327:q 2323:p 2319:. 2317:= 2315:. 2312:q 2309:. 2306:p 2288:x 2284:x 2280:p 2278:( 2276:f 2252:: 2233:r 2231:⊃ 2229:p 2225:r 2223:⊃ 2221:q 2217:q 2215:⊃ 2213:p 2211:( 2202:r 2200:⊃ 2198:p 2194:r 2192:⊃ 2190:q 2188:: 2186:q 2184:⊃ 2182:p 2143:. 2130:. 2126:. 2114:. 2110:. 2106:. 2085:. 2081:. 2077:. 2073:: 2067:✱ 2058:x 2054:x 2042:: 2038:. 2036:" 2008:p 2005:. 1994:p 1935:r 1931:q 1927:p 1923:r 1919:q 1915:p 1913:" 1873:i 1868:n 1863:n 1858:1 1853:m 1848:1 1843:n 1838:1 1833:m 1828:1 1823:m 1818:1 1813:m 1808:1 1803:m 1798:1 1796:τ 1785:m 1780:1 1775:n 1770:1 1765:m 1760:1 1749:n 1744:n 1739:1 1734:n 1729:1 1724:m 1719:1 1714:m 1709:1 1704:n 1699:1 1694:m 1689:1 1684:n 1679:1 1674:m 1669:1 1664:n 1659:1 1654:m 1649:1 1644:n 1639:1 1634:m 1629:1 1613:m 1608:1 1603:m 1598:1 1593:m 1588:1 1583:m 1578:1 1541:r 1537:r 1535:| 1533:q 1529:p 1525:p 1521:r 1517:q 1513:p 1494:. 1478:q 1474:p 1470:q 1466:p 1437:p 1433:p 1429:p 1425:p 1412:q 1408:p 1404:q 1400:p 1387:p 1383:p 1369:r 1365:p 1362:. 1360:⊃ 1358:. 1355:q 1351:p 1348:: 1346:⊃ 1344:. 1341:r 1337:q 1320:r 1316:p 1312:q 1309:. 1307:⊃ 1305:. 1301:r 1297:q 1293:p 1290:: 1276:p 1272:q 1269:. 1267:⊃ 1265:. 1262:q 1258:p 1255:: 1241:q 1237:p 1234:. 1232:⊃ 1230:. 1227:q 1224:: 1210:p 1207:. 1205:⊃ 1203:. 1200:p 1196:p 1193:: 1181:( 1162:q 1158:p 1154:. 1152:= 1150:. 1147:q 1143:p 1117:q 1113:p 1109:q 1105:p 1101:q 1097:p 1093:q 1089:p 1078:p 1074:p 1070:p 1066:p 1057:. 1043:. 1036:. 952:q 948:p 944:p 919:q 916:. 912:q 909:. 905:q 901:p 897:p 894:. 869:q 865:p 861:q 857:p 853:q 850:. 846:. 843:p 840:. 836:q 832:p 828:q 825:. 823:⊃ 821:. 818:p 815:: 811:p 808:. 776:x 772:x 758:p 754:q 750:. 746:q 742:p 738:. 736:= 734:. 731:q 727:p 724:: 704:p 700:q 696:. 692:q 688:p 684:q 680:p 658:q 654:p 650:. 648:= 646:. 643:q 640:. 637:p 623:q 619:p 615:. 613:= 611:. 608:q 604:p 548:B 544:B 540:B 536:A 532:A 527:B 523:A 514:B 510:A 506:A 454:c 450:b 446:a 444:" 34:. 20:)

Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.

Knowledge

Principia Mathematica

Index