Propositional formula

767:

whatever else is in the door's circuitry. Inspection of the circuit (either the diagram or the actual objects themselves—door, switches, wires, circuit board, etc.) might reveal that, on the circuit board "node 22" goes to +0 volts when the contacts of switch "SW_D" are mechanically in contact ("closed") and the door is in the "down" position (95% down), and "node 29" goes to +0 volts when the door is 95% UP and the contacts of switch SW_U are in mechanical contact ("closed"). The engineer must define the meanings of these voltages and all possible combinations (all 4 of them), including the "bad" ones (e.g. both nodes 22 and 29 at 0 volts, meaning that the door is open and closed at the same time). The circuit mindlessly responds to whatever voltages it experiences without any awareness of TRUTH or FALSEHOOD, RIGHT or WRONG, SAFE or DANGEROUS.

7774:, and the number terms also will be reduced in the process. Two abutting squares (2 x 1 horizontal or 1 x 2 vertical, even the edges represent abutting squares) lose one literal, four squares in a 4 x 1 rectangle (horizontal or vertical) or 2 x 2 square (even the four corners represent abutting squares) lose two literals, eight squares in a rectangle lose 3 literals, etc. (One seeks out the largest square or rectangles and ignores the smaller squares or rectangles contained totally within it. ) This process continues until all abutting squares are accounted for, at which point the propositional formula is minimized. 13307: 1373: 8820: 218:: "This pig has wings" AND "This pig is blue", whose internal structure is not considered. In contrast, in the predicate calculus, the first sentence breaks into "this pig" as the subject, and "has wings" as the predicate. Thus it asserts that object "this pig" is a member of the class (set, collection) of "winged things". The second sentence asserts that object "this pig" has an attribute "blue" and thus is a member of the class of "blue things". One might choose to write the two sentences connected with AND as: 5650: 9003: 144:(utterances, sentences, assertions) are considered to be either simple or compound. Compound propositions are considered to be linked by sentential connectives, some of the most common of which are "AND", "OR", "IF ... THEN ...", "NEITHER ... NOR ...", "... IS EQUIVALENT TO ..." . The linking semicolon ";", and connective "BUT" are considered to be expressions of "AND". A sequence of discrete sentences are considered to be linked by "AND"s, and formal analysis applies a 9024: 11553: 751:, engineers prefer to pull known objects from a small library—objects that have well-defined, predictable behaviors even in large combinations, (hence their name for the propositional calculus: "combinatorial logic"). The fewest behaviors of a single object are two (e.g. { OFF, ON }, { open, shut }, { UP, DOWN } etc.), and these are put in correspondence with { 0, 1 }. Such elements are called 8666:—that is, when an object m has a property P, but the object m is defined in terms of property P. The best advice for a rhetorician or one involved in deductive analysis is avoid impredicative definitions but at the same time be on the lookout for them because they can indeed create paradoxes. Engineers, on the other hand, put them to work in the form of propositional formulas with feedback. 276: 10624:"Boole's principal single innovation was law for logic: it stated that the mental acts of choosing the property x and choosing x again and again is the same as choosing x once... As consequence of it he formed the equations x•(1-x)=0 and x+(1-x)=1 which for him expressed respectively the law of contradiction and the law of excluded middle" (p. xxviiff). For Boole "1" was the 11541:, John Wiley & Sons, Inc., New York. No ISBN. Library of Congress Catalog Card Number: 68-21185. Tight presentation of engineering's analysis and synthesis methods, references McCluskey 1965. Unlike Suppes, Wickes' presentation of "Boolean algebra" starts with a set of postulates of a truth-table nature and then derives the customary theorems of them (p. 18ff). 4341:

over the other connectives. To "well-form" a formula, start with the connective with the highest rank and add parentheses around its components, then move down in rank (paying close attention to the connective's scope over which it is working). From most- to least-senior, with the predicate signs ∀x and ∃x, the IDENTITY = and arithmetic signs added for completeness:

11531:(no year cited) brought to Russell's and Whitehead's attention that what they considered their primitive propositions (connectives) could be reduced to a single |, nowadays known as the "stroke" or NAND (NOT-AND, NEITHER ... NOR...). Russell-Whitehead discuss this in their "Introduction to the Second Edition" and makes the definitions as discussed above. 3150:∨ n) are constructed from strings of two-argument AND and OR and written in abbreviated form without the parentheses. These, and other connectives as well, can then be used as building blocks for yet further connectives. Rhetoricians, philosophers, and mathematicians use truth tables and the various theorems to analyze and simplify their formulas. 10570:

one after another for the presence or absence of the assertion—then the law is considered intuitionistically appropriate. Thus an assertion such as: "This object must either BE or NOT BE (in the collection)", or "This object must either have this QUALITY or NOT have this QUALITY (relative to the objects in the collection)" is acceptable. See more at

10655:(PM). It is here that what we consider "modern" propositional logic first appeared. In particular, PM introduces NOT and OR and the assertion symbol ⊦ as primitives. In terms of these notions they define IMPLICATION → ( def. *1.01: ~p ∨ q ), then AND (def. *3.01: ~(~p ∨ ~q) ), then EQUIVALENCE p ←→ q (*4.01: (p → q) & ( q → p ) ). 10934:: For large "gains" k, e.g. k=100, 1/( 1 + e ) = 1/( 1 + e ) = { ≃0, ≃1 }. For example, if "The door is DOWN" means "The door is less than 50% of the way up", then a threshold thr=0.5 corresponding to 0.5*5.0 = +2.50 volts could be applied to a "linear" measuring-device with an output of 0 volts when fully closed and +5.0 volts when fully open. 984:. The symbols used will vary from author to author and between fields of endeavor. In general the abbreviations "T" and "F" stand for the evaluations TRUTH and FALSITY applied to the variables in the propositional formula (e.g. the assertion: "That cow is blue" will have the truth-value "T" for Truth or "F" for Falsity, as the case may be.). 7754: 6610: 2853:). the result of such a calculus will be another formula (i.e. a well-formed symbol string). Eventually, however, if one wants to use the calculus to study notions of validity and truth, one must add axioms that define the behavior of the symbols called "the truth values" {T, F} ( or {1, 0}, etc.) relative to the other symbols. 10569:

The use of the word "everything" in the law of excluded middle renders Russell's expression of this law open to debate. If restricted to an expression about BEING or QUALITY with reference to a finite collection of objects (a finite "universe of discourse") -- the members of which can be investigated

9714:

The formula known as "clocked flip-flop" memory ("c" is the "clock" and "d" is the "data") is given below. It works as follows: When c = 0 the data d (either 0 or 1) cannot "get through" to affect output q. When c = 1 the data d "gets through" and output q "follows" d's value. When c goes from 1 to 0

5653:

The engineering symbol for the NAND connective (the 'stroke') can be used to build any propositional formula. The notion that truth (1) and falsity (0) can be defined in terms of this connective is shown in the sequence of NANDs on the left, and the derivations of the four evaluations of a NAND b are

4564:

The sign " = " (as distinguished from logical equivalence ≡, alternately ↔ or ⇔) symbolizes the assignment of value or meaning. Thus the string (a & ~(a)) symbolizes "0", i.e. it means the same thing as symbol "0" ". In some "systems" this will be an axiom (definition) perhaps shown as ( (a &

4324:

Enterprising readers might challenge themselves to invent an "axiomatic system" that uses the symbols { ∨, &, ~, (, ), variables a, b, c }, the formation rules specified above, and as few as possible of the laws listed below, and then derive as theorems the others as well as the truth-table

3954:

Example: The following truth table is De Morgan's law for the behavior of NOT over OR: ~(a ∨ b) ≡ (~a & ~b). To the left of the principal connective ≡ (yellow column labelled "taut") the formula ~(b ∨ a) evaluates to (1, 0, 0, 0) under the label "P". On the right of "taut" the formula

1738:

between them exhaustively and unambiguously. In the truth table below, d1 is the formula: ( (IF c THEN b) AND (IF NOT-c THEN a) ). Its fully reduced form d2 is the formula: ( (c AND b) OR (NOT-c AND a). The two formulas are equivalent as shown by the columns "=d1" and "=d2". Electrical engineers call

734:

seeing a blue cow—unless I am lying my statement is a TRUTH relative to the object of my (perhaps flawed) perception. But is the blue cow "really there"? What do you see when you look out the same window? In order to proceed with a verification, you will need a prior notion (a template) of both "cow"

8722:

In the abstract (ideal) case the simplest oscillating formula is a NOT fed back to itself: ~(~(p=q)) = q. Analysis of an abstract (ideal) propositional formula in a truth-table reveals an inconsistency for both p=1 and p=0 cases: When p=1, q=0, this cannot be because p=q; ditto for when p=0 and q=1.

7789:

Observe that by the Idempotency law (A ∨ A) = A, we can create more terms. Then by association and distributive laws the variables to disappear can be paired, and then "disappeared" with the Law of contradiction (x & ~x)=0. The following uses brackets only to keep track of the terms; they

7777:

For example, squares #3 and #7 abut. These two abutting squares can lose one literal (e.g. "p" from squares #3 and #7), four squares in a rectangle or square lose two literals, eight squares in a rectangle lose 3 literals, etc. (One seeks out the largest square or rectangles.) This process continues

6665:

In the same way that a 2-row truth table displays the evaluation of a propositional formula for all 2 possible values of its variables, n variables produces a 2-square Karnaugh map (even though we cannot draw it in its full-dimensional realization). For example, 3 variables produces 2 = 8 rows and 8

4912:

It can be shown that any expression matched by the grammar has a balanced number of left and right parentheses, and any nonempty initial segment of a formula has more left than right parentheses. This fact can be used to give an algorithm for parsing formulas. For example, suppose that an expression

4340:

In general, to avoid confusion during analysis and evaluation of propositional formulas, one can make liberal use of parentheses. However, quite often authors leave them out. To parse a complicated formula one first needs to know the seniority, or rank, that each of the connectives (excepting *) has

11203:

McCluskey comments that "it could be argued that the analysis is still incomplete because the word statement "The outputs are equal to the previous values of the inputs" has not been obtained"; he goes on to dismiss such worries because "English is not a formal language in a mathematical sense, it

11070:

cf Minsky 1967:75, section 4.2.3 "The method of parenthesis counting". Minsky presents a state machine that will do the job, and by use of induction (recursive definition) Minsky proves the "method" and presents a theorem as the result. A fully generalized "parenthesis grammar" requires an infinite

9239:

the output q=1 so when and if (s=0 & r=1) the flip-flop will be reset. Or, if (s=1 & r=0) the flip-flop will be set. In the abstract (ideal) instance in which s=1 ⇒ s=0 & r=1 ⇒ r=0 simultaneously, the formula q will be indeterminate (undecidable). Due to delays in "real" OR, AND and NOT

247:

are treated by the predicate calculus. Along with the new function symbolism "F(x)" two new symbols are introduced: ∀ (For all), and ∃ (There exists ..., At least one of ... exists, etc.). The predicate calculus, but not the propositional calculus, can establish the formal validity of the following

173:

must be about specific objects or specific states of mind. Each must have at least a subject (an immediate object of thought or observation), a verb (in the active voice and present tense preferred), and perhaps an adjective or adverb. "Dog!" probably implies "I see a dog" but should be rejected as

9057:

About the simplest memory results when the output of an OR feeds back to one of its inputs, in this case output "q" feeds back into "p". Given that the formula is first evaluated (initialized) with p=0 & q=0, it will "flip" once when "set" by s=1. Thereafter, output "q" will sustain "q" in the

9044:

at the input and q at the output. After "breaking" the feed-back, the truth table construction proceeds in the conventional manner. But afterwards, in every row the output q is compared to the now-independent input p and any inconsistencies between p and q are noted (i.e. p=0 together with q=1, or

6613:

A truth table will contain 2 rows, where n is the number of variables (e.g. three variables "p", "d", "c" produce 2 rows). Each row represents a minterm. Each minterm can be found on the Hasse diagram, on the Veitch diagram, and on the Karnaugh map. (The evaluations of "p" shown in the truth table

5304:

in arguments, but arguments reduce to propositional formulas and can be evaluated the same as any other propositional formula. Here a valid inference means: "The formula that represents the inference evaluates to "truth" beneath its principal connective, no matter what truth-values are assigned to

9027:

A "clocked flip-flop" memory ("c" is the "clock" and "d" is the "data"). The data can change at any time when clock c=0; when clock c=1 the output q "tracks" the value of data d. When c goes from 1 to 0 it "traps" d = q's value and this continues to appear at q no matter what d does (as long as c

8836:

Analysis requires a delay to be inserted and then the loop cut between the delay and the input "p". The delay must be viewed as a kind of proposition that has "qd" (q-delayed) as output for "q" as input. This new proposition adds another column to the truth table. The inconsistency is now between

7761:

Use the values of the formula (e.g. "p") found by the truth-table method and place them in their into their respective (associated) Karnaugh squares (these are numbered per the Gray code convention). If values of "d" for "don't care" appear in the table, this adds flexibility during the reduction

328:

An algebra (and there are many different ones), loosely defined, is a method by which a collection of symbols called variables together with some other symbols such as parentheses (, ) and some sub-set of symbols such as *, +, ~, &, ∨, =, ≡, ∧, ￢ are manipulated within a system of

11111:

Wickes 1967:36ff. Wickes offers a good example of 8 of the 2 x 4 (3-variable maps) and 16 of the 4 x 4 (4-variable) maps. As an arbitrary 3-variable map could represent any one of 2=256 2x4 maps, and an arbitrary 4-variable map could represent any one of 2 = 65,536 different formula-evaluations,

1658:

and is the connective responsible for conditional goto's (jumps, branches). From this one connective all other connectives can be constructed (see more below). Although " IF c THEN b ELSE a " sounds like an implication it is, in its most reduced form, a switch that makes a decision and offers as

8678:

The simplest case occurs when an OR formula becomes one its own inputs e.g. p = q. Begin with (p ∨ s) = q, then let p = q. Observe that q's "definition" depends on itself "q" as well as on "s" and the OR connective; this definition of q is thus impredicative. Either of two conditions can

8674:

The notion of a propositional formula appearing as one of its own variables requires a formation rule that allows the assignment of the formula to a variable. In general there is no stipulation (either axiomatic or truth-table systems of objects and relations) that forbids this from happening.

3944:

The following "laws" of the propositional calculus are used to "reduce" complex formulas. The "laws" can be verified easily with truth tables. For each law, the principal (outermost) connective is associated with logical equivalence ≡ or identity =. A complete analysis of all 2 combinations of

3149:

As shown above, the CASE (IF c THEN b ELSE a ) connective is constructed either from the 2-argument connectives IF ... THEN ... and AND or from OR and AND and the 1-argument NOT. Connectives such as the n-argument AND (a & b & c & ... & n), OR (a ∨ b ∨ c ∨ ...

261:

Tarski asserts that the notion of IDENTITY (as distinguished from LOGICAL EQUIVALENCE) lies outside the propositional calculus; however, he notes that if a logic is to be of use for mathematics and the sciences it must contain a "theory" of IDENTITY. Some authors refer to "predicate logic with

8690:

of the inputs alone. That is, sometimes one looks at q and sees 0 and other times 1. To avoid this problem one has to know the state (condition) of the "hidden" variable p inside the box (i.e. the value of q fed back and assigned to p). When this is known the apparent inconsistency goes away.

766:

Thus an assignment of meaning of the variables and the two value-symbols { 0, 1 } comes from "outside" the formula that represents the behavior of the (usually) compound object. An example is a garage door with two "limit switches", one for UP labelled SW_U and one for DOWN labelled SW_D, and

9006:

About the simplest memory results when the output of an OR feeds back to one of its inputs, in this case output "q" feeding back into "p". The next simplest is the "flip-flop" shown below the once-flip. Analysis of these sorts of formulas can be done by either cutting the feedback path(s) or

3955:(~(b) ∨ ~(a)) also evaluates to (1, 0, 0, 0) under the label "Q". As the two columns have equivalent evaluations, the logical equivalence ≡ under "taut" evaluates to (1, 1, 1, 1), i.e. P ≡ Q. Thus either formula can be substituted for the other if it appears in a larger formula. 2833:

As noted above, Tarski considers IDENTITY to lie outside the propositional calculus, but he asserts that without the notion, "logic" is insufficient for mathematics and the deductive sciences. In fact the sign comes into the propositional calculus when a formula is to be evaluated.

10885:

Tarski p.54-68. Suppes calls IDENTITY a "further rule of inference" and has a brief development around it; Robbin, Bender and Williamson, and Goodstein introduce the sign and its usage without comment or explanation. Hamilton p. 37 employs two signs ≠ and = with respect to the

4973:— the connective under which the overall evaluation of the formula occurs for the outer-most parentheses (which are often omitted). It also locates the inner-most connective where one would begin evaluatation of the formula without the use of a truth table, e.g. at "level 6". 3949:

distinct variables will result in a column of 1's (T's) underneath this connective. This finding makes each law, by definition, a tautology. And, for a given law, because its formula on the left and right are equivalent (or identical) they can be substituted for one another.

9234:

shown below the once-flip. Given that r=0 & s=0 and q=0 at the outset, it is "set" (s=1) in a manner similar to the once-flip. It however has a provision to "reset" q=0 when "r"=1. And additional complication occurs if both set=1 and reset=1. In this formula, the set=1

8698:. Propositional formulas with feedback lead, in their simplest form, to state machines; they also lead to memories in the form of Turing tapes and counter-machine counters. From combinations of these elements one can build any sort of bounded computational model (e.g. 5329:

Example 1: What does one make of the following difficult-to-follow assertion? Is it valid? "If it's sunny, but if the frog is croaking then it's not sunny, then it's the same as saying that the frog isn't croaking." Convert this to a propositional formula as follows:

344:

When the values are restricted to just two and applied to the notion of simple sentences (e.g. spoken utterances or written assertions) linked by propositional connectives this whole algebraic system of symbols and rules and evaluation-methods is usually called the

10957:

peculiar; in fact (a "+" b) = (a + (b - a*b)) where "+" is the "logical sum" but + and - are the true arithmetic counterparts. Occasionally all four notions do appear in a formula: A AND B = 1/2*( A plus B minus ( A XOR B ) ] (cf p. 146 in John Wakerly 1978,

1380:

In general, the engineering connectives are just the same as the mathematics connectives excepting they tend to evaluate with "1" = "T" and "0" = "F". This is done for the purposes of analysis/minimization and synthesis of formulas by use of the notion of

6644:. A string of literals connected by ANDs is called a term. A string of literals connected by OR is called an alterm. Typically the literal ~(x) is abbreviated ~x. Sometimes the &-symbol is omitted altogether in the manner of algebraic multiplication. 329:

rules. These symbols, and well-formed strings of them, are said to represent objects, but in a specific algebraic system these objects do not have meanings. Thus work inside the algebra becomes an exercise in obeying certain laws (rules) of the algebra's

3172:

is following the convention of Reichenbach. Some examples of convenient definitions drawn from the symbol set { ~, &, (, ) } and variables. Each definition is producing a logically equivalent formula that can be used for substitution or replacement.

2803:

equivalence sometimes appears in speech as in this example: " 'The sun is shining' means 'I'm biking' " Translated into a propositional formula the words become: "IF 'the sun is shining' THEN 'I'm biking', AND IF 'I'm biking' THEN 'the sun is shining'":

8642:

Then assign the variable "s" to the left-most sentence "This sentence is simple". Define "compound" c = "not simple" ~s, and assign c = ~s to "This sentence is compound"; assign "j" to "It is conjoined by AND". The second sentence can be expressed as:

6078:

In the following truth table the column labelled "taut" for tautology evaluates logical equivalence (symbolized here by ≡) between the two columns labelled d. Because all four rows under "taut" are 1's, the equivalence indeed represents a tautology.

6731:

When working with Karnaugh maps one must always keep in mind that the top edge "wrap arounds" to the bottom edge, and the left edge wraps around to the right edge—the Karnaugh diagram is really a three- or four- or n-dimensional flattened object.

340:

For a well-formed sequence of symbols in the algebra —a formula— to have some usefulness outside the algebra the symbols are assigned meanings and eventually the variables are assigned values; then by a series of rules the formula is evaluated.

3153:

Electrical engineering uses drawn symbols and connect them with lines that stand for the mathematicals act of substitution and replacement. They then verify their drawings with truth tables and simplify the expressions as shown below by use of

8833:. If either of the delay and NOT are not abstract (i.e. not ideal), the type of analysis to be used will be dependent upon the exact nature of the objects that make up the oscillator; such things fall outside mathematics and into engineering. 2821:

Different authors use different signs for logical equivalence: ↔ (e.g. Suppes, Goodstein, Hamilton), ≡ (e.g. Robbin), ⇔ (e.g. Bender and Williamson). Typically identity is written as the equals sign =. One exception to this rule is found in

3158:

or the theorems. In this way engineers have created a host of "combinatorial logic" (i.e. connectives without feedback) such as "decoders", "encoders", "mutifunction gates", "majority logic", "binary adders", "arithmetic logic units", etc.

691:

Evaluation of a propositional formula begins with assignment of a truth value to each variable. Because each variable represents a simple sentence, the truth values are being applied to the "truth" or "falsity" of these simple sentences.

156:

For example: The assertion: "This cow is blue. That horse is orange but this horse here is purple." is actually a compound proposition linked by "AND"s: ( ("This cow is blue" AND "that horse is orange") AND "this horse here is purple" )

1708:

Thus IF ... THEN ... ELSE—unlike implication—does not evaluate to an ambiguous "TRUTH" when the first proposition is false i.e. c = F in (c → b). For example, most people would reject the following compound proposition as a nonsensical

4332:, that is, they stand in place of an infinite number of instances. Thus ( x ∨ y ) ≡ ( y ∨ x ) might be used in one instance, ( p ∨ 0 ) ≡ ( 0 ∨ p ) and in another instance ( 1 ∨ q ) ≡ ( q ∨ 1 ), etc. 11347:. Emphasis on the notion of "algebra of classes" with set-theoretic symbols such as ∩, ∪, ' (NOT), ⊂ (IMPLIES). Later Goldstein replaces these with &, ∨, ￢, → (respectively) in his treatment of "Sentence Logic" pp. 76–93. 10943:

In actuality the digital 1 and 0 are defined over non-overlapping ranges e.g. { "1" = +5/+0.2/−1.0 volts, 0 = +0.5/−0.2 volts }. When a value falls outside the defined range(s) the value becomes "u" -- unknown; e.g. +2.3 would be

11226:

The notion of delay and the principle of local causation as caused ultimately by the speed of light appears in Robin Gandy (1980), "Church's thesis and Principles for Mechanisms", in J. Barwise, H. J. Keisler and K. Kunen, eds.,

11129:

and Kleene believed that the classical paradoxes are uniformly examples of this sort of definition. But Kleene went on to assert that the problem has not been solved satisfactorily and impredicative definitions can be found in

1721:

Example: The proposition " IF 'Winston Churchill was Chinese' THEN 'The sun rises in the east' " evaluates as a TRUTH given that 'Winston Churchill was Chinese' is a FALSEHOOD and 'The sun rises in the east' evaluates as a

11231:, North-Holland Publishing Company (1980) 123-148. Gandy considered this to be the most important of his principles: "Contemporary physics rejects the possibility of instantaneous action at a distance" (p. 135). Gandy was 4450:

d & c ∨ p & ~(c & ~d) ≡ c & d ∨ p & c ∨ p & ~d rewritten is ( ( (d & c) ∨ ( p & ~((c & ~(d)) ) ) ) ≡ ( (c & d) ∨ (p & c) ∨ (p & ~(d)) )

6618:

Reduction to normal form is relatively simple once a truth table for the formula is prepared. But further attempts to minimize the number of literals (see below) requires some tools: reduction by De Morgan's laws and

4494:( (c & d) ∨ (p & c) ∨ (p & ~d) ) above should be written ( ((c & d) ∨ (p & c)) ∨ (p & ~(d) ) ) or possibly ( (c & d) ∨ ( (p & c) ∨ (p & ~(d)) ) ) 11031:

Hamilton p. 37. Bender and Williamson p. 29 state "In what follows, we'll replace "equals" with the symbol " ⇔ " (equivalence) which is usually used in logic. We use the more familiar " = " for assigning meaning and

1733:

The use of the IF ... THEN ... ELSE construction avoids controversy because it offers a completely deterministic choice between two stated alternatives; it offers two "objects" (the two alternatives b and a), and it

5658:

A set of logical connectives is called complete if every propositional formula is tautologically equivalent to a formula with just the connectives in that set. There are many complete sets of connectives, including

9032:

Without delay, inconsistencies must be eliminated from a truth table analysis. With the notion of "delay", this condition presents itself as a momentary inconsistency between the fed-back output variable q and p =

3237:

but shown (for illustrative purposes) with specific letters a, b, c for the variables, whereas any variable letters can go in their places as long as the letter substitutions follow the rule of substitution below.

3167:

A definition creates a new symbol and its behavior, often for the purposes of abbreviation. Once the definition is presented, either form of the equivalent symbol or formula can be used. The following symbolism

724:, meanings (pattern-matching templates) must first be applied to the words, and then these meaning-templates must be matched against whatever it is that is being asserted. For example, my utterance "That cow is 6627:

are very suitable a small number of variables (5 or less). Some sophisticated tabular methods exist for more complex circuits with multiple outputs but these are beyond the scope of this article; for more see

6918:

by converting the circles to abutting squares, and Karnaugh simplified the Veitch diagram by converting the minterms, written in their literal-form (e.g. ~abc~d) into numbers. The method proceeds as follows:

231:"winged things", p is either found to be a member of this domain or not. Thus there is a relationship W (wingedness) between p (pig) and { T, F }, W(p) evaluates to { T, F } where { T, F } is the set of the 6680:

In the following table, observe the peculiar numbering of the rows: (0, 1, 3, 2, 6, 7, 5, 4, 0). The first column is the decimal equivalent of the binary equivalent of the digits "cba", in other words:

1376:

Engineering symbols have varied over the years, but these are commonplace. Sometimes they appear simply as boxes with symbols in them. "a" and "b" are called "the inputs" and "c" is called "the output".

11022:

The use of quote marks around the expressions is not accidental. Tarski comments on the use of quotes in his "18. Identity of things and identity of their designations; use of quotation marks" p. 58ff.

11244:

McKlusky p. 194-5 discusses "breaking the loop" and inserts "amplifiers" to do this; Wickes (p. 118-121) discuss inserting delays. McCluskey p. 195ff discusses the problem of "races" caused by delays.

3423: 4770:

A key property of formulas is that they can be uniquely parsed to determine the structure of the formula in terms of its propositional variables and logical connectives. When formulas are written in

235:"true" and "false". Likewise for B (blueness) and p (pig) and { T, F }: B(p) evaluates to { T, F }. So one now can analyze the connected assertions "B(p) AND W(p)" for its overall truth-value, i.e.: 4328:

If used in an axiomatic system, the symbols 1 and 0 (or T and F) are considered to be well-formed formulas and thus obey all the same rules as the variables. Thus the laws listed below are actually

227:

The generalization of "this pig" to a (potential) member of two classes "winged things" and "blue things" means that it has a truth-relationship with both of these classes. In other words, given a

10979:

A careful look at its Karnaugh map shows that IF...THEN...ELSE can also be expressed, in a rather round-about way, in terms of two exclusive-ORs: ( (b AND (c XOR a)) OR (a AND (c XOR b)) ) = d.

3616: 865: 3915: 6936:

has been reduced to its (unminimized) conjunctive normal form: each row has its minterm expression and these can be OR'd to produce the formula in its (unminimized) conjunctive normal form.

11217:

More precisely, given enough "loop gain", either oscillation or memory will occur (cf McCluskey p. 191-2). In abstract (idealized) mathematical systems adequate loop gain is not a problem.

3790: 3137:

or laws of identity and nullity. The choice of which ones to use, together with laws such as commutation and distribution, is up to the system's designer as long as the set of axioms is

10822:

Rosenbloom discusses this problem of implication at some length. Most philosophers and mathematicians just accept the material definition as given above. But some do not, including the

3704: 352:

While some of the familiar rules of arithmetic algebra continue to hold in the algebra of propositions (e.g. the commutative and associative laws for AND and OR), some do not (e.g. the

5960: 5347:? In other words, when evaluated will this yield a tautology (all T) beneath the logical-equivalence symbol ≡ ? The answer is NO, it is not valid. However, if reconstructed as an 3518: 3853: 5919: 3884: 11194:

and this makes its definition impredicative. Kleene asserts that attempts to argue this away can be used to uphold the impredicative definitions in the paradoxes.(Kleene 1952:43).

937: 210:(stringing together) of symbols) into a form with the following blank-subject structure " ___|predicate", and the predicate in turn generalized to all things with that property. 182:

For the purposes of the propositional calculus a compound proposition can usually be reworded into a series of simple sentences, although the result will probably sound stilted.

7781:

Example: The map method usually is done by inspection. The following example expands the algebraic method to show the "trick" behind the combining of terms on a Karnaugh map:

5689: 3032:

the value F (or a meaning of "F") to the entire expression. The definitions also serve as formation rules that allow substitution of a value previously derived into a formula:

2799:" is not the same thing as "identity". For example, most would agree that the assertion "That cow is blue" is identical to the assertion "That cow is blue". On the other hand, 759:. Whenever decisions must be made in an analog system, quite often an engineer will convert an analog behavior (the door is 45.32146% UP) to digital (e.g. DOWN=0 ) by use of a 206:(a verb or possibly verb-clause that asserts a quality or attribute of the object(s)). The predicate calculus then generalizes the "subject|predicate" form (where | symbolizes 5785: 5721: 969: 5753: 3462: 747:

Engineers try to avoid notions of truth and falsity that bedevil philosophers, but in the final analysis engineers must trust their measuring instruments. In their quest for

11505:(pbk.) Translation/reprints of Frege (1879), Russell's letter to Frege (1902) and Frege's letter to Russell (1902), Richard's paradox (1905), Post (1921) can be found here. 10930:

modelling offers a good mathematical model for a comparator as follows: Given a signal S and a threshold "thr", subtract "thr" from S and substitute this difference d to a

3323:( connected by ≡ or ↔) to the formula that replaces it, and (ii) unlike substitution its permissible for the replacement to occur only in one place (i.e. for one formula). 824: 3822: 9045:

p=1 and q=0); when the "line" is "remade" both are rendered impossible by the Law of contradiction ~(p & ~p)). Rows revealing inconsistencies are either considered

6720:

where each corner's variables change only one at a time as one moves around the edges of the cube. Hasse diagrams (hypercubes) flattened into two dimensions are either

3733: 3644:, left and right parentheses, and all the logical connectives under consideration. Each logical connective corresponds to a formula building operation, a function from 10890:

of a formula in a formal calculus. Kleene p. 70 and Hamilton p. 52 place it in the predicate calculus, in particular with regards to the arithmetic of natural numbers.

4938: 3538: 3482: 885: 801: 3558: 905: 10635:'s massive undertaking (1879) resulted in a formal calculus of propositions, but his symbolism is so daunting that it had little influence excepting on one person: 6673:

Any propositional formula can be reduced to the "logical sum" (OR) of the active (i.e. "1"- or "T"-valued) minterms. When in this form the formula is said to be in

6008: 5988: 5862: 5842: 3578: 6034:

Example: The following shows how a theorem-based proof of "(c, b, 1) ≡ (c → b)" would proceed, below the proof is its truth-table verification. ( Note: (c → b) is

2991:) define the equivalent of the truth tables for the ~ (NOT) and → (IMPLICATION) connectives of his system. The first one derives F ≠ T and T ≠ F, in other words " 3279:: The variable or sub-formula to be substituted with another variable, constant, or sub-formula must be replaced in all instances throughout the overall formula. 286: 11414:, Prentice-Hall, Inc, Englewood Cliffs, N.J.. No ISBN. Library of Congress Catalog Card Number 67-12342. Useful especially for computability, plus good sources. 10911:"held that every idea must either originate directly in sense experience or else be compounded of ideas thus originating"; quoted from Quine reprinted in 1996 4774:, as above, unique readability is ensured through an appropriate use of parentheses in the definition of formulas. Alternatively, formulas can be written in 9007:

inserting (ideal) delay in the path. A cut path and an assumption that no delay occurs anywhere in the "circuit" results in inconsistencies for some of the

6927:

Produce the formula's truth table. Number its rows using the binary-equivalents of the variables (usually just sequentially 0 through n-1) for n variables.

5803:(1927:xvii). Since it is complete on its own, all other connectives can be expressed using only the stroke. For example, where the symbol " ≡ " represents 11686: 6589:

An arbitrary propositional formula may have a very complicated structure. It is often convenient to work with formulas that have simpler forms, known as

5755:. There are two binary connectives that are complete on their own, corresponding to NAND and NOR, respectively. Some pairs are not complete, for example 4416:

Thus the formula can be parsed—but because NOT does not obey the distributive law, the parentheses around the inner formula (~c & ~d) is mandatory:

8651:

If truth values are to be placed on the sentences c = ~s and j, then all are clearly FALSEHOODS: e.g. "This sentence is complex" is a FALSEHOOD (it is

2808:"IF 's' THEN 'b' AND IF 'b' THEN 's' " is written as ((s → b) & (b → s)) or in an abbreviated form as (s ↔ b). As the rightmost symbol string is a 6654:

p, q, r, s are variables. (((p ∨ ~(q) ) ∨ r) ∨ ~(s) ) is an alterm. This can be abbreviated as (p ∨ ~q ∨ r ∨ ~s).

10672:(1921) develops the truth-table method of analysis in his "Introduction to a general theory of elementary propositions". He notes Nicod's stroke | . 11418: 6651:

a, b, c, d are variables. ((( a & ~(b) ) & ~(c)) & d) is a term. This can be abbreviated as (a & ~b & ~c & d), or a~b~cd.

12361: 10605:'s work (1827) resulted in the notion of "quantification of the predicate" (1827) (nowadays symbolized as ∀ ≡ "for all"). A "row" instigated by 297: 9011:(combination of inputs and outputs, e.g. (p=0, s=1, r=1) results in an inconsistency). When delay is present these inconsistencies are merely 987:

The connectives go by a number of different word-usages, e.g. "a IMPLIES b" is also said "IF a THEN b". Some of these are shown in the table.

11402:

and developed some notable theorems with Quine and on his own. For those interested in the history, the book contains a wealth of references.

8829:: If a delay (ideal or non-ideal) is inserted in the abstract formula between p and q then p will oscillate between 1 and 0: 101010...101... 6677:. But even though it is in this form, it is not necessarily minimized with respect to either the number of terms or the number of literals. 12444: 11585: 7785:

Minterms #3 and #7 abut, #7 and #6 abut, and #4 and #6 abut (because the table's edges wrap around). So each of these pairs can be reduced.

5376:( ((a) → (b)) & (b) → (a) ) is well formed, but an invalid argument as shown by the red evaluation under the principal implication: 2849:, ... } and formula-formation rules (rules about how to make more symbol strings from previous strings by use of e.g. substitution and 2837:

In some systems there are no truth tables, but rather just formal axioms (e.g. strings of symbols from a set { ~, →, (, ), variables p

392:

they have designed using synthesis techniques and then apply various reduction and minimization techniques to simplify their designs.

10581:

applied to propositions had to wait until the early 19th century. In an (adverse) reaction to the 2000 year tradition of Aristotle's

10675:

Whitehead and Russell add an introduction to their 1927 re-publication of PM adding, in part, a favorable treatment of the "stroke".

4490:: The connectives are considered to be unary (one-variable, e.g. NOT) and binary (i.e. two-variable AND, OR, IMPLIES). For example: 11089:

cf Reichenbach p. 68 for a more involved discussion: "If the inference is valid and the premises are true, the inference is called

11049:

and is not a formal symbol with the following meaning: "by symbol ' s ' is to have the same meaning as the formula '(c & d)' ".

8686:. Without knowledge of what is going on "inside" the formula-"box" from the outside it would appear that the output is no longer a 951:

The "theory-extension" connective EQUALS (alternately, IDENTITY, or the sign " = " as distinguished from the "logical connective"

12758: 4508:

would appear. When the NOT is over a formula with more than one symbol, then the parentheses are mandatory, e.g. ~(a ∨ b).

4325:

valuations for ∨, &, and ~. One set attributed to Huntington (1904) (Suppes:204) uses eight of the laws defined below.

11557: 3384: 6708:

This numbering comes about because as one moves down the table from row to row only one variable at a time changes its value.

4516:

OR distributes over AND and AND distributes over OR. NOT does not distribute over AND or OR. See below about De Morgan's law:

3283:

Example: (c & d) ∨ (p & ~(c & ~d)), but (q1 & ~q2) ≡ d. Now wherever variable "d" occurs, substitute (q

12916: 11364: 10643:

he studied Frege's work and suggested a (famous and notorious) emendation with respect to it (1904) around the problem of an

6957:

However, this formula be reduced both in the number of terms (from 4 to 3) and in the total count of its literals (12 to 6).

403:

should behave given the addition of variables "b" and "a" and "carry_in" "ci", and the results "carry_out" "co" and "sum" Σ:

11704: 11398:, McGraw-Hill Book Company, New York. No ISBN. Library of Congress Catalog Card Number 65-17394. McCluskey was a student of 9715:

the last value of the data remains "trapped" at output "q". As long as c=0, d can change value without causing q to change.

12771: 12094: 178:

Example: "That purple dog is running", "This cow is blue", "Switch M31 is closed", "This cap is off", "Tomorrow is Friday".

395:

Synthesis: Engineers in particular synthesize propositional formulas (that eventually end up as circuits of symbols) from

11523:, Cambridge University Press, no ISBN. In the years between the first edition of 1912 and the 2nd edition of 1927, H. M. 9746:

The state diagram is similar in shape to the flip-flop's state diagram, but with different labelling on the transitions.

8655:, by definition). So their conjunction (AND) is a falsehood. But when taken in its assembled form, the sentence a TRUTH. 5335:" IF (a AND (IF b THEN NOT-a) THEN NOT-a" where " a " represents "its sunny" and " b " represents "the frog is croaking": 6614:

are not shown in the Hasse, Veitch and Karnaugh diagrams; these are shown in the Karnaugh map of the following section.)

3583: 1739:

the fully reduced formula the AND-OR-SELECT operator. The CASE (or SWITCH) operator is an extension of the same idea to

832: 12776: 12766: 12503: 12356: 11709: 3889: 675:, etc. A propositional variable is intended to represent an atomic proposition (assertion), such as "It is Saturday" = 11700: 12912: 11502: 11482: 11451: 11431: 11382: 11344: 11327: 11307: 11270: 10967: 10606: 315: 12254: 7804:

q = ( (~p & d & c ) ∨ (p & d & c) ∨ (p & d & ~c) ∨ (p & ~d & ~c) )

6949:( (~p & d & c ) ∨ (p & d & c) ∨ (p & d & ~c) ∨ (p & ~d & ~c) ) = q 3016:) specifies the third row in the truth table, and the other three rows then come from an application of definition ( 13009: 12753: 11578: 7757:

Steps in the reduction using a Karnaugh map. The final result is the OR (logical "sum") of the three reduced terms.

5373:"If pigs have wings, some winged animals are good to eat. Some winged animals are good to eat, so pigs have wings." 6065:

Commutivity and Identity (( 1 & ~c) = (~c & 1) = ~c, and (( 1 & b) ≡ (b & 1) ≡ b: ( ~c ∨ b )

3749: 13331: 12314: 12007: 10867:(PM) p. 91 eschews "the" because they require a clear-cut "object of sensation"; they stipulate the use of "this" 4532:

NOT, when distributed over OR or AND, does something peculiar (again, these can be verified with a truth-table):

11748: 10617:

to write up his ideas on logic, and to publish them as MAL in 1847" (Grattin-Guinness and Bornet 1997:xxviii).

7778:

until all abutting squares are accounted for, at which point the propositional formula is said to be minimized.

4952:

is a formula, there is exactly one symbol left after this expression, this symbol is a closing parenthesis, and

3669: 161:

Simple propositions are declarative in nature, that is, they make assertions about the condition or nature of a

13270: 12972: 12735: 12730: 12555: 11976: 11660: 10953:

While the notion of logical product is not so peculiar (e.g. 0*0=0, 0*1=0, 1*0=0, 1*1=1), the notion of (1+1=1

5925: 775:

Arbitrary propositional formulas are built from propositional variables and other propositional formulas using

368:, philosophers, rhetoricians and mathematicians reduce arguments to formulas and then study them (usually with 4498:

However, a truth-table demonstration shows that the form without the extra parentheses is perfectly adequate.

3489: 13265: 13048: 12965: 12678: 12609: 12486: 11728: 10651:). Russell's work led to a collaboration with Whitehead that, in the year 1912, produced the first volume of 6629: 4548:

Absorption, in particular the first one, causes the "laws" of logic to differ from the "laws" of arithmetic:

4440:

check 9 ( -parenthesis and 9 ) -parenthesis: ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~(a) ∨ b) ) )

679:(here the symbol = means " ... is assigned the variable named ...") or "I only go to the movies on Monday" = 3827: 13356: 13190: 13016: 12702: 12336: 11935: 10916: 7771: 6641: 5870: 4505: 3858: 132:" is not a value, but denotes a value. In some contexts, maintaining the distinction may be of importance. 28: 5799:, and written with a vertical bar | or vertical arrow ↑. The completeness of this connective was noted in 13068: 13063: 12673: 12412: 12341: 11670: 11571: 10666:

demonstrate that only one connective, the "stroke" | is sufficient to express all propositional formulas.

7770:

Minterms of adjacent (abutting) 1-squares (T-squares) can be reduced with respect to the number of their

5654:

shown along the bottom. The more common method is to use the definition of the NAND from the truth table.

1726:

In recognition of this problem, the sign → of formal implication in the propositional calculus is called

910: 407:

Example: in row 5, ( (b+a) + ci ) = ( (1+0) + 1 ) = the number "2". written as a binary number this is 10

384:, before we can conclude that a robot is an artificial intelligence the robot must pass the Turing test." 10805:

E. J. McCluskey and H. Shorr develop a method for simplifying propositional (switching) circuits (1962).

12997: 12587: 11981: 11949: 11640: 11458: 10686: 5662: 4504:: While ~(a) where a is a single variable is perfectly clear, ~a is adequate and is the usual way this 2827: 5758: 5694: 954: 13287: 13236: 13133: 12631: 12592: 12069: 11714: 11102:

As well as the first three, Hamilton pp.19-22 discusses logics built from only | (NAND), and ↓ (NOR).

5726: 3438: 2812:

for a new symbol in terms of the symbols on the left, the use of the IDENTITY sign = is appropriate:

980:

The following are the connectives common to rhetoric, philosophy and mathematics together with their

243:

In particular, simple sentences that employ notions of "all", "some", "a few", "one of", etc. called

115: 11743: 13336: 13128: 13058: 12597: 12449: 12432: 12155: 11635: 8663: 4957: 1670:

The following three propositions are equivalent (as indicated by the logical equivalence sign ≡ ):

1664: 806: 739:", and an ability to match the templates against the object of sensation (if indeed there is one). 8694:

To understand the behavior of formulas with feedback requires the more sophisticated analysis of

290:

that states a Knowledge editor's personal feelings or presents an original argument about a topic.

13346: 12960: 12937: 12898: 12784: 12725: 12371: 12291: 12135: 12079: 11692: 10775:

builds a multiplier using relays (1937–1938). He has to hand-wind his own relay coils to do this.

10543: 9231: 6674: 6598: 6594: 6014:(c, b, a) = d represents ( (c → b) ∨ (~c → a) ) ≡ ( (c & b) ∨ (~c & a) ) = d 4779: 377: 6670:. Each Karnaugh-map square and its corresponding truth-table evaluation represents one minterm. 3795: 13250: 12977: 12955: 12922: 12815: 12661: 12646: 12619: 12570: 12454: 12389: 12214: 12180: 12175: 12049: 11880: 11857: 11509: 10640: 10547: 8687: 7742:= (~p&d&c) ∨ (~p&d&c) ∨ (p&d&~c ) ∨ (p&d&c ) 6933: 6011: 4743: 3709: 2878: 2795:

The first table of this section stars *** the entry logical equivalence to note the fact that "

1402: 651: 346: 293: 59: 4434:& has seniority both sides: ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~a ∨ b) ) ) 198:

of propositions" It breaks a simple sentence down into two parts (i) its subject (the object (

35:. If the values of all variables in a propositional formula are given, it determines a unique 13351: 13180: 13033: 12825: 12543: 12279: 12185: 12044: 12029: 11910: 11351: 10864: 10699:(1937) invents the binary adder using mechanical relays. He builds this on his kitchen table. 10625: 8634:

Given the following examples-as-definitions, what does one make of the subsequent reasoning:

4920: 3626: 3523: 3467: 870: 786: 721: 6941:

Example: ((c & d) ∨ (p & ~(c & (~d)))) = q in conjunctive normal form is:

3543: 890: 13153: 13115: 12992: 12796: 12636: 12560: 12538: 12366: 12324: 12223: 12190: 12054: 11842: 11753: 10648: 6666:

Karnaugh squares; 4 variables produces 16 truth-table rows and 16 squares and therefore 16

5993: 5973: 5847: 5827: 4749: 4520:

Distributive law for OR: ( c ∨ ( a & b) ) ≡ ( (c ∨ a) & (c ∨ b) )

3563: 3426: 3134: 1727: 8638:(1) "This sentence is simple." (2) "This sentence is complex, and it is conjoined by AND." 6601:. Any propositional formula can be reduced to its conjunctive or disjunctive normal form. 6062:

Distribute "(1) &" over ((~c) ∨ b): ( ((1) & (~c)) ∨ ((1) & b )) )

4523:

Distributive law for AND: ( c & ( a ∨ b) ) ≡ ( (c & a) ∨ (c & b) )

8: 13341: 13282: 13173: 13158: 13138: 13095: 12982: 12932: 12858: 12803: 12740: 12533: 12528: 12476: 12244: 12233: 11905: 11805: 11733: 11724: 11720: 11655: 11650: 11489: 11280: 4785:

The inductive definition of infix formulas in the previous section can be converted to a

3141:(i.e. sufficient to form and to evaluate any well-formed formula created in the system). 3133:

specify these valuation axioms at the outset in the form of certain formulas such as the

2882:

from the wffs of his system L to the range (output) { T, F }, given that each variable p

2861: 2796: 1743:

possible, but mutually exclusive outcomes. Electrical engineers call the CASE operator a

1650:

The IF ... THEN ... ELSE ... connective appears as the simplest form of CASE operator of

1156: 717: 365: 228: 203: 55: 32: 20: 10601:

had critically analyzed the syllogistic logic with a sympathy toward Locke's semiotics.

13311: 13080: 13043: 13028: 13021: 13004: 12808: 12790: 12656: 12582: 12565: 12518: 12331: 12240: 12074: 12059: 12019: 11971: 11956: 11944: 11900: 11875: 11645: 11594: 11258: 10610: 8711: 8695: 7862:

Distributive law ( x & (y ∨ z) ) = ( (x & y) ∨ (x & z) ) :

6712:

is derived from this notion. This notion can be extended to three and four-dimensional

3246:(a → b), other variable-symbols such as "SW2" and "CON1" might be used, i.e. formally: 1655: 776: 716:—derived from experience and thereby susceptible to confirmation by third parties (the 244: 191: 12264: 1372: 13306: 13246: 13053: 12863: 12853: 12745: 12626: 12461: 12437: 12218: 12202: 12107: 12084: 11961: 11930: 11895: 11790: 11625: 11498: 11478: 11447: 11427: 11378: 11360: 11340: 11323: 11303: 11266: 11135: 11013:-- is required by the definition that Kleene gives the CASE operator (Kleene 1952229) 10963: 9002: 8819: 6640:

In electrical engineering, a variable x or its negation ~(x) can be referred to as a

5365:

Other circumstances may be preventing the frog from croaking: perhaps a crane ate it.

3225:

The definitions above for OR, IMPLICATION, XOR, and logical equivalence are actually

1696:( (c & b) ∨ (~c & a) ) ≡ " ( 'Counter is zero' AND 'go to instruction 748: 709: 252:"All blue pigs have wings but some pigs have no wings, hence some pigs are not blue". 232: 170: 107: 9058:"flipped" condition (state q=1). This behavior, now time-dependent, is shown by the 948:

Constant 0-ary connectives ⊤ and ⊥ (alternately, constants { T, F }, { 1, 0 } etc. )

13260: 13255: 13148: 13105: 12927: 12888: 12883: 12868: 12694: 12651: 12548: 12346: 12296: 11870: 11832: 11515: 11406: 11314: 10931: 10789: 10785: 10659: 10636: 10531: 8707: 4790: 3378: 1660: 1651: 353: 71: 5325:

valid is to submit it to verification with a truth table or by use of the "laws":

5305:

its variables", i.e. the formula is a tautology. Quite possibly a formula will be

4480:

Associative law for OR: (( a ∨ b ) ∨ c ) ≡ ( a ∨ (b ∨ c) )

3622:

This inductive definition can be easily extended to cover additional connectives.

165:

object of sensation e.g. "This cow is blue", "There's a coyote!" ("That coyote IS

13241: 13231: 13185: 13168: 13123: 13085: 12987: 12907: 12714: 12641: 12614: 12602: 12508: 12422: 12396: 12351: 12319: 12120: 11922: 11865: 11815: 11780: 11738: 10799: 10795: 10598: 10539: 9046: 8703: 4775: 4467: 4463: 4437:~ has seniority: ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~(a) ∨ b) ) ) 720:

of meaning). Empiricits hold that, in general, to arrive at the truth-value of a

400: 6059:

Law of excluded middle (((~c) ∨ c ) = 1 ): ( (1) & ((~c) ∨ b ) )

13226: 13205: 13163: 13143: 13038: 12893: 12491: 12481: 12471: 12466: 12400: 12274: 12150: 12039: 12034: 12012: 11613: 11438: 11122: 10696: 10602: 8699: 7898:

Law of identity ( x ∨ 0 ) = x leading to the reduced form of the formula:

7753: 6721: 6609: 6056:

Distribute "~c V" over (c & b): ( ((~c) ∨ c ) & ((~c) ∨ b )

5796: 4786: 4771: 2856:

For example, Hamilton uses two symbols = and ≠ when he defines the notion of a

1689:' ) AND ( IF 'It is NOT the case that counter is zero' THEN 'go to instruction 1685:( (c → b) & (~c → a) ) ≡ ( ( IF 'counter is zero' THEN 'go to instruction 656: 389: 11310:. This text is used in a "lower division two-quarter course" at UC San Diego. 10577:

Although a propositional calculus originated with Aristotle, the notion of an

5649: 148:"parenthesis rule" with respect to sequences of simple propositions (see more 13325: 13200: 12878: 12385: 12170: 12160: 12130: 12115: 11785: 11469: 11399: 10781: 10632: 9059: 9016: 6717: 3130: 756: 372:) for correctness (soundness). For example: Is the following argument sound? 207: 199: 119: 11126: 10802:(1956) address the theory of sequential (i.e. switching-circuit) "machines". 4423:

Example: " a & a → b ≡ a & ~a ∨ b " rewritten (rigorously) is

337:(meaning) of the symbols. The meanings are to be found outside the algebra. 185: 13100: 12947: 12848: 12840: 12720: 12668: 12577: 12513: 12496: 12427: 12286: 12145: 11847: 11630: 11147: 11046: 10823: 10690: 10614: 10571: 6915: 6725: 6624: 5295: 4483:

Associative law for AND: (( a & b ) & c ) ≡ ( a & (b & c) )

4329: 3359:

Use the notion of "schema" to substitute b for a in 2: ( (a & ~a) ≡ 0 )

3226: 3155: 2850: 1386: 752: 194:

goes a step further than the propositional calculus to an "analysis of the

106:", but, more precisely, a propositional formula is not a proposition but a 9023: 9015:

and expire when the delay(s) expire. The drawings on the right are called

7794:

Put the formula in conjunctive normal form with the formula to be reduced:

13210: 13090: 12269: 12259: 12206: 11890: 11810: 11795: 11675: 11620: 11232: 10772: 7880:

Commutative law and law of contradiction (x & ~x) = (~x & x) = 0:

6620: 1744: 1700:) OR ( 'It is NOT the case that 'counter is zero' AND 'go to instruction 981: 396: 381: 369: 265: 99: 36: 9040:

A truth table reveals the rows where inconsistencies occur between p = q

6909: 4559: 12140: 11995: 11966: 11772: 10927: 10917:

http://www.marxists.org/reference/subject/philosophy/works/us/quine.htm

10908: 10904: 10663: 10586: 7833:

Associative law (x ∨ (y ∨ z)) = ( (x ∨ y) ∨ z )

4420:

Example: " d & c ∨ w " rewritten is ( (d & c) ∨ w )

760: 701: 975: 13292: 13195: 12248: 12165: 12125: 12089: 12025: 11837: 11827: 11800: 11563: 11390: 10669: 10594: 10582: 10554:

Example: Here O is an expression about an object's BEING or QUALITY:

10535: 8683: 6713: 6709: 5358:"Saying it's sunny, but if the frog is croaking then it's not sunny, 5301: 4940:. Starting after the second symbol, match the shortest subexpression 3425:. The set of formulas over a given set of propositional variables is 3365:(see below for how to distribute "a ∨" over (b & ~b), etc.) 334: 145: 11041:

Reichenbach p. 20-22 and follows the conventions of PM. The symbol =

9240:

the result will be unknown at the outset but thereafter predicable.

5309:

but not valid. Another way of saying this is: "Being well-formed is

3640:

denote the set of all strings from an alphabet including symbols in

13277: 13075: 12523: 12228: 11822: 11495:

From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931

11131: 10826:; they consider it a form of the law of excluded middle misapplied. 10792:(1953) develop map-methods for simplifying propositional functions. 10644: 6667: 4569:

0 ); in other systems, it may be derived in the truth table below:

4431:→ has seniority: ( ( a & (a → b) ) ≡ ( a & ~a ∨ b ) ) 11475:

Introduction to Logic and to the Methodology of Deductive Sciences

8669: 3319:: (i) the formula to be replaced must be within a tautology, i.e. 262:

identity" to emphasize this extension. See more about this below.

102:, a propositional formula is often more briefly referred to as a " 12873: 11665: 11524: 11457:

On his page 204 in a footnote he references his set of axioms to

10991: 10903:(built-in, born-with) knowledge. "Radical reductionists" such as 8659: 6044:

Begin with the reduced form: ( (c & b) ∨ (~c & a) )

4428:≡ has seniority: ( ( a & a → b ) ≡ ( a & ~a ∨ b ) ) 6010:} ) forms a complete set. In the following the IF...THEN...ELSE 3362:

Use 2 to replace 0 with (b & ~b): ( a ∨ (b & ~b) )

1659:

outcome only one of two alternatives "a" or "b" (hence the name

214:

Example: "This blue pig has wings" becomes two sentences in the

11552: 10778:

Textbooks about "switching circuits" appear in the early 1950s.

700:

The truth values are only two: { TRUTH "T", FALSITY "F" }. An

686: 330: 11357:

George Boole: Selected Manuscripts on Logic and its Philosophy

10960:

Error Detecting Codes, Self-Checking Circuits and Applications

2826:. For more about the philosophy of the notion of IDENTITY see 12417: 11763: 11608: 11528: 11461:, "Sets of Independent Postulates for the Algebra of Logic", 7908:

q = ( (d & c) ∨ (p & d) ∨ (p & ~c) )

4742:

Complement for OR: (a ∨ ~a) = 1 or (a ∨ ~a) = T,

3625:

The inductive definition can also be rephrased in terms of a

1394: 659:), symbolic expressions are often denoted by variables named 10620:

About his contribution Grattin-Guinness and Bornet comment:

1730:

to distinguish it from the everyday, intuitive implication.

1645: 9049:

or just eliminated as inconsistent and hence "impossible".

8837:"qd" and "p" as shown in red; two stable states resulting: 5970:

This connective together with { 0, 1 }, ( or { F, T } or {

730:!" Is this statement a TRUTH? Truly I said it. And maybe I 287:

personal reflection, personal essay, or argumentative essay

11154:

and the two parts into which the number line is cut, i.e.

10693:(1919) describe a "trigger relay" made from a vacuum tube. 6047:

Substitute "1" for a: ( (c & b) ∨ (~c & 1) )

5864:(representing falsity) can be expressed using the stroke: 5795:

The binary connective corresponding to NAND is called the

4748:

Complement for AND: (a & ~a) = 0 or (a & ~a) = F,

4502:

Omitting parentheses with regards to a single-variable NOT

411:, where "co"=1 and Σ=0 as shown in the right-most columns. 399:. For example, one might write down a truth table for how 11071:

state machine (e.g. a Turing machine) to do the counting.

10705: 5135: 4956:

itself is a formula. This idea can be used to generate a

4474:

Commutative law for OR: ( a ∨ b ) ≡ ( b ∨ a )

3418:{\displaystyle \lnot ,\land ,\lor ,\to ,\leftrightarrow } 186:

Relationship between propositional and predicate formulas

11052: 7603: 7524: 7446: 7367: 7288: 7210: 7132: 7054: 6053:

Law of commutation for V: ( (~c) ∨ (c & b) )

6050:

Identity (~c & 1) = ~c: ( (c & b) ∨ (~c) )

5296:

Well-formed formulas versus valid formulas in inferences

2894:

in a wff is assigned an arbitrary truth value { T, F }.

755:; those with a continuous range of behaviors are called 10534:(1912:74) lists three laws of thought that derive from 4736:

Nullity for OR: (a ∨ 1) = 1 or (a ∨ T) = T

4730:

Identity for OR: (a ∨ 0) = a or (a ∨ F) = a

3377:

The classical presentation of propositional logic (see

3327:

Example: Use this set of formula schemas/equivalences:

359: 11497:, Harvard University Press, Cambridge, Massachusetts. 10835:

Rosenbloom and Kleene 1952:73-74 ranks all 11 symbols.

9751: 7917: 4477:

Commutative law for AND: ( a & b ) ≡ ( b & a )

3936:

and closed under all the formula building operations.

3356:

Use 1 to replace "a" with (a ∨ 0): (a ∨ 0)

266:

An algebra of propositions, the propositional calculus

11335:, (Pergamon Press 1963), 1966, (Dover edition 2007), 11009:

Indeed, exhaustive selection between alternatives --

6910:

Reduction by use of the map method (Veitch, Karnaugh)

5996: 5976: 5928: 5873: 5850: 5830: 5761: 5729: 5697: 5665: 4923: 4560:

Laws of evaluation: Identity, nullity, and complement

4335: 3892: 3861: 3830: 3798: 3752: 3712: 3672: 3586: 3566: 3546: 3526: 3492: 3470: 3441: 3387: 957: 913: 893: 873: 835: 809: 789: 11485:(pbk.). This book is in print and readily available. 11454:(pbk.). This book is in print and readily available. 7748: 6922: 4739:

Nullity for AND: (a & 0) = 0 or (a & F) = F

4733:

Identity for AND: (a & 1) = a or (a & T) = a

3433:

Each propositional variable in the set is a formula,

942:

Other binary connectives, such as NAND, NOR, and XOR

696:

Truth values in rhetoric, philosophy and mathematics

5370:Example 2 (from Reichenbach via Bertrand Russell): 5300:The notion of valid argument is usually applied to 4782:, eliminating the need for parentheses altogether. 4539:

De Morgan's law for AND: ¬(a ^ b) ≡ (¬a ∨ ¬b)

4457: 976:

Connectives of rhetoric, philosophy and mathematics

169:, behind the rocks."). Thus the simple "primitive" 122:

under discussion, just like an expression such as "

54:A propositional formula is constructed from simple 11208:procedure for obtaining word statements" (p. 185). 6002: 5982: 5954: 5913: 5856: 5836: 5779: 5747: 5715: 5683: 4932: 4552:Absorption (idempotency) for OR: (a ∨ a) ≡ a 4536:De Morgan's law for OR: ¬(a ∨ b) ≡ (¬a ^ ¬b) 3909: 3878: 3847: 3816: 3784: 3727: 3698: 3611:{\displaystyle \land ,\lor ,\to ,\leftrightarrow } 3610: 3572: 3552: 3532: 3512: 3476: 3456: 3417: 3271: 2872:in his "formal statement calculus" L. A valuation 963: 931: 899: 879: 860:{\displaystyle \land ,\lor ,\to ,\leftrightarrow } 859: 818: 795: 11519:1927 2nd edition, paperback edition to *53 1962, 11463:Transactions of the American Mathematical Society 4555:Absorption (idempotency) for AND: (a & a) ≡ a 3910:{\displaystyle {\mathcal {E}}_{\leftrightarrow }} 3429:to be the smallest set of expressions such that: 3233:(demonstrations, examples) for a general formula 13323: 11396:Introduction to the Theory of Switching Circuits 10546:: "Nothing can both be and not be", and (3) The 3633:denote a set of propositional variables and let 3207:LOGICAL EQUIVALENCE: ( (a → b) & (b → a) ) = 649:The simplest type of propositional formula is a 149: 140:For the purposes of the propositional calculus, 11477:, Dover Publications, Inc., Mineola, New York. 11446:, Dover Publications, Inc., Mineola, New York. 11426:, Dover Publications, Inc., Mineola, New York, 4755: 3217: 1674:( IF 'counter is zero' THEN 'go to instruction 945:The ternary connective IF ... THEN ... ELSE ... 376:"Given that consciousness is sufficient for an 74:such as NOT, AND, OR, or IMPLIES; for example: 39:. A propositional formula may also be called a 11287:. Amsterdam: North-Holland Publishing Company. 11265:. Mineola, New York: Dover Publications, Inc. 10288:state 1 with (d =0 & c=0 ), 1 is trapped 5644: 4765: 3917:corresponding to the other binary connectives. 3261:of the definition schema (~SW2 ∨ CON1) = 704:puts all propositions into two broad classes: 11579: 11339:, Dover Publications, Inc. Minola, New York, 10647:that he discovered in Frege's treatment ( cf 10441:state 1 with (d =1 & c=0 ), 1 is trapped 10135:state 0 with ( d=1 & r=0 ), 0 is trapped 9979:state 0 with ( s=0 & r=0 ), 0 is trapped 8629: 4488:Omitting parentheses in strings of AND and OR 11377:, Cambridge University Press, Cambridge UK, 11134:. He gives as example the definition of the 8574: 7815:Idempotency (absorption) [ A ∨ A) = A: 7684: 7673: 7671: 7669: 7667: 7665: 7662: 7660: 7657: 7654: 7651: 7649: 7647: 7644: 7641: 7638: 7636: 7633: 7631: 7628: 7625: 7622: 7620: 7618: 7615: 7612: 7609: 7606: 7594: 7592: 7590: 7588: 7586: 7583: 7581: 7578: 7575: 7572: 7570: 7568: 7565: 7562: 7559: 7557: 7554: 7552: 7549: 7546: 7543: 7541: 7539: 7536: 7533: 7530: 7527: 7516: 7514: 7512: 7510: 7508: 7505: 7503: 7500: 7497: 7494: 7492: 7490: 7487: 7484: 7481: 7479: 7476: 7474: 7471: 7468: 7465: 7463: 7461: 7458: 7455: 7452: 7449: 7437: 7435: 7433: 7431: 7429: 7426: 7424: 7421: 7418: 7415: 7413: 7411: 7408: 7405: 7402: 7400: 7397: 7395: 7392: 7389: 7386: 7384: 7382: 7379: 7376: 7373: 7370: 7358: 7356: 7354: 7352: 7350: 7347: 7345: 7342: 7339: 7336: 7334: 7332: 7329: 7326: 7323: 7321: 7318: 7316: 7313: 7310: 7307: 7305: 7303: 7300: 7297: 7294: 7291: 7280: 7278: 7276: 7274: 7272: 7269: 7267: 7264: 7261: 7258: 7256: 7254: 7251: 7248: 7245: 7243: 7240: 7238: 7235: 7232: 7229: 7227: 7225: 7222: 7219: 7216: 7213: 7202: 7200: 7198: 7196: 7194: 7191: 7189: 7186: 7183: 7180: 7178: 7176: 7173: 7170: 7167: 7165: 7162: 7160: 7157: 7154: 7151: 7149: 7147: 7144: 7141: 7138: 7135: 7124: 7122: 7120: 7118: 7116: 7113: 7111: 7108: 7105: 7102: 7100: 7098: 7095: 7092: 7089: 7087: 7084: 7082: 7079: 7076: 7073: 7071: 7069: 7066: 7063: 7060: 7057: 6889: 6872: 6855: 6838: 6821: 6804: 6787: 6770: 6753: 6736: 5774: 5762: 5742: 5730: 5710: 5698: 5678: 5666: 5288: 5285: 5282: 5279: 5276: 5273: 5270: 5267: 5264: 5261: 5258: 5255: 5252: 5249: 5246: 5243: 5240: 5237: 5234: 5231: 5228: 5225: 5222: 5219: 5216: 5213: 5210: 5207: 5204: 5201: 5198: 5195: 5192: 5189: 5186: 5183: 5180: 5177: 5174: 5171: 5168: 5165: 5162: 5159: 5156: 5153: 5150: 5147: 5144: 5141: 5138: 4977: 3785:{\displaystyle {\mathcal {E}}_{\land }(y,z)} 991: 770: 687:Truth-value assignments, formula evaluations 10591:Essay concerning human understanding (1690) 9709: 7682: 6635: 6604: 3242:Example: In the definition (~a ∨ b) = 3179:definition of a new variable: (c & d) = 11771: 11586: 11572: 11493:1967, 3rd printing with emendations 1976, 11257: 11058: 10997: 9811: 9230:The next simplest case is the "set-reset" 4727:Commutation of equality: (a = b) ≡ (b = a) 3699:{\displaystyle {\mathcal {E}}_{\lnot }(z)} 2790: 1389:(see below). Engineers also use the words 1367: 644: 58:, such as "five is greater than three" or 11412:Computation: Finite and Infinite Machines 10526: 9809: 9807: 9805: 9803: 9801: 9799: 9797: 9794: 9791: 9789: 9787: 9785: 9782: 9779: 9777: 9775: 9772: 9770: 9768: 9765: 9763: 9761: 9759: 9757: 9755: 9753: 8572: 7806:= ( #3 ∨ #7 ∨ #6 ∨ #4 ) 5955:{\displaystyle \bot \equiv (\top |\top )} 3503: 3499: 1646:CASE connective: IF ... THEN ... ELSE ... 380:and only conscious entities can pass the 316:Learn how and when to remove this message 10597:(theory of the use of symbols). By 1826 10563:Law of excluded middle: (O ∨ ~(O)) 9703:state 1 with s & r simultaneously 1 9022: 9001: 8818: 7752: 6608: 5824:In particular, the zero-ary connectives 5648: 5313:for a formula to be valid but it is not 3925:is defined to be the smallest subset of 3513:{\displaystyle (\alpha \,\Box \,\beta )} 3200:XOR: (~a & b) ∨ (a & ~b) = 3144: 1371: 8728: 6084: 5965: 5384: 4978: 4574: 3961: 3372: 1752: 239:( B(p) AND W(p) ) evaluates to { T, F } 13324: 11593: 11300:A Short Course in Discrete Mathematics 11279: 11190:, is defined in terms of the totality 9245: 9067: 8842: 8682:It helps to think of the formula as a 7924: 6962: 6728:(these are virtually the same thing). 3848:{\displaystyle {\mathcal {E}}_{\lor }} 3037: 11567: 11539:Logic Design with Integrated Circuits 11320:A Mathematical Introduction to Logic. 11112:writing down every one is infeasible. 10560:Law of contradiction: ~(O & ~(O)) 8670:Propositional formula with "feedback" 5914:{\displaystyle \top \equiv (a|(a|a))} 5338:( ( (a) & ( (b) → ~(a) ) ≡ ~(b) ) 5317:." The only way to find out if it is 4543: 3879:{\displaystyle {\mathcal {E}}_{\to }} 1136: 10913:The Emergence of Logical Empriricism 6737: 5790: 4511: 2931: 2896: 1092:b IS NECESSARY AND SUFFICIENT FOR a 992: 360:Usefulness of propositional formulas 269: 202:or plural) of discourse) and (ii) a 9225: 9052: 7918:Verify reduction with a truth table 7824:( #3 ∨ ∨ ∨ #4 ) 7050:Formula in conjunctive normal form 6593:. Some common normal forms include 4527: 3939: 3229:(or "schemata"), that is, they are 932:{\displaystyle (\alpha \to \beta )} 779:. Examples of connectives include: 13: 11424:Mathematical Logic: A First Course 11302:, Dover Publications, Mineola NY, 11263:The Elements of Mathematical Logic 11170:is defined in terms of the notion 10550:: "Everything must be or not be." 9737:& ( ~( c & ~( d ) ) ) ) = 9726:& ( ~( c & ~( d ) ) ) ) = 7765: 5997: 5977: 5946: 5938: 5929: 5874: 5851: 5831: 5739: 5707: 5675: 4948:that has balanced parentheses. If 4927: 4336:Connective seniority (symbol rank) 3896: 3865: 3834: 3756: 3716: 3682: 3676: 3445: 3388: 810: 783:The unary negation connective. If 333:(symbol-formation) rather than in 14: 13368: 11545: 11204:is not really possible to have a 10876:(italics added) Reichenbach p.80. 7749:Create the formula's Karnaugh map 6923:Produce the formula's truth table 5684:{\displaystyle \{\land ,\lnot \}} 3580:is one of the binary connectives 3302:)) ∨ (p & ~(c & ~(q 2815:((s → b) & (b → s)) = (s ↔ b) 829:The classical binary connectives 13305: 11551: 10899:Empiricits eschew the notion of 6738:decimal equivalent of (c, b, a) 5780:{\displaystyle \{\land ,\lor \}} 5716:{\displaystyle \{\lor ,\lnot \}} 4458:Commutative and associative laws 964:{\displaystyle \leftrightarrow } 655:. Propositions that are simple ( 274: 11285:Introduction to metamathematics 11238: 11220: 11211: 11197: 11115: 11105: 11096: 11083: 11074: 11064: 11035: 11025: 11016: 11003: 10982: 10829: 10816: 10680:Computation and switching logic 10518:state 1 with ( d=1 & c=1 ): 10056:state 0 with ( d=0 & c=1 ): 9656:state 1 with ( s=1 & r=0 ) 9563:state 1 with ( s=0 & r=0 ) 9424:state 0 with ( s=0 & r=1 ) 9377:state 0 with ( s=0 & r=0 ) 9062:to the right of the once-flip. 8679:result: oscillation or memory. 6630:Quine–McCluskey algorithm 6584: 6068:( ~c ∨ b ) is defined as 5748:{\displaystyle \{\to ,\lnot \}} 5343:This is well-formed, but is it 4969:This method locates as "1" the 4964:Example of parenthesis counting 3824:. There are similar operations 3629:operation (Enderton 2002). Let 3457:{\displaystyle (\lnot \alpha )} 3272:Substitution versus replacement 1713:because the second sentence is 135: 10973: 10947: 10937: 10921: 10893: 10879: 10870: 10858: 10849: 10542:: "Whatever is, is.", (2) The 8717: 7790:have no special significance: 6914:Veitch improved the notion of 5949: 5942: 5935: 5908: 5905: 5898: 5891: 5887: 5880: 5733: 5362:that the frog isn't croaking." 4924: 3902: 3871: 3811: 3799: 3779: 3767: 3722: 3713: 3693: 3687: 3605: 3599: 3507: 3493: 3451: 3442: 3412: 3406: 3162: 958: 926: 920: 914: 854: 848: 1: 13266:History of mathematical logic 11251: 10609:over a priority dispute with 8623: 8621: 8619: 8617: 8615: 8613: 8611: 8609: 8604: 8602: 8600: 8598: 8596: 8594: 8592: 8590: 8588: 8586: 8584: 8582: 8580: 8578: 8576: 7739: 7737: 7735: 7733: 7731: 7729: 7727: 7725: 7723: 7721: 7719: 7717: 7715: 7713: 7711: 7709: 7707: 7702: 7700: 7698: 7696: 7694: 7692: 7690: 7688: 7686: 7678: 7599: 7520: 7442: 7363: 7284: 7282: 7206: 7204: 7128: 7126: 3257:CON1, so we would have as an 3193:IMPLICATION: (~a ∨ b) = 1063:b IF AND ONLY IF a; b IFF a 819:{\displaystyle \lnot \alpha } 152:about well-formed formulas). 13191:Primitive recursive function 11465:, Vol. 5 91904) pp. 288-309. 11359:, Birkhäuser Verlag, Basil, 11235:'s student and close friend. 11121:This definition is given by 10842: 10809: 10444: 10367: 10291: 10214: 10138: 10061: 9982: 9905: 9817: 9816: 9659: 9612: 9566: 9519: 9473: 9427: 9380: 9333: 9281: 9244: 9195: 9168: 9142: 9115: 9087: 9066: 8968: 8942: 8916: 8890: 8862: 8841: 8793: 8770: 8746: 8727: 8606: 8500: 8429: 8358: 8287: 8216: 8145: 8074: 8003: 7923: 7741: 7704: 7675: 7596: 7518: 7439: 7360: 6961: 6498: 6415: 6332: 6249: 6152: 5598: 5555: 5512: 5469: 5421: 5420: 5383: 4756:Double negative (involution) 4686: 4649: 4606: 4261: 4201: 4141: 4081: 4011: 3111: 3096: 3081: 3066: 3049: 3036: 3024: 3012: 2987: 2969: 2683: 2579: 2475: 2371: 2267: 2163: 2059: 1955: 1835: 1751: 1326: 1288: 1250: 1212: 1174: 1135: 1103: 1074: 1046: 1018: 1004: 349:or the sentential calculus. 7: 11473:1941 (1995 Dover edition), 11442:1957 (1999 Dover edition), 10962:, North-Holland, New York, 9276: 9274: 9272: 9270: 9268: 9266: 9264: 9260: 9258: 9255: 9253: 9251: 9082: 9080: 9078: 9075: 9073: 9071: 9069: 8857: 8855: 8853: 8851: 8848: 8844: 8741: 8739: 8737: 8735: 8732: 6903:(~a & ~b & ~c) 6767:(~c & ~b & ~a) 6695:cba = (c=1, b=0, a=1) = 101 6660: 6149: 6147: 6145: 6142: 6140: 6138: 6136: 6134: 6132: 6127: 6125: 6123: 6121: 6119: 6117: 6115: 6113: 6111: 6108: 6106: 6104: 6102: 6100: 6098: 6096: 6094: 6090: 6088: 6086: 5645:Reduced sets of connectives 5415: 5404: 5387: 4980: 4766:Well-formed formulas (wffs) 4603: 4591: 3995: 3982: 3980: 3963: 3381:2002) uses the connectives 3044: 3018: 2981: 2922: 1830: 1828: 1826: 1824: 1822: 1820: 1818: 1816: 1814: 1811: 1809: 1807: 1805: 1803: 1801: 1799: 1795: 1793: 1791: 1789: 1785: 1783: 1781: 1779: 1777: 1774: 1772: 1770: 1766: 1764: 1762: 1758: 1756: 1754: 1011: 1007: 1002: 743:Truth values in engineering 708:—true no matter what (e.g. 256: 10: 13373: 12255:Schröder–Bernstein theorem 11982:Monadic predicate calculus 11641:Foundations of mathematics 10915:, Garland Publishing Inc. 10639:. First as the student of 9733:( ( c & d ) ∨ ( 9722:( ( c & d ) ∨ ( 9262: 9249: 9247: 8846: 8730: 8658:This is an example of the 8630:Impredicative propositions 7999: 7996: 7993: 7990: 7987: 7984: 7981: 7978: 7975: 7972: 7969: 7966: 7963: 7960: 7957: 7954: 7951: 7948: 7945: 7942: 7939: 7043: 7040: 7037: 7034: 7031: 7028: 7025: 7022: 7019: 7016: 7013: 7010: 7007: 7004: 7001: 6998: 6995: 6992: 6989: 6986: 6983: 6980: 6977: 6886:(c & ~b & ~a) 6784:(~c & ~b & a) 6129: 6092: 5412: 5410: 5408: 5406: 5402: 5400: 5398: 5396: 5394: 5392: 4600: 4595: 4593: 4589: 4587: 4584: 4582: 4410:(s, arithmetic successor). 4008: 4006: 4004: 4002: 4000: 3998: 3991: 3989: 3987: 3985: 3978: 3976: 3974: 3972: 3969: 3967: 3817:{\displaystyle (y\land z)} 3046: 3039: 1797: 1768: 1760: 1678:' ELSE 'go to instruction 994: 13301: 13288:Philosophy of mathematics 13237:Automated theorem proving 13219: 13114: 12946: 12839: 12691: 12408: 12384: 12362:Von Neumann–Bernays–Gödel 12307: 12201: 12105: 12003: 11994: 11921: 11856: 11762: 11684: 11601: 11322:Harcourt/Academic Press. 11182:. Thus the definition of 10445: 10368: 10292: 10215: 10139: 10062: 9983: 9906: 9813: 9660: 9613: 9567: 9520: 9474: 9428: 9381: 9334: 9282: 9278: 9196: 9169: 9143: 9116: 9088: 9084: 8997: 8969: 8943: 8917: 8891: 8863: 8859: 8794: 8771: 8747: 8743: 8501: 8430: 8359: 8288: 8217: 8146: 8075: 8008:( ~p & ~d & ~c ) 8004: 7058:( ~p & ~d & ~c ) 6890: 6873: 6869:(c & ~b & a) 6856: 6839: 6835:(c & b & ~a) 6822: 6818:(~c & b & ~a) 6805: 6801:(~c & b & a) 6788: 6771: 6754: 6499: 6416: 6333: 6250: 6153: 6027:(c, c, a) ≡ (c ∨ a) 5844:(representing truth) and 5599: 5556: 5513: 5470: 5390: 4687: 4650: 4607: 4576: 4462:Both AND and OR obey the 4262: 4202: 4142: 4082: 4012: 3965: 3921:The set of formulas over 3728:{\displaystyle (\lnot z)} 3112: 3097: 3082: 3067: 3050: 2684: 2580: 2476: 2372: 2268: 2164: 2060: 1956: 1836: 1611: 1579: 1547: 1515: 1483: 1457: 1454: 1435: 1423: 1420: 1410: 1327: 1289: 1251: 1213: 1175: 1104: 1075: 1047: 1019: 777:propositional connectives 771:Propositional connectives 11375:Logic for Mathematicians 11355:and Gérard Bornet 1997, 9710:Clocked flip-flop memory 8965:qd & p inconsistent 8939:qd & p inconsistent 8664:impredicative definition 8292:( p & ~d & ~c ) 8150:( ~p & d & ~c ) 7936: 7933: 7930: 7371:( p & ~d & ~c ) 7214:( ~p & d & ~c ) 6974: 6971: 6968: 6636:Literal, term and alterm 6605:Reduction to normal form 6038:to be (~c ∨ b) ): 5417: 5130: 5127: 5124: 5121: 5118: 5115: 5112: 5109: 5106: 5103: 5100: 5097: 5094: 5091: 5088: 5085: 5082: 5079: 5076: 5073: 5070: 5067: 5064: 5061: 5058: 5055: 5052: 5049: 5046: 5043: 5040: 5037: 5034: 5031: 5028: 5025: 5022: 5019: 5016: 5013: 5010: 5007: 5004: 5001: 4998: 4995: 4992: 4989: 4986: 4983: 4958:recursive descent parser 4795: 4597: 3993: 3041: 1832: 1787: 1715:not connected in meaning 1397:'s notion (a*a = a) and 1015: 1013: 1009: 1000: 998: 996: 867:. Thus, for example, if 41:propositional expression 12938:Self-verifying theories 12759:Tarski's axiomatization 11710:Tarski's undefinability 11705:incompleteness theorems 11178:is defined in terms of 11000:, pp. 30 and 54ff. 10544:law of noncontradiction 10364:q & p inconsistent 10211:q & p inconsistent 9609:q & p inconsistent 9516:q & p inconsistent 9470:q & p inconsistent 9165:q & p inconsistent 8813:q & p inconsistent 8790:q & p inconsistent 8434:( p & d & ~c ) 8363:( p & ~d & c ) 8221:( ~p & d & c ) 8079:( ~p & ~d & c) 7871:( ∨ ∨ ) 7842:( ∨ ∨ ) 7528:( p & d & ~c ) 7450:( p & ~d & c ) 7292:( ~p & d & c ) 7136:( ~p & ~d & c) 6675:disjunctive normal form 6599:disjunctive normal form 6595:conjunctive normal form 6030:(c, b, c) ≡ (c & b) 4933:{\displaystyle (\lnot } 4780:reverse Polish notation 4580: 4578: 3533:{\displaystyle \alpha } 3477:{\displaystyle \alpha } 3344: 2791:IDENTITY and evaluation 1667:programming language). 1368:Engineering connectives 880:{\displaystyle \alpha } 796:{\displaystyle \alpha } 645:Propositional variables 378:artificial intelligence 70:, using connectives or 60:propositional variables 27:is a type of syntactic 13332:Propositional calculus 13312:Mathematics portal 12923:Proof of impossibility 12571:propositional variable 11881:Propositional calculus 11510:Alfred North Whitehead 10704:Example: Given binary 10641:Alfred North Whitehead 10557:Law of Identity: O = O 10548:law of excluded middle 10527:Historical development 9029: 9020: 8827:Oscillation with delay 8823: 8505:( p & d & c ) 7889:( ∨ ∨ ) 7758: 7676:( p & d & c ) 7607:( p & d & c ) 6934:propositional function 6852:(c & b & a) 6615: 6004: 5984: 5956: 5915: 5858: 5838: 5781: 5749: 5717: 5685: 5655: 4934: 4813:propositional variable 4744:law of excluded middle 3911: 3880: 3849: 3818: 3786: 3729: 3700: 3612: 3574: 3554: 3553:{\displaystyle \beta } 3534: 3520:is a formula whenever 3514: 3478: 3464:is a formula whenever 3458: 3419: 3330:( (a ∨ 0) ≡ a ). 1431:half-adder (no carry) 1377: 1032:b IS SUFFICIENT FOR a 965: 933: 901: 900:{\displaystyle \beta } 881: 861: 820: 797: 652:propositional variable 388:Engineers analyze the 356:for AND, OR and NOT). 347:propositional calculus 296:by rewriting it in an 216:propositional calculus 13181:Kolmogorov complexity 13134:Computably enumerable 13034:Model complete theory 12826:Principia Mathematica 11886:Propositional formula 11715:Banach–Tarski paradox 11558:Propositional formula 11521:Principia Mathematica 11444:Introduction to Logic 11352:Ivor Grattan-Guinness 10865:Principia Mathematica 10653:Principia Mathematica 10626:universe of discourse 10520:q=1 is following d=1 10058:q=0 is following d=0 9026: 9005: 8822: 7756: 7597:(p & d & ~c) 7440:(~p & d & c) 7361:(~p & d & c) 6699:= 1*2 + 0*2 + 1*2 = 5 6623:can be unwieldy, but 6612: 6005: 6003:{\displaystyle \top } 5985: 5983:{\displaystyle \bot } 5957: 5916: 5859: 5857:{\displaystyle \bot } 5839: 5837:{\displaystyle \top } 5801:Principia Mathematica 5782: 5750: 5718: 5686: 5652: 4935: 4404:(arithmetic multiply) 4350:(LOGICAL EQUIVALENCE) 3945:truth-values for its 3912: 3881: 3850: 3819: 3787: 3730: 3701: 3613: 3575: 3573:{\displaystyle \Box } 3555: 3535: 3515: 3479: 3459: 3420: 3333:( (a & ~a) ≡ 0 ). 3218:Axiom and definition 3145:More complex formulas 2979:The two definitions ( 2946:) = F if and only if 2824:Principia Mathematica 1375: 1060:a IS NECESSARY FOR b 966: 934: 902: 882: 862: 821: 798: 722:synthetic proposition 25:propositional formula 13129:Church–Turing thesis 13116:Computability theory 12325:continuum hypothesis 11843:Square of opposition 11701:Gödel's completeness 11560:at Wikimedia Commons 11229:The Kleene Symposium 10724:and carry-out (c_out 10720:), their summation Σ 10628:and "0" was nothing. 9730:, but now let p = q: 8662:that result from an 5994: 5974: 5966:IF ... THEN ... ELSE 5926: 5871: 5848: 5828: 5759: 5727: 5695: 5663: 4971:principal connective 4921: 4750:law of contradiction 3890: 3859: 3828: 3796: 3750: 3710: 3670: 3584: 3564: 3544: 3524: 3490: 3468: 3439: 3385: 3373:Inductive definition 3321:logically equivalent 3186:OR: ~(~a & ~b) = 3135:law of contradiction 2862:well-formed formulas 1728:material implication 1405:' notion (a+a = a). 1157:logically equivalent 955: 911: 907:are formulas, so is 891: 871: 833: 807: 787: 13357:Logical expressions 13283:Mathematical object 13174:P versus NP problem 13139:Computable function 12933:Reverse mathematics 12859:Logical consequence 12736:primitive recursive 12731:elementary function 12504:Free/bound variable 12357:Tarski–Grothendieck 11876:Logical connectives 11806:Logical equivalence 11656:Logical consequence 11490:Jean van Heijenoort 11296:Williamson, S. Gill 11150:of the number line 10716:and carry-in ( c_in 9219:state 1 with s = 1 9192:state 1 with s = 0 8712:Macintosh computers 8696:sequential circuits 6024:(c, b, 1) ≡ (c → b) 5817:p ∨ q ≡ ~p|~q 5805:logical equivalence 4386:(THERE EXISTS AN x) 3427:inductively defined 2797:Logical equivalence 1035:b PRECISELY WHEN a 803:is a formula, then 718:verification theory 366:deductive reasoning 245:logical quantifiers 229:domain of discourse 21:propositional logic 13081:Transfer principle 13044:Semantics of logic 13029:Categorical theory 13005:Non-standard model 12519:Logical connective 11646:Information theory 11595:Mathematical logic 10611:Augustus De Morgan 9030: 9021: 8824: 7759: 6692:= c*2 + b*2 + a*2: 6616: 6000: 5980: 5952: 5911: 5854: 5834: 5820:p & q ≡ ~(p|q) 5777: 5745: 5713: 5681: 5656: 5351:then the argument 4930: 4544:Laws of absorption 3907: 3876: 3845: 3814: 3782: 3725: 3696: 3608: 3570: 3550: 3530: 3510: 3474: 3454: 3415: 3336:( (~a ∨ b) = 3022:). In particular ( 1656:computation theory 1378: 961: 929: 897: 877: 857: 816: 793: 298:encyclopedic style 285:is written like a 192:predicate calculus 49:sentential formula 13319: 13318: 13251:Abstract category 13054:Theories of truth 12864:Rule of inference 12854:Natural deduction 12835: 12834: 12380: 12379: 12085:Cartesian product 11990: 11989: 11896:Many-valued logic 11871:Boolean functions 11754:Russell's paradox 11729:diagonal argument 11626:First-order logic 11556:Media related to 11535:William E. Wickes 11527:1921 and M. Jean 11365:978-0-8176-5456-6 11292:Bender, Edward A. 11136:least upper bound 10649:Russell's paradox 10524: 10523: 9707: 9706: 9223: 9222: 8995: 8994: 8817: 8816: 8708:register machines 8627: 8626: 7746: 7745: 6932:Technically, the 6907: 6906: 6582: 6581: 5791:The stroke (NAND) 5642: 5641: 5293: 5292: 4724: 4723: 4512:Distributive laws 4322: 4321: 3560:are formulas and 3353:start with "a": a 3127: 3126: 2977: 2976: 2930: 2929: 2788: 2787: 1643: 1642: 1365: 1364: 1162:f IS A tautology 642: 641: 354:distributive laws 326: 325: 318: 108:formal expression 72:logical operators 13364: 13310: 13309: 13261:History of logic 13256:Category of sets 13149:Decision problem 12928:Ordinal analysis 12869:Sequent calculus 12767:Boolean algebras 12707: 12706: 12681: 12652:logical/constant 12406: 12405: 12392: 12315:Zermelo–Fraenkel 12066:Set operations: 12001: 12000: 11938: 11769: 11768: 11749:Löwenheim–Skolem 11636:Formal semantics 11588: 11581: 11574: 11565: 11564: 11555: 11536: 11518: 11516:Bertrand Russell 11512: 11492: 11472: 11459:E. V. Huntington 11441: 11421: 11409: 11407:Marvin L. Minsky 11393: 11372: 11354: 11334: 11333:Goodstein, R. L. 11317: 11297: 11293: 11288: 11276: 11259:Rosenbloom, Paul 11245: 11242: 11236: 11224: 11218: 11215: 11209: 11201: 11195: 11186:, an element of 11119: 11113: 11109: 11103: 11100: 11094: 11087: 11081: 11078: 11072: 11068: 11062: 11056: 11050: 11039: 11033: 11029: 11023: 11020: 11014: 11011:mutual exclusion 11007: 11001: 10995: 10989: 10986: 10980: 10977: 10971: 10951: 10945: 10941: 10935: 10932:sigmoid function 10925: 10919: 10897: 10891: 10883: 10877: 10874: 10868: 10862: 10856: 10853: 10836: 10833: 10827: 10820: 10660:Henry M. Sheffer 10637:Bertrand Russell 10607:William Hamilton 10532:Bertrand Russell 9749: 9748: 9243: 9242: 9226:Flip-flop memory 9065: 9064: 9053:Once-flip memory 9047:transient states 8840: 8839: 8726: 8725: 8704:counter machines 8647:( NOT(s) AND j ) 7922: 7921: 7047:Active minterms 6960: 6959: 6735: 6734: 6082: 6081: 6009: 6007: 6006: 6001: 5989: 5987: 5986: 5981: 5961: 5959: 5958: 5953: 5945: 5920: 5918: 5917: 5912: 5901: 5890: 5863: 5861: 5860: 5855: 5843: 5841: 5840: 5835: 5786: 5784: 5783: 5778: 5754: 5752: 5751: 5746: 5722: 5720: 5719: 5714: 5690: 5688: 5687: 5682: 5382: 5381: 4976: 4975: 4939: 4937: 4936: 4931: 4907: 4904: 4901: 4897: 4894: 4891: 4887: 4884: 4881: 4877: 4874: 4871: 4867: 4864: 4861: 4857: 4854: 4851: 4847: 4844: 4841: 4837: 4834: 4831: 4827: 4824: 4821: 4817: 4814: 4811: 4808: 4805: 4802: 4799: 4791:Backus-Naur form 4572: 4571: 4528:De Morgan's laws 4398:(arithmetic sum) 3959: 3958: 3940:Parsing formulas 3916: 3914: 3913: 3908: 3906: 3905: 3900: 3899: 3885: 3883: 3882: 3877: 3875: 3874: 3869: 3868: 3854: 3852: 3851: 3846: 3844: 3843: 3838: 3837: 3823: 3821: 3820: 3815: 3791: 3789: 3788: 3783: 3766: 3765: 3760: 3759: 3746:, the operation 3734: 3732: 3731: 3726: 3705: 3703: 3702: 3697: 3686: 3685: 3680: 3679: 3666:, the operation 3617: 3615: 3614: 3609: 3579: 3577: 3576: 3571: 3559: 3557: 3556: 3551: 3539: 3537: 3536: 3531: 3519: 3517: 3516: 3511: 3483: 3481: 3480: 3475: 3463: 3461: 3460: 3455: 3424: 3422: 3421: 3416: 3035: 3034: 3010:)". Definition ( 2971: 2932: 2924: 2897: 1750: 1749: 1661:switch statement 1652:recursion theory 1421:logical product 1408: 1407: 1165:NEITHER a NOR b 990: 989: 970: 968: 967: 962: 938: 936: 935: 930: 906: 904: 903: 898: 886: 884: 883: 878: 866: 864: 863: 858: 825: 823: 822: 817: 802: 800: 799: 794: 738: 728: 415: 414: 321: 314: 310: 307: 301: 278: 277: 270: 131: 13372: 13371: 13367: 13366: 13365: 13363: 13362: 13361: 13337:Boolean algebra 13322: 13321: 13320: 13315: 13304: 13297: 13242:Category theory 13232:Algebraic logic 13215: 13186:Lambda calculus 13124:Church encoding 13110: 13086:Truth predicate 12942: 12908:Complete theory 12831: 12700: 12696: 12692: 12687: 12679: 12399: and 12395: 12390: 12376: 12352:New Foundations 12320:axiom of choice 12303: 12265:Gödel numbering 12205: and 12197: 12101: 11986: 11936: 11917: 11866:Boolean algebra 11852: 11816:Equiconsistency 11781:Classical logic 11758: 11739:Halting problem 11727: and 11703: and 11691: and 11690: 11685:Theorems ( 11680: 11597: 11592: 11548: 11534: 11514: 11508: 11488: 11468: 11437: 11417: 11405: 11388: 11370: 11350: 11337:Boolean Algebra 11332: 11315:Enderton, H. B. 11313: 11295: 11291: 11281:Kleene, Stephen 11273: 11254: 11249: 11248: 11243: 11239: 11225: 11221: 11216: 11212: 11202: 11198: 11120: 11116: 11110: 11106: 11101: 11097: 11088: 11084: 11079: 11075: 11069: 11065: 11059:Rosenbloom 1950 11057: 11053: 11044: 11040: 11036: 11030: 11026: 11021: 11017: 11008: 11004: 10998:Rosenbloom 1950 10996: 10992: 10987: 10983: 10978: 10974: 10952: 10948: 10942: 10938: 10926: 10922: 10898: 10894: 10884: 10880: 10875: 10871: 10863: 10859: 10855:Hamilton 1978:1 10854: 10850: 10845: 10840: 10839: 10834: 10830: 10821: 10817: 10812: 10800:Edward F. Moore 10796:George H. Mealy 10784:1952 and 1955, 10764: 10760: 10756: 10752: 10746: 10742: 10738: 10734: 10727: 10723: 10719: 10715: 10711: 10599:Richard Whately 10540:law of identity 10529: 10519: 10057: 9712: 9228: 9055: 9043: 9036: 9000: 8720: 8700:Turing machines 8672: 8632: 7920: 7768: 7766:Reduce minterms 7751: 6925: 6912: 6722:Veitch diagrams 6702: 6698: 6691: 6663: 6638: 6607: 6587: 5995: 5992: 5991: 5975: 5972: 5971: 5968: 5941: 5927: 5924: 5923: 5897: 5886: 5872: 5869: 5868: 5849: 5846: 5845: 5829: 5826: 5825: 5793: 5760: 5757: 5756: 5728: 5725: 5724: 5696: 5693: 5692: 5664: 5661: 5660: 5647: 5298: 4922: 4919: 4918: 4910: 4909: 4905: 4902: 4899: 4895: 4892: 4889: 4885: 4882: 4879: 4875: 4872: 4869: 4865: 4862: 4859: 4855: 4852: 4849: 4845: 4842: 4839: 4835: 4832: 4829: 4825: 4822: 4819: 4815: 4812: 4809: 4806: 4803: 4800: 4797: 4776:Polish notation 4768: 4758: 4568: 4562: 4546: 4530: 4514: 4468:associative law 4464:commutative law 4460: 4338: 3942: 3930: 3901: 3895: 3894: 3893: 3891: 3888: 3887: 3870: 3864: 3863: 3862: 3860: 3857: 3856: 3839: 3833: 3832: 3831: 3829: 3826: 3825: 3797: 3794: 3793: 3761: 3755: 3754: 3753: 3751: 3748: 3747: 3711: 3708: 3707: 3681: 3675: 3674: 3673: 3671: 3668: 3667: 3662:Given a string 3656: 3649: 3638: 3585: 3582: 3581: 3565: 3562: 3561: 3545: 3542: 3541: 3525: 3522: 3521: 3491: 3488: 3487: 3469: 3466: 3465: 3440: 3437: 3436: 3386: 3383: 3382: 3375: 3368: 3339: 3309: 3305: 3301: 3297: 3290: 3286: 3274: 3264: 3256: 3252: 3245: 3223: 3210: 3203: 3196: 3189: 3182: 3171: 3165: 3147: 2893: 2889: 2885: 2848: 2844: 2840: 2793: 1648: 1508:~(b ∨ a) 1391:logical product 1370: 978: 956: 953: 952: 912: 909: 908: 892: 889: 888: 872: 869: 868: 834: 831: 830: 808: 805: 804: 788: 785: 784: 773: 736: 726: 689: 647: 410: 401:binary addition 362: 322: 311: 305: 302: 294:help improve it 291: 279: 275: 268: 259: 196:inner structure 188: 174:too ambiguous. 138: 123: 17: 12: 11: 5: 13370: 13360: 13359: 13354: 13349: 13347:Syntax (logic) 13344: 13339: 13334: 13317: 13316: 13302: 13299: 13298: 13296: 13295: 13290: 13285: 13280: 13275: 13274: 13273: 13263: 13258: 13253: 13244: 13239: 13234: 13229: 13227:Abstract logic 13223: 13221: 13217: 13216: 13214: 13213: 13208: 13206:Turing machine 13203: 13198: 13193: 13188: 13183: 13178: 13177: 13176: 13171: 13166: 13161: 13156: 13146: 13144:Computable set 13141: 13136: 13131: 13126: 13120: 13118: 13112: 13111: 13109: 13108: 13103: 13098: 13093: 13088: 13083: 13078: 13073: 13072: 13071: 13066: 13061: 13051: 13046: 13041: 13039:Satisfiability 13036: 13031: 13026: 13025: 13024: 13014: 13013: 13012: 13002: 13001: 13000: 12995: 12990: 12985: 12980: 12970: 12969: 12968: 12963: 12956:Interpretation 12952: 12950: 12944: 12943: 12941: 12940: 12935: 12930: 12925: 12920: 12910: 12905: 12904: 12903: 12902: 12901: 12891: 12886: 12876: 12871: 12866: 12861: 12856: 12851: 12845: 12843: 12837: 12836: 12833: 12832: 12830: 12829: 12821: 12820: 12819: 12818: 12813: 12812: 12811: 12806: 12801: 12781: 12780: 12779: 12777:minimal axioms 12774: 12763: 12762: 12761: 12750: 12749: 12748: 12743: 12738: 12733: 12728: 12723: 12710: 12708: 12689: 12688: 12686: 12685: 12684: 12683: 12671: 12666: 12665: 12664: 12659: 12654: 12649: 12639: 12634: 12629: 12624: 12623: 12622: 12617: 12607: 12606: 12605: 12600: 12595: 12590: 12580: 12575: 12574: 12573: 12568: 12563: 12553: 12552: 12551: 12546: 12541: 12536: 12531: 12526: 12516: 12511: 12506: 12501: 12500: 12499: 12494: 12489: 12484: 12474: 12469: 12467:Formation rule 12464: 12459: 12458: 12457: 12452: 12442: 12441: 12440: 12430: 12425: 12420: 12415: 12409: 12403: 12386:Formal systems 12382: 12381: 12378: 12377: 12375: 12374: 12369: 12364: 12359: 12354: 12349: 12344: 12339: 12334: 12329: 12328: 12327: 12322: 12311: 12309: 12305: 12304: 12302: 12301: 12300: 12299: 12289: 12284: 12283: 12282: 12275:Large cardinal 12272: 12267: 12262: 12257: 12252: 12238: 12237: 12236: 12231: 12226: 12211: 12209: 12199: 12198: 12196: 12195: 12194: 12193: 12188: 12183: 12173: 12168: 12163: 12158: 12153: 12148: 12143: 12138: 12133: 12128: 12123: 12118: 12112: 12110: 12103: 12102: 12100: 12099: 12098: 12097: 12092: 12087: 12082: 12077: 12072: 12064: 12063: 12062: 12057: 12047: 12042: 12040:Extensionality 12037: 12035:Ordinal number 12032: 12022: 12017: 12016: 12015: 12004: 11998: 11992: 11991: 11988: 11987: 11985: 11984: 11979: 11974: 11969: 11964: 11959: 11954: 11953: 11952: 11942: 11941: 11940: 11927: 11925: 11919: 11918: 11916: 11915: 11914: 11913: 11908: 11903: 11893: 11888: 11883: 11878: 11873: 11868: 11862: 11860: 11854: 11853: 11851: 11850: 11845: 11840: 11835: 11830: 11825: 11820: 11819: 11818: 11808: 11803: 11798: 11793: 11788: 11783: 11777: 11775: 11766: 11760: 11759: 11757: 11756: 11751: 11746: 11741: 11736: 11731: 11719:Cantor's 11717: 11712: 11707: 11697: 11695: 11682: 11681: 11679: 11678: 11673: 11668: 11663: 11658: 11653: 11648: 11643: 11638: 11633: 11628: 11623: 11618: 11617: 11616: 11605: 11603: 11599: 11598: 11591: 11590: 11583: 11576: 11568: 11562: 11561: 11547: 11546:External links 11544: 11543: 11542: 11532: 11506: 11486: 11466: 11455: 11439:Patrick Suppes 11435: 11419:Joel W. Robbin 11415: 11403: 11386: 11371:A. G. Hamilton 11368: 11348: 11330: 11311: 11289: 11277: 11271: 11253: 11250: 11247: 11246: 11237: 11219: 11210: 11196: 11123:Stephen Kleene 11114: 11104: 11095: 11082: 11073: 11063: 11051: 11042: 11034: 11024: 11015: 11002: 10990: 10981: 10972: 10946: 10936: 10920: 10892: 10878: 10869: 10857: 10847: 10846: 10844: 10841: 10838: 10837: 10828: 10814: 10813: 10811: 10808: 10807: 10806: 10803: 10793: 10779: 10776: 10769: 10768: 10767: 10766: 10762: 10758: 10757:) ∨ c_in 10754: 10750: 10747: 10744: 10740: 10736: 10732: 10725: 10721: 10717: 10713: 10709: 10701: 10700: 10697:George Stibitz 10694: 10687:William Eccles 10677: 10676: 10673: 10667: 10630: 10629: 10603:George Bentham 10593:used the word 10567: 10566: 10565: 10564: 10561: 10558: 10528: 10525: 10522: 10521: 10516: 10513: 10511: 10509: 10507: 10505: 10503: 10500: 10498: 10495: 10492: 10489: 10487: 10485: 10482: 10479: 10476: 10474: 10471: 10469: 10466: 10463: 10460: 10458: 10456: 10453: 10450: 10447: 10443: 10442: 10439: 10436: 10434: 10432: 10430: 10428: 10426: 10423: 10421: 10418: 10415: 10412: 10410: 10408: 10405: 10402: 10399: 10397: 10394: 10392: 10389: 10386: 10383: 10381: 10379: 10376: 10373: 10370: 10366: 10365: 10362: 10360: 10358: 10356: 10354: 10352: 10350: 10347: 10345: 10342: 10339: 10336: 10334: 10332: 10329: 10326: 10323: 10321: 10318: 10316: 10313: 10310: 10307: 10305: 10303: 10300: 10297: 10294: 10290: 10289: 10286: 10283: 10281: 10279: 10277: 10275: 10273: 10270: 10268: 10265: 10262: 10259: 10257: 10255: 10252: 10249: 10246: 10244: 10241: 10239: 10236: 10233: 10230: 10228: 10226: 10223: 10220: 10217: 10213: 10212: 10209: 10207: 10205: 10203: 10201: 10199: 10197: 10194: 10192: 10189: 10186: 10183: 10181: 10179: 10176: 10173: 10170: 10168: 10165: 10163: 10160: 10157: 10154: 10152: 10150: 10147: 10144: 10141: 10137: 10136: 10133: 10130: 10128: 10126: 10124: 10122: 10120: 10117: 10115: 10112: 10109: 10106: 10104: 10102: 10099: 10096: 10093: 10091: 10088: 10086: 10083: 10080: 10077: 10075: 10073: 10070: 10067: 10064: 10060: 10059: 10054: 10051: 10049: 10047: 10045: 10043: 10041: 10038: 10036: 10033: 10030: 10027: 10025: 10023: 10020: 10017: 10014: 10012: 10009: 10007: 10004: 10001: 9998: 9996: 9994: 9991: 9988: 9985: 9981: 9980: 9977: 9974: 9972: 9970: 9968: 9966: 9964: 9961: 9959: 9956: 9953: 9950: 9948: 9946: 9943: 9940: 9937: 9935: 9932: 9930: 9927: 9924: 9921: 9919: 9917: 9914: 9911: 9908: 9904: 9903: 9900: 9897: 9894: 9891: 9888: 9885: 9882: 9879: 9876: 9873: 9870: 9867: 9864: 9861: 9858: 9855: 9852: 9849: 9846: 9843: 9840: 9837: 9834: 9831: 9828: 9825: 9822: 9819: 9815: 9814: 9812: 9810: 9808: 9806: 9804: 9802: 9800: 9798: 9796: 9793: 9790: 9788: 9786: 9784: 9781: 9778: 9776: 9774: 9771: 9769: 9767: 9764: 9762: 9760: 9758: 9756: 9754: 9752: 9744: 9743: 9742: 9741: 9731: 9711: 9708: 9705: 9704: 9701: 9698: 9696: 9694: 9692: 9689: 9687: 9684: 9681: 9678: 9676: 9673: 9670: 9668: 9665: 9662: 9658: 9657: 9654: 9651: 9649: 9647: 9645: 9642: 9640: 9637: 9634: 9631: 9629: 9626: 9623: 9621: 9618: 9615: 9611: 9610: 9607: 9605: 9603: 9601: 9599: 9596: 9594: 9591: 9588: 9585: 9583: 9580: 9577: 9575: 9572: 9569: 9565: 9564: 9561: 9558: 9556: 9554: 9552: 9549: 9547: 9544: 9541: 9538: 9536: 9533: 9530: 9528: 9525: 9522: 9518: 9517: 9514: 9512: 9510: 9508: 9506: 9503: 9501: 9498: 9495: 9492: 9490: 9487: 9484: 9482: 9479: 9476: 9472: 9471: 9468: 9466: 9464: 9462: 9460: 9457: 9455: 9452: 9449: 9446: 9444: 9441: 9438: 9436: 9433: 9430: 9426: 9425: 9422: 9419: 9417: 9415: 9413: 9410: 9408: 9405: 9402: 9399: 9397: 9394: 9391: 9389: 9386: 9383: 9379: 9378: 9375: 9372: 9370: 9368: 9366: 9363: 9361: 9358: 9355: 9352: 9350: 9347: 9344: 9342: 9339: 9336: 9332: 9331: 9329: 9326: 9323: 9320: 9317: 9314: 9311: 9308: 9305: 9302: 9299: 9296: 9293: 9290: 9287: 9284: 9280: 9279: 9277: 9275: 9273: 9271: 9269: 9267: 9265: 9263: 9261: 9259: 9257: 9254: 9252: 9250: 9248: 9246: 9227: 9224: 9221: 9220: 9217: 9214: 9212: 9209: 9206: 9203: 9201: 9198: 9194: 9193: 9190: 9187: 9185: 9182: 9179: 9176: 9174: 9171: 9167: 9166: 9163: 9161: 9159: 9156: 9153: 9150: 9148: 9145: 9141: 9140: 9137: 9134: 9132: 9129: 9126: 9123: 9121: 9118: 9114: 9113: 9111: 9108: 9105: 9102: 9099: 9096: 9093: 9090: 9086: 9085: 9083: 9081: 9079: 9077: 9074: 9072: 9070: 9068: 9054: 9051: 9041: 9034: 9017:state diagrams 8999: 8996: 8993: 8992: 8989: 8986: 8984: 8981: 8979: 8976: 8974: 8971: 8967: 8966: 8963: 8960: 8958: 8955: 8953: 8950: 8948: 8945: 8941: 8940: 8937: 8934: 8932: 8929: 8927: 8924: 8922: 8919: 8915: 8914: 8911: 8908: 8906: 8903: 8901: 8898: 8896: 8893: 8889: 8888: 8886: 8883: 8880: 8877: 8874: 8871: 8868: 8865: 8861: 8860: 8858: 8856: 8854: 8852: 8850: 8847: 8845: 8843: 8815: 8814: 8811: 8808: 8806: 8803: 8801: 8798: 8796: 8792: 8791: 8788: 8785: 8783: 8780: 8778: 8775: 8773: 8769: 8768: 8766: 8763: 8760: 8757: 8754: 8751: 8749: 8745: 8744: 8742: 8740: 8738: 8736: 8734: 8731: 8729: 8719: 8716: 8671: 8668: 8649: 8648: 8640: 8639: 8631: 8628: 8625: 8624: 8622: 8620: 8618: 8616: 8614: 8612: 8610: 8608: 8605: 8603: 8601: 8599: 8597: 8595: 8593: 8591: 8589: 8587: 8585: 8583: 8581: 8579: 8577: 8575: 8573: 8570: 8569: 8567: 8565: 8562: 8560: 8557: 8554: 8551: 8549: 8546: 8544: 8541: 8538: 8535: 8533: 8530: 8528: 8525: 8522: 8519: 8517: 8515: 8512: 8509: 8506: 8503: 8499: 8498: 8496: 8494: 8491: 8489: 8486: 8483: 8480: 8478: 8475: 8473: 8470: 8467: 8464: 8462: 8459: 8457: 8454: 8451: 8448: 8446: 8444: 8441: 8438: 8435: 8432: 8428: 8427: 8425: 8423: 8420: 8418: 8415: 8412: 8409: 8407: 8404: 8402: 8399: 8396: 8393: 8391: 8388: 8386: 8383: 8380: 8377: 8375: 8373: 8370: 8367: 8364: 8361: 8357: 8356: 8354: 8352: 8349: 8347: 8344: 8341: 8338: 8336: 8333: 8331: 8328: 8325: 8322: 8320: 8317: 8315: 8312: 8309: 8306: 8304: 8302: 8299: 8296: 8293: 8290: 8286: 8285: 8283: 8281: 8278: 8276: 8273: 8270: 8267: 8265: 8262: 8260: 8257: 8254: 8251: 8249: 8246: 8244: 8241: 8238: 8235: 8233: 8231: 8228: 8225: 8222: 8219: 8215: 8214: 8212: 8210: 8207: 8205: 8202: 8199: 8196: 8194: 8191: 8189: 8186: 8183: 8180: 8178: 8175: 8173: 8170: 8167: 8164: 8162: 8160: 8157: 8154: 8151: 8148: 8144: 8143: 8141: 8139: 8136: 8134: 8131: 8128: 8125: 8123: 8120: 8118: 8115: 8112: 8109: 8107: 8104: 8102: 8099: 8096: 8093: 8091: 8089: 8086: 8083: 8080: 8077: 8073: 8072: 8070: 8068: 8065: 8063: 8060: 8057: 8054: 8052: 8049: 8047: 8044: 8041: 8038: 8036: 8033: 8031: 8028: 8025: 8022: 8020: 8018: 8015: 8012: 8009: 8006: 8002: 8001: 7998: 7995: 7992: 7989: 7986: 7983: 7980: 7977: 7974: 7971: 7968: 7965: 7962: 7959: 7956: 7953: 7950: 7947: 7944: 7941: 7938: 7935: 7932: 7929: 7926: 7919: 7916: 7915: 7914: 7913: 7912: 7911: 7910: 7900: 7899: 7895: 7894: 7893: 7892: 7891: 7890: 7882: 7881: 7877: 7876: 7875: 7874: 7873: 7872: 7864: 7863: 7859: 7858: 7857: 7856: 7855: 7854: 7843: 7835: 7834: 7830: 7829: 7828: 7827: 7826: 7825: 7817: 7816: 7812: 7811: 7810: 7809: 7808: 7807: 7796: 7795: 7787: 7786: 7767: 7764: 7750: 7747: 7744: 7743: 7740: 7738: 7736: 7734: 7732: 7730: 7728: 7726: 7724: 7722: 7720: 7718: 7716: 7714: 7712: 7710: 7708: 7706: 7703: 7701: 7699: 7697: 7695: 7693: 7691: 7689: 7687: 7685: 7683: 7680: 7679: 7677: 7674: 7672: 7670: 7668: 7666: 7664: 7661: 7659: 7656: 7653: 7650: 7648: 7646: 7643: 7640: 7637: 7635: 7632: 7630: 7627: 7624: 7621: 7619: 7617: 7614: 7611: 7608: 7605: 7601: 7600: 7598: 7595: 7593: 7591: 7589: 7587: 7585: 7582: 7580: 7577: 7574: 7571: 7569: 7567: 7564: 7561: 7558: 7556: 7553: 7551: 7548: 7545: 7542: 7540: 7538: 7535: 7532: 7529: 7526: 7522: 7521: 7519: 7517: 7515: 7513: 7511: 7509: 7507: 7504: 7502: 7499: 7496: 7493: 7491: 7489: 7486: 7483: 7480: 7478: 7475: 7473: 7470: 7467: 7464: 7462: 7460: 7457: 7454: 7451: 7448: 7444: 7443: 7441: 7438: 7436: 7434: 7432: 7430: 7428: 7425: 7423: 7420: 7417: 7414: 7412: 7410: 7407: 7404: 7401: 7399: 7396: 7394: 7391: 7388: 7385: 7383: 7381: 7378: 7375: 7372: 7369: 7365: 7364: 7362: 7359: 7357: 7355: 7353: 7351: 7349: 7346: 7344: 7341: 7338: 7335: 7333: 7331: 7328: 7325: 7322: 7320: 7317: 7315: 7312: 7309: 7306: 7304: 7302: 7299: 7296: 7293: 7290: 7286: 7285: 7283: 7281: 7279: 7277: 7275: 7273: 7271: 7268: 7266: 7263: 7260: 7257: 7255: 7253: 7250: 7247: 7244: 7242: 7239: 7237: 7234: 7231: 7228: 7226: 7224: 7221: 7218: 7215: 7212: 7208: 7207: 7205: 7203: 7201: 7199: 7197: 7195: 7193: 7190: 7188: 7185: 7182: 7179: 7177: 7175: 7172: 7169: 7166: 7164: 7161: 7159: 7156: 7153: 7150: 7148: 7146: 7143: 7140: 7137: 7134: 7130: 7129: 7127: 7125: 7123: 7121: 7119: 7117: 7115: 7112: 7110: 7107: 7104: 7101: 7099: 7097: 7094: 7091: 7088: 7086: 7083: 7081: 7078: 7075: 7072: 7070: 7068: 7065: 7062: 7059: 7056: 7052: 7051: 7048: 7045: 7042: 7039: 7036: 7033: 7030: 7027: 7024: 7021: 7018: 7015: 7012: 7009: 7006: 7003: 7000: 6997: 6994: 6991: 6988: 6985: 6982: 6979: 6976: 6973: 6970: 6967: 6964: 6955: 6954: 6953: 6952: 6951: 6950: 6939: 6938: 6924: 6921: 6911: 6908: 6905: 6904: 6901: 6898: 6895: 6892: 6888: 6887: 6884: 6881: 6878: 6875: 6871: 6870: 6867: 6864: 6861: 6858: 6854: 6853: 6850: 6847: 6844: 6841: 6837: 6836: 6833: 6830: 6827: 6824: 6820: 6819: 6816: 6813: 6810: 6807: 6803: 6802: 6799: 6796: 6793: 6790: 6786: 6785: 6782: 6779: 6776: 6773: 6769: 6768: 6765: 6762: 6759: 6756: 6752: 6751: 6748: 6745: 6742: 6739: 6718:Hasse diagrams 6706: 6705: 6704: 6703: 6700: 6696: 6693: 6689: 6662: 6659: 6658: 6657: 6656: 6655: 6652: 6637: 6634: 6606: 6603: 6586: 6583: 6580: 6579: 6577: 6575: 6572: 6569: 6567: 6564: 6562: 6559: 6557: 6554: 6552: 6550: 6547: 6544: 6542: 6539: 6537: 6534: 6532: 6529: 6527: 6524: 6521: 6518: 6516: 6514: 6512: 6510: 6507: 6504: 6501: 6497: 6496: 6494: 6492: 6489: 6486: 6484: 6481: 6479: 6476: 6474: 6471: 6469: 6467: 6464: 6461: 6459: 6456: 6454: 6451: 6449: 6446: 6444: 6441: 6438: 6435: 6433: 6431: 6429: 6427: 6424: 6421: 6418: 6414: 6413: 6411: 6409: 6406: 6403: 6401: 6398: 6396: 6393: 6391: 6388: 6386: 6384: 6381: 6378: 6376: 6373: 6371: 6368: 6366: 6363: 6361: 6358: 6355: 6352: 6350: 6348: 6346: 6344: 6341: 6338: 6335: 6331: 6330: 6328: 6326: 6323: 6320: 6318: 6315: 6313: 6310: 6308: 6305: 6303: 6301: 6298: 6295: 6293: 6290: 6288: 6285: 6283: 6280: 6278: 6275: 6272: 6269: 6267: 6265: 6263: 6261: 6258: 6255: 6252: 6248: 6247: 6244: 6241: 6238: 6235: 6232: 6229: 6226: 6223: 6220: 6217: 6214: 6211: 6208: 6205: 6202: 6199: 6196: 6193: 6190: 6187: 6184: 6181: 6178: 6175: 6172: 6169: 6166: 6164: 6161: 6158: 6155: 6151: 6150: 6148: 6146: 6144: 6141: 6139: 6137: 6135: 6133: 6131: 6128: 6126: 6124: 6122: 6120: 6118: 6116: 6114: 6112: 6110: 6107: 6105: 6103: 6101: 6099: 6097: 6095: 6093: 6091: 6089: 6087: 6085: 6076: 6075: 6074: 6073: 6066: 6063: 6060: 6057: 6054: 6051: 6048: 6045: 6032: 6031: 6028: 6025: 6022: 6021:(c, 0, 1) ≡ ~c 6019: 5999: 5979: 5967: 5964: 5963: 5962: 5951: 5948: 5944: 5940: 5937: 5934: 5931: 5921: 5910: 5907: 5904: 5900: 5896: 5893: 5889: 5885: 5882: 5879: 5876: 5853: 5833: 5822: 5821: 5818: 5815: 5812: 5797:Sheffer stroke 5792: 5789: 5776: 5773: 5770: 5767: 5764: 5744: 5741: 5738: 5735: 5732: 5712: 5709: 5706: 5703: 5700: 5680: 5677: 5674: 5671: 5668: 5646: 5643: 5640: 5639: 5637: 5634: 5631: 5629: 5626: 5623: 5621: 5618: 5615: 5612: 5610: 5608: 5606: 5604: 5601: 5597: 5596: 5594: 5591: 5588: 5586: 5583: 5580: 5578: 5575: 5572: 5569: 5567: 5565: 5563: 5561: 5558: 5554: 5553: 5551: 5548: 5545: 5543: 5540: 5537: 5535: 5532: 5529: 5526: 5524: 5522: 5520: 5518: 5515: 5511: 5510: 5508: 5505: 5502: 5500: 5497: 5494: 5492: 5489: 5486: 5483: 5481: 5479: 5477: 5475: 5472: 5468: 5467: 5464: 5461: 5458: 5455: 5452: 5449: 5446: 5443: 5440: 5437: 5434: 5431: 5428: 5426: 5423: 5419: 5418: 5416: 5414: 5411: 5409: 5407: 5405: 5403: 5401: 5399: 5397: 5395: 5393: 5391: 5389: 5386: 5380: 5379: 5378: 5377: 5374: 5368: 5367: 5366: 5363: 5356: 5341: 5340: 5339: 5336: 5297: 5294: 5291: 5290: 5287: 5284: 5281: 5278: 5275: 5272: 5269: 5266: 5263: 5260: 5257: 5254: 5251: 5248: 5245: 5242: 5239: 5236: 5233: 5230: 5227: 5224: 5221: 5218: 5215: 5212: 5209: 5206: 5203: 5200: 5197: 5194: 5191: 5188: 5185: 5182: 5179: 5176: 5173: 5170: 5167: 5164: 5161: 5158: 5155: 5152: 5149: 5146: 5143: 5140: 5137: 5133: 5132: 5129: 5126: 5123: 5120: 5117: 5114: 5111: 5108: 5105: 5102: 5099: 5096: 5093: 5090: 5087: 5084: 5081: 5078: 5075: 5072: 5069: 5066: 5063: 5060: 5057: 5054: 5051: 5048: 5045: 5042: 5039: 5036: 5033: 5030: 5027: 5024: 5021: 5018: 5015: 5012: 5009: 5006: 5003: 5000: 4997: 4994: 4991: 4988: 4985: 4982: 4979: 4960:for formulas. 4929: 4926: 4796: 4787:formal grammar 4772:infix notation 4767: 4764: 4763: 4762: 4757: 4754: 4753: 4752: 4746: 4740: 4737: 4734: 4731: 4728: 4722: 4721: 4719: 4716: 4713: 4711: 4709: 4706: 4704: 4701: 4698: 4695: 4693: 4691: 4689: 4685: 4684: 4682: 4679: 4676: 4674: 4672: 4669: 4667: 4664: 4661: 4658: 4656: 4654: 4652: 4648: 4647: 4644: 4641: 4638: 4635: 4632: 4629: 4626: 4623: 4620: 4617: 4614: 4611: 4609: 4605: 4604: 4602: 4599: 4596: 4594: 4592: 4590: 4588: 4586: 4583: 4581: 4579: 4577: 4575: 4566: 4561: 4558: 4557: 4556: 4553: 4545: 4542: 4541: 4540: 4537: 4529: 4526: 4525: 4524: 4521: 4513: 4510: 4496: 4495: 4485: 4484: 4481: 4478: 4475: 4459: 4456: 4455: 4454: 4453: 4452: 4445: 4444: 4443: 4442: 4441: 4438: 4435: 4432: 4429: 4421: 4414: 4413: 4412: 4411: 4408: 4405: 4402: 4399: 4396: 4393: 4390: 4387: 4384: 4381: 4378: 4375: 4372: 4369: 4366: 4363: 4360: 4357: 4354: 4351: 4348: 4337: 4334: 4320: 4319: 4317: 4315: 4313: 4310: 4308: 4305: 4302: 4300: 4297: 4295: 4292: 4290: 4287: 4285: 4282: 4279: 4276: 4274: 4271: 4269: 4267: 4264: 4260: 4259: 4257: 4255: 4253: 4250: 4248: 4245: 4242: 4240: 4237: 4235: 4232: 4230: 4227: 4225: 4222: 4219: 4216: 4214: 4211: 4209: 4207: 4204: 4200: 4199: 4197: 4195: 4193: 4190: 4188: 4185: 4182: 4180: 4177: 4175: 4172: 4170: 4167: 4165: 4162: 4159: 4156: 4154: 4151: 4149: 4147: 4144: 4140: 4139: 4137: 4135: 4133: 4130: 4128: 4125: 4122: 4120: 4117: 4115: 4112: 4110: 4107: 4105: 4102: 4099: 4096: 4094: 4091: 4089: 4087: 4084: 4080: 4079: 4076: 4073: 4070: 4067: 4064: 4061: 4058: 4055: 4052: 4049: 4046: 4043: 4040: 4037: 4034: 4031: 4028: 4025: 4022: 4019: 4017: 4014: 4010: 4009: 4007: 4005: 4003: 4001: 3999: 3997: 3994: 3992: 3990: 3988: 3986: 3984: 3981: 3979: 3977: 3975: 3973: 3971: 3968: 3966: 3964: 3962: 3957: 3956: 3941: 3938: 3928: 3919: 3918: 3904: 3898: 3873: 3867: 3842: 3836: 3813: 3810: 3807: 3804: 3801: 3781: 3778: 3775: 3772: 3769: 3764: 3758: 3738:Given strings 3736: 3724: 3721: 3718: 3715: 3695: 3692: 3689: 3684: 3678: 3654: 3647: 3636: 3620: 3619: 3607: 3604: 3601: 3598: 3595: 3592: 3589: 3569: 3549: 3529: 3509: 3506: 3502: 3498: 3495: 3485: 3473: 3453: 3450: 3447: 3444: 3434: 3414: 3411: 3408: 3405: 3402: 3399: 3396: 3393: 3390: 3374: 3371: 3370: 3369: 3367: 3366: 3363: 3360: 3357: 3354: 3350: 3348: 3347: 3346: 3343: 3341: 3337: 3334: 3331: 3314: 3313: 3312: 3311: 3307: 3303: 3299: 3295: 3288: 3284: 3273: 3270: 3269: 3268: 3267: 3266: 3262: 3254: 3250: 3243: 3222: 3216: 3215: 3214: 3213: 3212: 3208: 3205: 3201: 3198: 3194: 3191: 3187: 3184: 3180: 3169: 3164: 3161: 3146: 3143: 3131:formal systems 3125: 3124: 3122: 3119: 3116: 3113: 3110: 3109: 3107: 3104: 3101: 3098: 3095: 3094: 3092: 3089: 3086: 3083: 3080: 3079: 3077: 3074: 3071: 3068: 3065: 3064: 3061: 3058: 3055: 3052: 3048: 3047: 3045: 3043: 3040: 3038: 2975: 2974: 2965: 2963: 2928: 2927: 2918: 2916: 2891: 2887: 2883: 2846: 2842: 2838: 2819: 2818: 2817: 2816: 2792: 2789: 2786: 2785: 2782: 2780: 2778: 2775: 2772: 2770: 2767: 2765: 2762: 2760: 2757: 2755: 2752: 2749: 2746: 2744: 2742: 2740: 2737: 2735: 2733: 2730: 2727: 2725: 2722: 2720: 2717: 2715: 2712: 2710: 2707: 2704: 2701: 2699: 2697: 2695: 2692: 2689: 2686: 2682: 2681: 2678: 2676: 2674: 2671: 2668: 2666: 2663: 2661: 2658: 2656: 2653: 2651: 2648: 2645: 2642: 2640: 2638: 2636: 2633: 2631: 2629: 2626: 2623: 2621: 2618: 2616: 2613: 2611: 2608: 2606: 2603: 2600: 2597: 2595: 2593: 2591: 2588: 2585: 2582: 2578: 2577: 2574: 2572: 2570: 2567: 2564: 2562: 2559: 2557: 2554: 2552: 2549: 2547: 2544: 2541: 2538: 2536: 2534: 2532: 2529: 2527: 2525: 2522: 2519: 2517: 2514: 2512: 2509: 2507: 2504: 2502: 2499: 2496: 2493: 2491: 2489: 2487: 2484: 2481: 2478: 2474: 2473: 2470: 2468: 2466: 2463: 2460: 2458: 2455: 2453: 2450: 2448: 2445: 2443: 2440: 2437: 2434: 2432: 2430: 2428: 2425: 2423: 2421: 2418: 2415: 2413: 2410: 2408: 2405: 2403: 2400: 2398: 2395: 2392: 2389: 2387: 2385: 2383: 2380: 2377: 2374: 2370: 2369: 2366: 2364: 2362: 2359: 2356: 2354: 2351: 2349: 2346: 2344: 2341: 2339: 2336: 2333: 2330: 2328: 2326: 2324: 2321: 2319: 2317: 2314: 2311: 2309: 2306: 2304: 2301: 2299: 2296: 2294: 2291: 2288: 2285: 2283: 2281: 2279: 2276: 2273: 2270: 2266: 2265: 2262: 2260: 2258: 2255: 2252: 2250: 2247: 2245: 2242: 2240: 2237: 2235: 2232: 2229: 2226: 2224: 2222: 2220: 2217: 2215: 2213: 2210: 2207: 2205: 2202: 2200: 2197: 2195: 2192: 2190: 2187: 2184: 2181: 2179: 2177: 2175: 2172: 2169: 2166: 2162: 2161: 2158: 2156: 2154: 2151: 2148: 2146: 2143: 2141: 2138: 2136: 2133: 2131: 2128: 2125: 2122: 2120: 2118: 2116: 2113: 2111: 2109: 2106: 2103: 2101: 2098: 2096: 2093: 2091: 2088: 2086: 2083: 2080: 2077: 2075: 2073: 2071: 2068: 2065: 2062: 2058: 2057: 2054: 2052: 2050: 2047: 2044: 2042: 2039: 2037: 2034: 2032: 2029: 2027: 2024: 2021: 2018: 2016: 2014: 2012: 2009: 2007: 2005: 2002: 1999: 1997: 1994: 1992: 1989: 1987: 1984: 1982: 1979: 1976: 1973: 1971: 1969: 1967: 1964: 1961: 1958: 1954: 1953: 1950: 1947: 1944: 1941: 1938: 1935: 1932: 1929: 1926: 1923: 1920: 1917: 1914: 1911: 1908: 1905: 1902: 1900: 1897: 1894: 1891: 1888: 1885: 1882: 1879: 1876: 1873: 1870: 1867: 1864: 1861: 1858: 1855: 1852: 1849: 1847: 1844: 1841: 1838: 1834: 1833: 1831: 1829: 1827: 1825: 1823: 1821: 1819: 1817: 1815: 1813: 1810: 1808: 1806: 1804: 1802: 1800: 1798: 1796: 1794: 1792: 1790: 1788: 1786: 1784: 1782: 1780: 1778: 1776: 1773: 1771: 1769: 1767: 1765: 1763: 1761: 1759: 1757: 1755: 1753: 1724: 1723: 1717:to the first. 1706: 1705: 1694: 1683: 1647: 1644: 1641: 1640: 1637: 1634: 1631: 1628: 1625: 1622: 1619: 1616: 1613: 1609: 1608: 1605: 1602: 1599: 1596: 1593: 1590: 1587: 1584: 1581: 1577: 1576: 1573: 1570: 1567: 1564: 1561: 1558: 1555: 1552: 1549: 1545: 1544: 1541: 1538: 1535: 1532: 1529: 1526: 1523: 1520: 1517: 1513: 1512: 1509: 1506: 1503: 1502:(b ∨ a) 1500: 1497: 1494: 1491: 1488: 1485: 1481: 1480: 1477: 1474: 1471: 1468: 1465: 1462: 1459: 1456: 1452: 1451: 1448: 1446: 1444: 1442: 1440: 1438: 1436: 1433: 1432: 1429: 1427: 1425: 1422: 1419: 1417: 1415: 1413: 1411: 1369: 1366: 1363: 1362: 1359: 1356: 1353: 1350: 1347: 1344: 1341: 1338: 1335: 1332: 1329: 1325: 1324: 1321: 1318: 1315: 1312: 1309: 1306: 1303: 1300: 1297: 1294: 1291: 1287: 1286: 1283: 1280: 1277: 1274: 1271: 1268: 1265: 1262: 1259: 1256: 1253: 1249: 1248: 1245: 1242: 1239: 1236: 1233: 1230: 1227: 1224: 1221: 1218: 1215: 1211: 1210: 1207: 1204: 1201: 1200:(f = formula) 1198: 1195: 1192: 1191:(b ∨ a) 1189: 1188:(b ∧ a) 1186: 1183: 1180: 1177: 1173: 1172: 1169: 1166: 1163: 1160: 1153: 1150: 1147: 1144: 1141: 1138: 1134: 1133: 1131: 1129: 1127: 1125: 1124:biconditional 1122: 1119: 1116: 1113: 1110: 1107: 1105: 1102: 1101: 1099: 1097: 1095: 1093: 1090: 1087: 1084: 1082: 1080: 1078: 1076: 1073: 1072: 1070: 1068: 1066: 1064: 1061: 1058: 1056: 1054: 1052: 1050: 1048: 1045: 1044: 1042: 1040: 1038: 1036: 1033: 1030: 1028: 1026: 1024: 1022: 1020: 1017: 1016: 1014: 1012: 1010: 1008: 1006: 1003: 1001: 999: 997: 995: 993: 977: 974: 973: 972: 960: 949: 946: 943: 940: 928: 925: 922: 919: 916: 896: 876: 856: 853: 850: 847: 844: 841: 838: 827: 815: 812: 792: 772: 769: 688: 685: 646: 643: 640: 639: 636: 633: 630: 628: 625: 622: 619: 615: 614: 611: 608: 605: 603: 600: 597: 594: 590: 589: 586: 583: 580: 578: 575: 572: 569: 565: 564: 561: 558: 555: 553: 550: 547: 544: 540: 539: 536: 533: 530: 528: 525: 522: 519: 515: 514: 511: 508: 505: 503: 500: 497: 494: 490: 489: 486: 483: 480: 478: 475: 472: 469: 465: 464: 461: 458: 455: 453: 450: 447: 444: 440: 439: 436: 433: 430: 428: 425: 422: 419: 413: 412: 408: 390:logic circuits 386: 385: 361: 358: 324: 323: 282: 280: 273: 267: 264: 258: 255: 254: 253: 241: 240: 233:Boolean values 225: 224: 223: 222: 187: 184: 180: 179: 159: 158: 137: 134: 96: 95: 15: 9: 6: 4: 3: 2: 13369: 13358: 13355: 13353: 13350: 13348: 13345: 13343: 13340: 13338: 13335: 13333: 13330: 13329: 13327: 13314: 13313: 13308: 13300: 13294: 13291: 13289: 13286: 13284: 13281: 13279: 13276: 13272: 13269: 13268: 13267: 13264: 13262: 13259: 13257: 13254: 13252: 13248: 13245: 13243: 13240: 13238: 13235: 13233: 13230: 13228: 13225: 13224: 13222: 13218: 13212: 13209: 13207: 13204: 13202: 13201:Recursive set 13199: 13197: 13194: 13192: 13189: 13187: 13184: 13182: 13179: 13175: 13172: 13170: 13167: 13165: 13162: 13160: 13157: 13155: 13152: 13151: 13150: 13147: 13145: 13142: 13140: 13137: 13135: 13132: 13130: 13127: 13125: 13122: 13121: 13119: 13117: 13113: 13107: 13104: 13102: 13099: 13097: 13094: 13092: 13089: 13087: 13084: 13082: 13079: 13077: 13074: 13070: 13067: 13065: 13062: 13060: 13057: 13056: 13055: 13052: 13050: 13047: 13045: 13042: 13040: 13037: 13035: 13032: 13030: 13027: 13023: 13020: 13019: 13018: 13015: 13011: 13010:of arithmetic 13008: 13007: 13006: 13003: 12999: 12996: 12994: 12991: 12989: 12986: 12984: 12981: 12979: 12976: 12975: 12974: 12971: 12967: 12964: 12962: 12959: 12958: 12957: 12954: 12953: 12951: 12949: 12945: 12939: 12936: 12934: 12931: 12929: 12926: 12924: 12921: 12918: 12917:from ZFC 12914: 12911: 12909: 12906: 12900: 12897: 12896: 12895: 12892: 12890: 12887: 12885: 12882: 12881: 12880: 12877: 12875: 12872: 12870: 12867: 12865: 12862: 12860: 12857: 12855: 12852: 12850: 12847: 12846: 12844: 12842: 12838: 12828: 12827: 12823: 12822: 12817: 12816:non-Euclidean 12814: 12810: 12807: 12805: 12802: 12800: 12799: 12795: 12794: 12792: 12789: 12788: 12786: 12782: 12778: 12775: 12773: 12770: 12769: 12768: 12764: 12760: 12757: 12756: 12755: 12751: 12747: 12744: 12742: 12739: 12737: 12734: 12732: 12729: 12727: 12724: 12722: 12719: 12718: 12716: 12712: 12711: 12709: 12704: 12698: 12693:Example 12690: 12682: 12677: 12676: 12675: 12672: 12670: 12667: 12663: 12660: 12658: 12655: 12653: 12650: 12648: 12645: 12644: 12643: 12640: 12638: 12635: 12633: 12630: 12628: 12625: 12621: 12618: 12616: 12613: 12612: 12611: 12608: 12604: 12601: 12599: 12596: 12594: 12591: 12589: 12586: 12585: 12584: 12581: 12579: 12576: 12572: 12569: 12567: 12564: 12562: 12559: 12558: 12557: 12554: 12550: 12547: 12545: 12542: 12540: 12537: 12535: 12532: 12530: 12527: 12525: 12522: 12521: 12520: 12517: 12515: 12512: 12510: 12507: 12505: 12502: 12498: 12495: 12493: 12490: 12488: 12485: 12483: 12480: 12479: 12478: 12475: 12473: 12470: 12468: 12465: 12463: 12460: 12456: 12453: 12451: 12450:by definition 12448: 12447: 12446: 12443: 12439: 12436: 12435: 12434: 12431: 12429: 12426: 12424: 12421: 12419: 12416: 12414: 12411: 12410: 12407: 12404: 12402: 12398: 12393: 12387: 12383: 12373: 12370: 12368: 12365: 12363: 12360: 12358: 12355: 12353: 12350: 12348: 12345: 12343: 12340: 12338: 12337:Kripke–Platek 12335: 12333: 12330: 12326: 12323: 12321: 12318: 12317: 12316: 12313: 12312: 12310: 12306: 12298: 12295: 12294: 12293: 12290: 12288: 12285: 12281: 12278: 12277: 12276: 12273: 12271: 12268: 12266: 12263: 12261: 12258: 12256: 12253: 12250: 12246: 12242: 12239: 12235: 12232: 12230: 12227: 12225: 12222: 12221: 12220: 12216: 12213: 12212: 12210: 12208: 12204: 12200: 12192: 12189: 12187: 12184: 12182: 12181:constructible 12179: 12178: 12177: 12174: 12172: 12169: 12167: 12164: 12162: 12159: 12157: 12154: 12152: 12149: 12147: 12144: 12142: 12139: 12137: 12134: 12132: 12129: 12127: 12124: 12122: 12119: 12117: 12114: 12113: 12111: 12109: 12104: 12096: 12093: 12091: 12088: 12086: 12083: 12081: 12078: 12076: 12073: 12071: 12068: 12067: 12065: 12061: 12058: 12056: 12053: 12052: 12051: 12048: 12046: 12043: 12041: 12038: 12036: 12033: 12031: 12027: 12023: 12021: 12018: 12014: 12011: 12010: 12009: 12006: 12005: 12002: 11999: 11997: 11993: 11983: 11980: 11978: 11975: 11973: 11970: 11968: 11965: 11963: 11960: 11958: 11955: 11951: 11948: 11947: 11946: 11943: 11939: 11934: 11933: 11932: 11929: 11928: 11926: 11924: 11920: 11912: 11909: 11907: 11904: 11902: 11899: 11898: 11897: 11894: 11892: 11889: 11887: 11884: 11882: 11879: 11877: 11874: 11872: 11869: 11867: 11864: 11863: 11861: 11859: 11858:Propositional 11855: 11849: 11846: 11844: 11841: 11839: 11836: 11834: 11831: 11829: 11826: 11824: 11821: 11817: 11814: 11813: 11812: 11809: 11807: 11804: 11802: 11799: 11797: 11794: 11792: 11789: 11787: 11786:Logical truth 11784: 11782: 11779: 11778: 11776: 11774: 11770: 11767: 11765: 11761: 11755: 11752: 11750: 11747: 11745: 11742: 11740: 11737: 11735: 11732: 11730: 11726: 11722: 11718: 11716: 11713: 11711: 11708: 11706: 11702: 11699: 11698: 11696: 11694: 11688: 11683: 11677: 11674: 11672: 11669: 11667: 11664: 11662: 11659: 11657: 11654: 11652: 11649: 11647: 11644: 11642: 11639: 11637: 11634: 11632: 11629: 11627: 11624: 11622: 11619: 11615: 11612: 11611: 11610: 11607: 11606: 11604: 11600: 11596: 11589: 11584: 11582: 11577: 11575: 11570: 11569: 11566: 11559: 11554: 11550: 11549: 11540: 11533: 11530: 11526: 11522: 11517: 11511: 11507: 11504: 11503:0-674-32449-8 11500: 11496: 11491: 11487: 11484: 11483:0-486-28462-X 11480: 11476: 11471: 11470:Alfred Tarski 11467: 11464: 11460: 11456: 11453: 11452:0-486-40687-3 11449: 11445: 11440: 11436: 11433: 11432:0-486-45018-X 11429: 11425: 11420: 11416: 11413: 11408: 11404: 11401: 11400:Willard Quine 11397: 11392: 11387: 11384: 11383:0-521-21838-1 11380: 11376: 11369: 11366: 11362: 11358: 11353: 11349: 11346: 11345:0-486-45894-6 11342: 11338: 11331: 11329: 11328:0-12-238452-0 11325: 11321: 11316: 11312: 11309: 11308:0-486-43946-1 11305: 11301: 11290: 11286: 11282: 11278: 11274: 11272:0-486-44617-4 11268: 11264: 11260: 11256: 11255: 11241: 11234: 11230: 11223: 11214: 11207: 11200: 11193: 11189: 11185: 11181: 11177: 11173: 11169: 11165: 11161: 11157: 11153: 11149: 11145: 11141: 11137: 11133: 11128: 11124: 11118: 11108: 11099: 11092: 11086: 11077: 11067: 11061:, p. 32. 11060: 11055: 11048: 11038: 11028: 11019: 11012: 11006: 10999: 10994: 10985: 10976: 10969: 10968:0-444-00259-6 10965: 10961: 10956: 10950: 10940: 10933: 10929: 10924: 10918: 10914: 10910: 10906: 10902: 10896: 10889: 10882: 10873: 10866: 10861: 10852: 10848: 10832: 10825: 10824:intuitionists 10819: 10815: 10804: 10801: 10797: 10794: 10791: 10787: 10783: 10782:Willard Quine 10780: 10777: 10774: 10771: 10770: 10748: 10730: 10729: 10707: 10703: 10702: 10698: 10695: 10692: 10688: 10685: 10684: 10683: 10681: 10674: 10671: 10668: 10665: 10661: 10658: 10657: 10656: 10654: 10650: 10646: 10642: 10638: 10634: 10633:Gottlob Frege 10627: 10623: 10622: 10621: 10618: 10616: 10612: 10608: 10604: 10600: 10596: 10592: 10588: 10584: 10580: 10575: 10573: 10562: 10559: 10556: 10555: 10553: 10552: 10551: 10549: 10545: 10541: 10537: 10533: 10517: 10514: 10512: 10510: 10508: 10506: 10504: 10501: 10499: 10496: 10493: 10490: 10488: 10486: 10483: 10480: 10477: 10475: 10472: 10470: 10467: 10464: 10461: 10459: 10457: 10454: 10451: 10448: 10440: 10437: 10435: 10433: 10431: 10429: 10427: 10424: 10422: 10419: 10416: 10413: 10411: 10409: 10406: 10403: 10400: 10398: 10395: 10393: 10390: 10387: 10384: 10382: 10380: 10377: 10374: 10371: 10363: 10361: 10359: 10357: 10355: 10353: 10351: 10348: 10346: 10343: 10340: 10337: 10335: 10333: 10330: 10327: 10324: 10322: 10319: 10317: 10314: 10311: 10308: 10306: 10304: 10301: 10298: 10295: 10287: 10284: 10282: 10280: 10278: 10276: 10274: 10271: 10269: 10266: 10263: 10260: 10258: 10256: 10253: 10250: 10247: 10245: 10242: 10240: 10237: 10234: 10231: 10229: 10227: 10224: 10221: 10218: 10210: 10208: 10206: 10204: 10202: 10200: 10198: 10195: 10193: 10190: 10187: 10184: 10182: 10180: 10177: 10174: 10171: 10169: 10166: 10164: 10161: 10158: 10155: 10153: 10151: 10148: 10145: 10142: 10134: 10131: 10129: 10127: 10125: 10123: 10121: 10118: 10116: 10113: 10110: 10107: 10105: 10103: 10100: 10097: 10094: 10092: 10089: 10087: 10084: 10081: 10078: 10076: 10074: 10071: 10068: 10065: 10055: 10052: 10050: 10048: 10046: 10044: 10042: 10039: 10037: 10034: 10031: 10028: 10026: 10024: 10021: 10018: 10015: 10013: 10010: 10008: 10005: 10002: 9999: 9997: 9995: 9992: 9989: 9986: 9978: 9975: 9973: 9971: 9969: 9967: 9965: 9962: 9960: 9957: 9954: 9951: 9949: 9947: 9944: 9941: 9938: 9936: 9933: 9931: 9928: 9925: 9922: 9920: 9918: 9915: 9912: 9909: 9901: 9898: 9895: 9892: 9889: 9886: 9883: 9880: 9877: 9874: 9871: 9868: 9865: 9862: 9859: 9856: 9853: 9850: 9847: 9844: 9841: 9838: 9835: 9832: 9829: 9826: 9823: 9820: 9750: 9747: 9740: 9736: 9732: 9729: 9725: 9721: 9720: 9718: 9717: 9716: 9702: 9699: 9697: 9695: 9693: 9690: 9688: 9685: 9682: 9679: 9677: 9674: 9671: 9669: 9666: 9663: 9655: 9652: 9650: 9648: 9646: 9643: 9641: 9638: 9635: 9632: 9630: 9627: 9624: 9622: 9619: 9616: 9608: 9606: 9604: 9602: 9600: 9597: 9595: 9592: 9589: 9586: 9584: 9581: 9578: 9576: 9573: 9570: 9562: 9559: 9557: 9555: 9553: 9550: 9548: 9545: 9542: 9539: 9537: 9534: 9531: 9529: 9526: 9523: 9515: 9513: 9511: 9509: 9507: 9504: 9502: 9499: 9496: 9493: 9491: 9488: 9485: 9483: 9480: 9477: 9469: 9467: 9465: 9463: 9461: 9458: 9456: 9453: 9450: 9447: 9445: 9442: 9439: 9437: 9434: 9431: 9423: 9420: 9418: 9416: 9414: 9411: 9409: 9406: 9403: 9400: 9398: 9395: 9392: 9390: 9387: 9384: 9376: 9373: 9371: 9369: 9367: 9364: 9362: 9359: 9356: 9353: 9351: 9348: 9345: 9343: 9340: 9337: 9330: 9327: 9324: 9321: 9318: 9315: 9312: 9309: 9306: 9303: 9300: 9297: 9294: 9291: 9288: 9285: 9241: 9238: 9233: 9218: 9215: 9213: 9210: 9207: 9204: 9202: 9199: 9191: 9188: 9186: 9183: 9180: 9177: 9175: 9172: 9164: 9162: 9160: 9157: 9154: 9151: 9149: 9146: 9139:state 0, s=0 9138: 9135: 9133: 9130: 9127: 9124: 9122: 9119: 9112: 9109: 9106: 9103: 9100: 9097: 9094: 9091: 9063: 9061: 9060:state diagram 9050: 9048: 9038: 9025: 9018: 9014: 9010: 9004: 8990: 8987: 8985: 8982: 8980: 8977: 8975: 8972: 8964: 8961: 8959: 8956: 8954: 8951: 8949: 8946: 8938: 8935: 8933: 8930: 8928: 8925: 8923: 8920: 8912: 8909: 8907: 8904: 8902: 8899: 8897: 8894: 8887: 8884: 8881: 8878: 8875: 8872: 8869: 8866: 8838: 8834: 8832: 8828: 8821: 8812: 8809: 8807: 8804: 8802: 8799: 8797: 8789: 8786: 8784: 8781: 8779: 8776: 8774: 8767: 8764: 8761: 8758: 8755: 8752: 8750: 8724: 8715: 8713: 8709: 8705: 8701: 8697: 8692: 8689: 8685: 8680: 8676: 8667: 8665: 8661: 8656: 8654: 8646: 8645: 8644: 8637: 8636: 8635: 8571: 8568: 8566: 8563: 8561: 8558: 8555: 8552: 8550: 8547: 8545: 8542: 8539: 8536: 8534: 8531: 8529: 8526: 8523: 8520: 8518: 8516: 8513: 8510: 8507: 8504: 8497: 8495: 8492: 8490: 8487: 8484: 8481: 8479: 8476: 8474: 8471: 8468: 8465: 8463: 8460: 8458: 8455: 8452: 8449: 8447: 8445: 8442: 8439: 8436: 8433: 8426: 8424: 8421: 8419: 8416: 8413: 8410: 8408: 8405: 8403: 8400: 8397: 8394: 8392: 8389: 8387: 8384: 8381: 8378: 8376: 8374: 8371: 8368: 8365: 8362: 8355: 8353: 8350: 8348: 8345: 8342: 8339: 8337: 8334: 8332: 8329: 8326: 8323: 8321: 8318: 8316: 8313: 8310: 8307: 8305: 8303: 8300: 8297: 8294: 8291: 8284: 8282: 8279: 8277: 8274: 8271: 8268: 8266: 8263: 8261: 8258: 8255: 8252: 8250: 8247: 8245: 8242: 8239: 8236: 8234: 8232: 8229: 8226: 8223: 8220: 8213: 8211: 8208: 8206: 8203: 8200: 8197: 8195: 8192: 8190: 8187: 8184: 8181: 8179: 8176: 8174: 8171: 8168: 8165: 8163: 8161: 8158: 8155: 8152: 8149: 8142: 8140: 8137: 8135: 8132: 8129: 8126: 8124: 8121: 8119: 8116: 8113: 8110: 8108: 8105: 8103: 8100: 8097: 8094: 8092: 8090: 8087: 8084: 8081: 8078: 8071: 8069: 8066: 8064: 8061: 8058: 8055: 8053: 8050: 8048: 8045: 8042: 8039: 8037: 8034: 8032: 8029: 8026: 8023: 8021: 8019: 8016: 8013: 8010: 8007: 7927: 7909: 7906: 7905: 7904: 7903: 7902: 7901: 7897: 7896: 7888: 7887: 7886: 7885: 7884: 7883: 7879: 7878: 7870: 7869: 7868: 7867: 7866: 7865: 7861: 7860: 7852: 7849: 7846: 7844: 7841: 7840: 7839: 7838: 7837: 7836: 7832: 7831: 7823: 7822: 7821: 7820: 7819: 7818: 7814: 7813: 7805: 7802: 7801: 7800: 7799: 7798: 7797: 7793: 7792: 7791: 7784: 7783: 7782: 7779: 7775: 7773: 7763: 7755: 7681: 7602: 7523: 7445: 7366: 7287: 7209: 7131: 7053: 7049: 7046: 6965: 6958: 6948: 6947: 6946: 6945: 6944: 6943: 6942: 6937: 6935: 6930: 6929: 6928: 6920: 6917: 6916:Venn diagrams 6902: 6899: 6896: 6893: 6885: 6882: 6879: 6876: 6868: 6865: 6862: 6859: 6851: 6848: 6845: 6842: 6834: 6831: 6828: 6825: 6817: 6814: 6811: 6808: 6800: 6797: 6794: 6791: 6783: 6780: 6777: 6774: 6766: 6763: 6760: 6757: 6749: 6746: 6743: 6740: 6733: 6729: 6727: 6726:Karnaugh maps 6723: 6719: 6715: 6711: 6694: 6687: 6686: 6684: 6683: 6682: 6678: 6676: 6671: 6669: 6653: 6650: 6649: 6647: 6646: 6645: 6643: 6633: 6631: 6626: 6625:Karnaugh maps 6622: 6611: 6602: 6600: 6596: 6592: 6578: 6576: 6573: 6570: 6568: 6565: 6563: 6560: 6558: 6555: 6553: 6551: 6548: 6545: 6543: 6540: 6538: 6535: 6533: 6530: 6528: 6525: 6522: 6519: 6517: 6515: 6513: 6511: 6508: 6505: 6502: 6495: 6493: 6490: 6487: 6485: 6482: 6480: 6477: 6475: 6472: 6470: 6468: 6465: 6462: 6460: 6457: 6455: 6452: 6450: 6447: 6445: 6442: 6439: 6436: 6434: 6432: 6430: 6428: 6425: 6422: 6419: 6412: 6410: 6407: 6404: 6402: 6399: 6397: 6394: 6392: 6389: 6387: 6385: 6382: 6379: 6377: 6374: 6372: 6369: 6367: 6364: 6362: 6359: 6356: 6353: 6351: 6349: 6347: 6345: 6342: 6339: 6336: 6329: 6327: 6324: 6321: 6319: 6316: 6314: 6311: 6309: 6306: 6304: 6302: 6299: 6296: 6294: 6291: 6289: 6286: 6284: 6281: 6279: 6276: 6273: 6270: 6268: 6266: 6264: 6262: 6259: 6256: 6253: 6245: 6242: 6239: 6236: 6233: 6230: 6227: 6224: 6221: 6218: 6215: 6212: 6209: 6206: 6203: 6200: 6197: 6194: 6191: 6188: 6185: 6182: 6179: 6176: 6173: 6170: 6167: 6165: 6162: 6159: 6156: 6083: 6080: 6071: 6067: 6064: 6061: 6058: 6055: 6052: 6049: 6046: 6043: 6042: 6041: 6040: 6039: 6037: 6029: 6026: 6023: 6020: 6017: 6016: 6015: 6013: 5932: 5922: 5902: 5894: 5883: 5877: 5867: 5866: 5865: 5819: 5816: 5813: 5810: 5809: 5808: 5806: 5802: 5798: 5788: 5771: 5768: 5765: 5736: 5704: 5701: 5672: 5669: 5651: 5638: 5635: 5632: 5630: 5627: 5624: 5622: 5619: 5616: 5613: 5611: 5609: 5607: 5605: 5602: 5595: 5592: 5589: 5587: 5584: 5581: 5579: 5576: 5573: 5570: 5568: 5566: 5564: 5562: 5559: 5552: 5549: 5546: 5544: 5541: 5538: 5536: 5533: 5530: 5527: 5525: 5523: 5521: 5519: 5516: 5509: 5506: 5503: 5501: 5498: 5495: 5493: 5490: 5487: 5484: 5482: 5480: 5478: 5476: 5473: 5465: 5462: 5459: 5456: 5453: 5450: 5447: 5444: 5441: 5438: 5435: 5432: 5429: 5427: 5424: 5375: 5372: 5371: 5369: 5364: 5361: 5357: 5354: 5350: 5346: 5342: 5337: 5334: 5333: 5332: 5331: 5328: 5327: 5326: 5324: 5320: 5316: 5312: 5308: 5303: 5134: 4974: 4972: 4967: 4965: 4961: 4959: 4955: 4951: 4947: 4943: 4916: 4794: 4792: 4788: 4783: 4781: 4777: 4773: 4760: 4759: 4751: 4747: 4745: 4741: 4738: 4735: 4732: 4729: 4726: 4725: 4720: 4717: 4714: 4712: 4710: 4707: 4705: 4702: 4699: 4696: 4694: 4692: 4690: 4683: 4680: 4677: 4675: 4673: 4670: 4668: 4665: 4662: 4659: 4657: 4655: 4653: 4645: 4642: 4639: 4636: 4633: 4630: 4627: 4624: 4621: 4618: 4615: 4612: 4610: 4573: 4570: 4554: 4551: 4550: 4549: 4538: 4535: 4534: 4533: 4522: 4519: 4518: 4517: 4509: 4507: 4503: 4499: 4493: 4492: 4491: 4489: 4482: 4479: 4476: 4473: 4472: 4471: 4469: 4465: 4449: 4448: 4446: 4439: 4436: 4433: 4430: 4427: 4426: 4425: 4424: 4422: 4419: 4418: 4417: 4409: 4406: 4403: 4400: 4397: 4394: 4391: 4388: 4385: 4382: 4379: 4376: 4373: 4370: 4367: 4364: 4361: 4358: 4356:(IMPLICATION) 4355: 4352: 4349: 4346: 4345: 4344: 4343: 4342: 4333: 4331: 4330:axiom schemas 4326: 4318: 4316: 4314: 4311: 4309: 4306: 4303: 4301: 4298: 4296: 4293: 4291: 4288: 4286: 4283: 4280: 4277: 4275: 4272: 4270: 4268: 4265: 4258: 4256: 4254: 4251: 4249: 4246: 4243: 4241: 4238: 4236: 4233: 4231: 4228: 4226: 4223: 4220: 4217: 4215: 4212: 4210: 4208: 4205: 4198: 4196: 4194: 4191: 4189: 4186: 4183: 4181: 4178: 4176: 4173: 4171: 4168: 4166: 4163: 4160: 4157: 4155: 4152: 4150: 4148: 4145: 4138: 4136: 4134: 4131: 4129: 4126: 4123: 4121: 4118: 4116: 4113: 4111: 4108: 4106: 4103: 4100: 4097: 4095: 4092: 4090: 4088: 4085: 4077: 4074: 4071: 4068: 4065: 4062: 4059: 4056: 4053: 4050: 4047: 4044: 4041: 4038: 4035: 4032: 4029: 4026: 4023: 4020: 4018: 4015: 3960: 3953: 3952: 3951: 3948: 3937: 3935: 3931: 3924: 3840: 3808: 3805: 3802: 3776: 3773: 3770: 3762: 3745: 3741: 3737: 3719: 3690: 3665: 3661: 3660: 3659: 3657: 3650: 3643: 3639: 3632: 3628: 3623: 3602: 3596: 3593: 3590: 3587: 3567: 3547: 3527: 3504: 3500: 3496: 3486: 3471: 3448: 3435: 3432: 3431: 3430: 3428: 3409: 3403: 3400: 3397: 3394: 3391: 3380: 3364: 3361: 3358: 3355: 3352: 3351: 3349: 3345:( ~(~a) ≡ a ) 3342: 3335: 3332: 3329: 3328: 3326: 3325: 3324: 3322: 3318: 3293: 3292: 3282: 3281: 3280: 3278: 3260: 3248: 3247: 3241: 3240: 3239: 3236: 3232: 3228: 3221: 3206: 3199: 3192: 3190:(a ∨ b) 3185: 3178: 3177: 3176: 3175: 3174: 3160: 3157: 3156:Karnaugh maps 3151: 3142: 3140: 3136: 3132: 3123: 3120: 3117: 3114: 3108: 3105: 3102: 3099: 3093: 3090: 3087: 3084: 3078: 3075: 3072: 3069: 3062: 3059: 3056: 3053: 3033: 3031: 3027: 3026: 3021: 3020: 3015: 3014: 3009: 3005: 3002: 2998: 2994: 2990: 2989: 2984: 2983: 2973: 2966: 2964: 2961: 2957: 2953: 2949: 2945: 2941: 2937: 2934: 2933: 2926: 2919: 2917: 2914: 2910: 2906: 2902: 2899: 2898: 2895: 2881: 2880: 2875: 2871: 2867: 2863: 2859: 2854: 2852: 2835: 2831: 2829: 2828:Leibniz's law 2825: 2814: 2813: 2811: 2807: 2806: 2805: 2802: 2798: 2783: 2781: 2779: 2776: 2773: 2771: 2768: 2766: 2763: 2761: 2758: 2756: 2753: 2750: 2747: 2745: 2743: 2741: 2738: 2736: 2734: 2731: 2728: 2726: 2723: 2721: 2718: 2716: 2713: 2711: 2708: 2705: 2702: 2700: 2698: 2696: 2693: 2690: 2687: 2679: 2677: 2675: 2672: 2669: 2667: 2664: 2662: 2659: 2657: 2654: 2652: 2649: 2646: 2643: 2641: 2639: 2637: 2634: 2632: 2630: 2627: 2624: 2622: 2619: 2617: 2614: 2612: 2609: 2607: 2604: 2601: 2598: 2596: 2594: 2592: 2589: 2586: 2583: 2575: 2573: 2571: 2568: 2565: 2563: 2560: 2558: 2555: 2553: 2550: 2548: 2545: 2542: 2539: 2537: 2535: 2533: 2530: 2528: 2526: 2523: 2520: 2518: 2515: 2513: 2510: 2508: 2505: 2503: 2500: 2497: 2494: 2492: 2490: 2488: 2485: 2482: 2479: 2471: 2469: 2467: 2464: 2461: 2459: 2456: 2454: 2451: 2449: 2446: 2444: 2441: 2438: 2435: 2433: 2431: 2429: 2426: 2424: 2422: 2419: 2416: 2414: 2411: 2409: 2406: 2404: 2401: 2399: 2396: 2393: 2390: 2388: 2386: 2384: 2381: 2378: 2375: 2367: 2365: 2363: 2360: 2357: 2355: 2352: 2350: 2347: 2345: 2342: 2340: 2337: 2334: 2331: 2329: 2327: 2325: 2322: 2320: 2318: 2315: 2312: 2310: 2307: 2305: 2302: 2300: 2297: 2295: 2292: 2289: 2286: 2284: 2282: 2280: 2277: 2274: 2271: 2263: 2261: 2259: 2256: 2253: 2251: 2248: 2246: 2243: 2241: 2238: 2236: 2233: 2230: 2227: 2225: 2223: 2221: 2218: 2216: 2214: 2211: 2208: 2206: 2203: 2201: 2198: 2196: 2193: 2191: 2188: 2185: 2182: 2180: 2178: 2176: 2173: 2170: 2167: 2159: 2157: 2155: 2152: 2149: 2147: 2144: 2142: 2139: 2137: 2134: 2132: 2129: 2126: 2123: 2121: 2119: 2117: 2114: 2112: 2110: 2107: 2104: 2102: 2099: 2097: 2094: 2092: 2089: 2087: 2084: 2081: 2078: 2076: 2074: 2072: 2069: 2066: 2063: 2055: 2053: 2051: 2048: 2045: 2043: 2040: 2038: 2035: 2033: 2030: 2028: 2025: 2022: 2019: 2017: 2015: 2013: 2010: 2008: 2006: 2003: 2000: 1998: 1995: 1993: 1990: 1988: 1985: 1983: 1980: 1977: 1974: 1972: 1970: 1968: 1965: 1962: 1959: 1951: 1948: 1945: 1942: 1939: 1936: 1933: 1930: 1927: 1924: 1921: 1918: 1915: 1912: 1909: 1906: 1903: 1901: 1898: 1895: 1892: 1889: 1886: 1883: 1880: 1877: 1874: 1871: 1868: 1865: 1862: 1859: 1856: 1853: 1850: 1848: 1845: 1842: 1839: 1748: 1746: 1742: 1737: 1731: 1729: 1720: 1719: 1718: 1716: 1712: 1703: 1699: 1695: 1692: 1688: 1684: 1681: 1677: 1673: 1672: 1671: 1668: 1666: 1662: 1657: 1653: 1638: 1635: 1632: 1629: 1626: 1623: 1620: 1617: 1614: 1610: 1606: 1603: 1600: 1597: 1594: 1591: 1588: 1585: 1582: 1578: 1574: 1571: 1568: 1565: 1562: 1559: 1556: 1553: 1550: 1546: 1542: 1539: 1536: 1533: 1530: 1527: 1524: 1521: 1518: 1514: 1510: 1507: 1505:~(b & a) 1504: 1501: 1498: 1495: 1492: 1489: 1486: 1482: 1478: 1475: 1472: 1469: 1466: 1463: 1460: 1453: 1450:exclusive OR 1449: 1447: 1445: 1443: 1441: 1439: 1437: 1434: 1430: 1428: 1426: 1418: 1416: 1414: 1412: 1409: 1406: 1404: 1400: 1396: 1392: 1388: 1387:Karnaugh maps 1384: 1374: 1360: 1357: 1354: 1351: 1348: 1345: 1342: 1339: 1336: 1333: 1330: 1322: 1319: 1316: 1313: 1310: 1307: 1304: 1301: 1298: 1295: 1292: 1284: 1281: 1278: 1275: 1272: 1269: 1266: 1263: 1260: 1257: 1254: 1246: 1243: 1240: 1237: 1234: 1231: 1228: 1225: 1222: 1219: 1216: 1208: 1205: 1202: 1199: 1196: 1193: 1190: 1187: 1184: 1181: 1178: 1171:exclusive OR 1170: 1167: 1164: 1161: 1158: 1154: 1151: 1148: 1145: 1142: 1139: 1132: 1130: 1128: 1126: 1123: 1120: 1117: 1114: 1111: 1108: 1106: 1100: 1098: 1096: 1094: 1091: 1088: 1086:inclusive OR 1085: 1083: 1081: 1079: 1077: 1071: 1069: 1067: 1065: 1062: 1059: 1057: 1055: 1053: 1051: 1049: 1043: 1041: 1039: 1037: 1034: 1031: 1029: 1027: 1025: 1023: 1021: 988: 985: 983: 950: 947: 944: 941: 923: 917: 894: 874: 851: 845: 842: 839: 836: 828: 826:is a formula. 813: 790: 782: 781: 780: 778: 768: 764: 762: 758: 754: 750: 745: 744: 740: 733: 729: 723: 719: 715: 711: 707: 703: 698: 697: 693: 684: 682: 678: 674: 670: 666: 662: 658: 654: 653: 637: 634: 631: 629: 626: 623: 620: 617: 616: 612: 609: 606: 604: 601: 598: 595: 592: 591: 587: 584: 581: 579: 576: 573: 570: 567: 566: 562: 559: 556: 554: 551: 548: 545: 542: 541: 537: 534: 531: 529: 526: 523: 520: 517: 516: 512: 509: 506: 504: 501: 498: 495: 492: 491: 487: 484: 481: 479: 476: 473: 470: 467: 466: 462: 459: 456: 454: 451: 448: 445: 442: 441: 437: 434: 431: 429: 426: 423: 420: 417: 416: 406: 405: 404: 402: 398: 393: 391: 383: 379: 375: 374: 373: 371: 367: 364:Analysis: In 357: 355: 350: 348: 342: 338: 336: 332: 320: 317: 309: 299: 295: 289: 288: 283:This section 281: 272: 271: 263: 251: 250: 249: 246: 238: 237: 236: 234: 230: 220: 219: 217: 213: 212: 211: 209: 208:concatenation 205: 201: 197: 193: 183: 177: 176: 175: 172: 168: 164: 155: 154: 153: 151: 147: 143: 133: 130: 126: 121: 120:formal object 117: 113: 109: 105: 101: 93: 89: 85: 81: 77: 76: 75: 73: 69: 65: 61: 57: 52: 50: 46: 42: 38: 34: 30: 26: 22: 16:Logic formula 13352:Propositions 13303: 13101:Ultraproduct 12948:Model theory 12913:Independence 12849:Formal proof 12841:Proof theory 12824: 12797: 12754:real numbers 12726:second-order 12637:Substitution 12514:Metalanguage 12455:conservative 12428:Axiom schema 12372:Constructive 12342:Morse–Kelley 12308:Set theories 12287:Aleph number 12280:inaccessible 12186:Grothendieck 12070:intersection 11957:Higher-order 11945:Second-order 11891:Truth tables 11885: 11848:Venn diagram 11631:Formal proof 11538: 11520: 11494: 11474: 11462: 11443: 11423: 11422:1969, 1997, 11411: 11395: 11374: 11356: 11336: 11319: 11299: 11284: 11262: 11240: 11228: 11222: 11213: 11205: 11199: 11191: 11187: 11183: 11179: 11175: 11171: 11167: 11166:), l.u.b. = 11163: 11159: 11155: 11151: 11148:Dedekind cut 11143: 11139: 11117: 11107: 11098: 11090: 11085: 11076: 11066: 11054: 11047:metalanguage 11037: 11027: 11018: 11010: 11005: 10993: 10988:Robbin p. 3. 10984: 10975: 10959: 10954: 10949: 10939: 10923: 10912: 10900: 10895: 10887: 10881: 10872: 10860: 10851: 10831: 10818: 10786:E. W. Veitch 10691:F. W. Jordan 10679: 10678: 10652: 10631: 10619: 10615:George Boole 10590: 10578: 10576: 10572:Venn diagram 10568: 10530: 9902:Description 9745: 9738: 9734: 9727: 9723: 9713: 9236: 9229: 9056: 9039: 9031: 9012: 9009:total states 9008: 8835: 8831:ad infinitum 8830: 8826: 8825: 8721: 8693: 8681: 8677: 8673: 8657: 8652: 8650: 8641: 8633: 7907: 7851: 7848: 7845: 7803: 7788: 7780: 7776: 7769: 7760: 6956: 6940: 6931: 6926: 6913: 6730: 6707: 6679: 6672: 6664: 6639: 6621:truth tables 6617: 6591:normal forms 6590: 6588: 6585:Normal forms 6077: 6069: 6035: 6033: 5969: 5823: 5814:p → q ≡ p|~q 5804: 5800: 5794: 5657: 5359: 5352: 5348: 5344: 5322: 5321:well-formed 5318: 5314: 5310: 5306: 5299: 4970: 4968: 4963: 4962: 4953: 4949: 4945: 4941: 4917:begins with 4914: 4911: 4784: 4769: 4563: 4547: 4531: 4515: 4501: 4500: 4497: 4487: 4486: 4461: 4415: 4339: 4327: 4323: 3946: 3943: 3933: 3926: 3922: 3920: 3743: 3739: 3663: 3652: 3645: 3641: 3634: 3630: 3624: 3621: 3376: 3320: 3316: 3315: 3277:Substitution 3276: 3275: 3265:(SW2 → CON1) 3258: 3234: 3230: 3224: 3219: 3166: 3152: 3148: 3138: 3128: 3029: 3023: 3017: 3011: 3007: 3003: 3000: 2996: 2992: 2986: 2980: 2978: 2967: 2959: 2955: 2951: 2947: 2943: 2939: 2935: 2920: 2912: 2908: 2904: 2900: 2877: 2873: 2869: 2865: 2857: 2855: 2851:modus ponens 2836: 2832: 2823: 2820: 2809: 2800: 2794: 1740: 1735: 1732: 1725: 1714: 1711:non sequitur 1710: 1707: 1701: 1697: 1690: 1686: 1679: 1675: 1669: 1649: 1499:(b & a) 1424:logical sum 1398: 1390: 1382: 1379: 1152:b IMPLIES a 1121:implication 1118:disjunction 1115:conjunction 1089:IF b THEN a 1005:b only if a 986: 982:truth tables 979: 774: 765: 746: 742: 741: 731: 725: 713: 705: 699: 695: 694: 690: 680: 676: 672: 668: 664: 660: 650: 648: 397:truth tables 394: 387: 370:truth tables 363: 351: 343: 339: 327: 312: 303: 284: 260: 242: 226: 215: 195: 189: 181: 166: 162: 160: 142:propositions 141: 139: 136:Propositions 128: 124: 111: 103: 97: 91: 87: 83: 79: 67: 63: 56:propositions 53: 48: 44: 40: 24: 18: 13211:Type theory 13159:undecidable 13091:Truth value 12978:equivalence 12657:non-logical 12270:Enumeration 12260:Isomorphism 12207:cardinality 12191:Von Neumann 12156:Ultrafilter 12121:Uncountable 12055:equivalence 11972:Quantifiers 11962:Fixed-point 11931:First-order 11811:Consistency 11796:Proposition 11773:Traditional 11744:Lindström's 11734:Compactness 11676:Type theory 11621:Cardinality 11233:Alan Turing 11080:Robbin p. 7 10798:(1955) and 10790:M. Karnaugh 10773:Alan Turing 10662:(1921) and 9028:remains 0). 8718:Oscillation 5349:implication 5307:well-formed 4380:(FOR ALL x) 3932:containing 3317:Replacement 3294:(c & (q 3163:Definitions 2999:) does not 2858:valuation v 1745:multiplexer 1455:row number 1399:logical sum 1168:b stroke a 382:Turing test 248:statement: 221:p|W AND p|B 116:proposition 104:proposition 100:mathematics 86:) IMPLIES ( 37:truth value 33:well formed 13342:Statements 13326:Categories 13022:elementary 12715:arithmetic 12583:Quantifier 12561:functional 12433:Expression 12151:Transitive 12095:identities 12080:complement 12013:hereditary 11996:Set theory 11252:References 11174:, whereas 11146:. Given a 11127:Kurt Gödel 11091:conclusive 11045:is in the 10928:Neural net 10909:David Hume 10905:John Locke 10788:1952, and 10739:) XOR c_in 10664:Jean Nicod 10613:"inspired 10587:John Locke 10583:syllogisms 10538:: (1) The 6714:hypercubes 6018:(c, b, a): 5315:sufficient 5302:inferences 4392:(IDENTITY) 3340:(a → b) ). 2954:) = T and 2810:definition 1458:variables 1203:(a NOR b) 1185:¬(a) 1182:¬(b) 1137:variables 761:comparator 749:robustness 702:empiricist 171:assertions 163:particular 13293:Supertask 13196:Recursion 13154:decidable 12988:saturated 12966:of models 12889:deductive 12884:axiomatic 12804:Hilbert's 12791:Euclidean 12772:canonical 12695:axiomatic 12627:Signature 12556:Predicate 12445:Extension 12367:Ackermann 12292:Operation 12171:Universal 12161:Recursive 12136:Singleton 12131:Inhabited 12116:Countable 12106:Types of 12090:power set 12060:partition 11977:Predicate 11923:Predicate 11838:Syllogism 11828:Soundness 11801:Inference 11791:Tautology 11693:paradoxes 11391:McCluskey 11367:(Boston). 11318:, 2002, 10888:valuation 10843:Citations 10810:Footnotes 10761:) = c_out 10670:Emil Post 10595:semiotics 10536:Aristotle 9719:Examples 9232:flip-flop 9013:transient 8714:, etc.). 8684:black box 8660:paradoxes 7928:Minterms 6966:Minterms 6710:Gray code 6648:Examples 5998:⊤ 5978:⊥ 5947:⊤ 5939:⊤ 5933:≡ 5930:⊥ 5878:≡ 5875:⊤ 5852:⊥ 5832:⊤ 5772:∨ 5766:∧ 5740:¬ 5734:→ 5708:¬ 5702:∨ 5676:¬ 5670:∧ 5311:necessary 4928:¬ 4761:¬(¬a) ≡ a 4447:Example: 3903:↔ 3872:→ 3841:∨ 3806:∧ 3763:∧ 3717:¬ 3683:¬ 3606:↔ 3600:→ 3594:∨ 3588:∧ 3568:◻ 3548:β 3528:α 3505:β 3501:◻ 3497:α 3472:α 3449:α 3446:¬ 3413:↔ 3407:→ 3401:∨ 3395:∧ 3389:¬ 3211:( a ≡ b ) 1159:TO a *** 1112:negation 1109:negation 959:↔ 924:β 921:→ 918:α 895:β 875:α 855:↔ 849:→ 843:∨ 837:∧ 814:α 811:¬ 791:α 714:synthetic 710:tautology 335:semantics 306:June 2021 204:predicate 146:recursive 31:which is 13278:Logicism 13271:timeline 13247:Concrete 13106:Validity 13076:T-schema 13069:Kripke's 13064:Tarski's 13059:semantic 13049:Strength 12998:submodel 12993:spectrum 12961:function 12809:Tarski's 12798:Elements 12785:geometry 12741:Robinson 12662:variable 12647:function 12620:spectrum 12610:Sentence 12566:variable 12509:Language 12462:Relation 12423:Automata 12413:Alphabet 12397:language 12251:-jection 12229:codomain 12215:Function 12176:Universe 12146:Infinite 12050:Relation 11833:Validity 11823:Argument 11721:theorem, 11298:, 2005, 11283:(1952). 11261:(1950). 11138:(l.u.b) 11132:analysis 11032:values." 10901:a priori 10645:antinomy 9848:∨ 9298:∨ 9101:∨ 8991:state 0 8913:state 1 8688:function 7976:∨ 7958:∨ 7850:∨ 7847:∨ 7772:literals 6996:∨ 6750:minterm 6685:Example 6668:minterms 6661:Minterms 6072:Q. E. D. 6012:relation 5811:~p ≡ p|p 3792:returns 3706:returns 3379:Enderton 3306:& ~q 3298:& ~q 3287:& ~q 3259:instance 3253:SW2, b = 3139:complete 2879:function 1922:∨ 1484:b*2+a*2 1383:minterms 1209:various 1197:(b ↔ a) 1194:(b → a) 1146:b AND a 706:analytic 432:(b+a)+ci 257:Identity 200:singular 82:AND NOT 62:such as 45:sentence 13220:Related 13017:Diagram 12915: ( 12894:Hilbert 12879:Systems 12874:Theorem 12752:of the 12697:systems 12477:Formula 12472:Grammar 12388: ( 12332:General 12045:Forcing 12030:Element 11950:Monadic 11725:paradox 11666:Theorem 11602:General 11525:Sheffer 11434:(pbk.). 11125:. Both 10753:& b 10728:) are: 10579:algebra 9042:delayed 9035:delayed 7762:phase. 6716:called 6642:literal 6036:defined 5360:implies 4903:formula 4893:formula 4883:formula 4873:formula 4863:formula 4853:formula 4843:formula 4833:formula 4823:formula 4801:formula 4565:~(a)) = 4506:literal 4365:∨ 3627:closure 3484:is, and 3227:schemas 3220:schemas 3204:(a ⊕ b) 3197:(a → b) 3042:v(A→B) 3030:assigns 2985:) and ( 2864:(wffs) 2860:of any 2801:logical 1736:selects 1663:in the 1149:b OR a 753:digital 712:), and 292:Please 112:denotes 47:, or a 29:formula 12983:finite 12746:Skolem 12699: 12674:Theory 12642:Symbol 12632:String 12615:atomic 12492:ground 12487:closed 12482:atomic 12438:ground 12401:syntax 12297:binary 12224:domain 12141:Finite 11906:finite 11764:Logics 11723: 11671:Theory 11537:1968, 11501: 11481: 11450: 11430: 11410:1967, 11394:1965, 11389:E. J. 11381: 11373:1978, 11363: 11343: 11326: 11306: 11269: 11206:formal 10966: 9872:& 9857:& 9839:& 9307:& 9237:forces 8998:Memory 8653:simple 7985:& 7967:& 7949:& 7020:& 7005:& 6987:& 6207:& 6180:& 5723:, and 5460:-> 5451:& 5442:-> 5355:valid. 5136:count 5110:& 5089:& 5071:& 5029:& 5014:& 4996:& 4981:start 4888:) | ( 4868:) | ( 4848:) | ( 4828:) | ( 4818:| ( ¬ 4622:& 4060:& 3886:, and 3235:format 3231:models 1940:& 1913:& 1869:& 1722:TRUTH. 1693:) " ≡ 1403:Jevons 1206:(b|a) 1143:NOT a 1140:NOT b 757:analog 657:atomic 331:syntax 12973:Model 12721:Peano 12578:Proof 12418:Arity 12347:Naive 12234:image 12166:Fuzzy 12126:Empty 12075:union 12020:Class 11661:Model 11651:Lemma 11609:Axiom 11529:Nicod 11158:and ( 10970:pbk.) 10735:XOR b 10731:( ( a 10712:and b 6154:rows 6130:taut 6070:c → b 5345:valid 4598:taut 4374:(NOT) 4362:(AND) 4359:& 3983:taut 3129:Some 3060:v(B) 3054:v(A) 2962:) = F 2876:is a 1496:~(a) 1493:~(b) 1473:NAND 1401:from 1395:Boole 1393:from 1155:b IS 735:and " 667:, or 167:there 150:below 110:that 13096:Type 12899:list 12703:list 12680:list 12669:Term 12603:rank 12497:open 12391:list 12203:Maps 12108:sets 11967:Free 11937:list 11687:list 11614:list 11513:and 11499:ISBN 11479:ISBN 11448:ISBN 11428:ISBN 11379:ISBN 11361:ISBN 11341:ISBN 11324:ISBN 11304:ISBN 11294:and 11267:ISBN 10964:ISBN 10944:"u". 10907:and 10743:)= Σ 10706:bits 10689:and 9818:row 9328:= q 9110:= q 8885:= q 8765:= q 7925:row 6963:row 6597:and 6500:6,7 6417:4,5 6334:2,3 6251:0,1 5413:arg 5319:both 4906:> 4900:< 4896:> 4890:< 4886:> 4880:< 4876:> 4870:< 4866:> 4860:< 4856:> 4850:< 4846:> 4840:< 4836:> 4830:< 4826:> 4820:< 4816:> 4810:< 4804:> 4798:< 4466:and 4368:(OR) 3742:and 3540:and 3001:mean 2907:) ≠ 2868:and 1952:=d2 1899:=d1 1837:row 1682:') ≡ 1654:and 1479:XOR 1476:NOR 1467:AND 1464:NOT 1461:NOT 1385:and 887:and 737:blue 727:blue 418:row 190:The 118:, a 66:and 43:, a 23:, a 12783:of 12765:of 12713:of 12245:Sur 12219:Map 12026:Ur- 12008:Set 11142:of 10749:( a 10589:'s 9899:=q 8864:qd 6724:or 6688:cba 5323:and 4944:of 4807:::= 4789:in 4778:or 3651:to 3310:))) 3291:): 3249:a = 2890:, p 2886:, p 2845:, p 2841:, p 1812:d2 1775:d1 1704:) " 1470:OR 98:In 90:OR 19:In 13328:: 13169:NP 12793:: 12787:: 12717:: 12394:), 12249:Bi 12241:In 11162:- 11043:Df 10955:is 10682:: 10585:, 10574:. 10515:1 10502:1 10497:0 10494:0 10491:1 10484:1 10481:1 10478:1 10473:1 10468:1 10465:1 10462:1 10455:1 10452:1 10449:1 10446:7 10438:1 10425:1 10420:0 10417:0 10414:0 10407:1 10404:1 10401:1 10396:1 10391:1 10388:0 10385:0 10378:0 10375:1 10372:1 10369:6 10349:0 10344:1 10341:1 10338:1 10331:0 10328:0 10325:1 10320:0 10315:0 10312:0 10309:1 10302:1 10299:0 10296:1 10293:5 10285:1 10272:0 10267:1 10264:0 10261:0 10254:1 10251:1 10248:1 10243:1 10238:0 10235:0 10232:0 10225:0 10222:0 10219:1 10216:4 10196:1 10191:0 10188:0 10185:1 10178:1 10175:0 10172:0 10167:1 10162:1 10159:1 10156:1 10149:1 10146:1 10143:0 10140:3 10132:0 10119:1 10114:0 10111:0 10108:0 10101:1 10098:0 10095:0 10090:0 10085:1 10082:0 10079:0 10072:0 10069:1 10066:0 10063:2 10053:0 10040:0 10035:1 10032:1 10029:1 10022:0 10019:0 10016:0 10011:0 10006:0 10003:0 10000:1 9993:1 9990:0 9987:0 9984:1 9976:0 9963:0 9958:1 9955:0 9952:0 9945:1 9942:0 9939:0 9934:0 9929:0 9926:0 9923:0 9916:0 9913:0 9910:0 9907:0 9896:) 9893:) 9890:) 9887:) 9884:) 9881:d 9878:( 9875:~ 9869:c 9866:( 9863:( 9860:~ 9854:q 9851:( 9845:) 9842:d 9836:c 9833:( 9830:( 9827:c 9824:d 9821:q 9795:u 9792:r 9783:v 9780:w 9773:q 9766:s 9700:1 9691:1 9686:0 9683:0 9680:1 9675:1 9672:1 9667:1 9664:1 9661:1 9653:1 9644:0 9639:1 9636:1 9633:1 9628:1 9625:1 9620:0 9617:1 9614:1 9598:1 9593:0 9590:0 9587:1 9582:0 9579:0 9574:1 9571:0 9568:1 9560:1 9551:0 9546:1 9543:1 9540:1 9535:1 9532:0 9527:0 9524:0 9521:1 9505:1 9500:0 9497:0 9494:0 9489:1 9486:1 9481:1 9478:1 9475:0 9459:0 9454:1 9451:0 9448:0 9443:1 9440:1 9435:0 9432:1 9429:0 9421:0 9412:1 9407:0 9404:0 9401:0 9396:0 9393:0 9388:1 9385:0 9382:0 9374:0 9365:0 9360:1 9357:0 9354:0 9349:0 9346:0 9341:0 9338:0 9335:0 9325:) 9322:) 9319:) 9316:r 9313:( 9310:~ 9304:p 9301:( 9295:s 9292:( 9289:r 9286:s 9283:p 9256:q 9216:1 9211:1 9208:1 9205:1 9200:1 9197:1 9189:1 9184:1 9181:1 9178:0 9173:0 9170:1 9158:0 9155:1 9152:1 9147:1 9144:0 9136:0 9131:0 9128:0 9125:0 9120:0 9117:0 9107:) 9104:p 9098:s 9095:( 9092:s 9089:p 9076:q 9037:. 8988:0 8983:1 8978:0 8973:1 8970:1 8962:1 8957:0 8952:1 8947:0 8944:1 8936:0 8931:1 8926:0 8921:1 8918:0 8910:1 8905:0 8900:1 8895:0 8892:0 8882:) 8879:p 8876:( 8873:~ 8870:( 8867:p 8849:q 8810:0 8805:1 8800:0 8795:1 8787:1 8782:0 8777:1 8772:0 8762:) 8759:p 8756:( 8753:~ 8748:p 8733:q 8710:, 8706:, 8702:, 8607:q 8564:1 8559:0 8556:0 8553:1 8548:1 8543:1 8540:1 8537:1 8532:1 8527:1 8524:1 8521:1 8514:1 8511:1 8508:1 8502:7 8493:0 8488:1 8485:1 8482:1 8477:1 8472:1 8469:1 8466:1 8461:1 8456:0 8453:0 8450:1 8443:0 8440:1 8437:1 8431:6 8422:1 8417:0 8414:0 8411:1 8406:0 8401:0 8398:0 8395:1 8390:0 8385:1 8382:0 8379:0 8372:1 8369:0 8366:1 8360:5 8351:0 8346:1 8343:1 8340:1 8335:1 8330:0 8327:0 8324:1 8319:0 8314:0 8311:0 8308:0 8301:0 8298:0 8295:1 8289:4 8280:1 8275:0 8272:0 8269:0 8264:1 8259:1 8256:0 8253:0 8248:1 8243:1 8240:1 8237:1 8230:1 8227:1 8224:0 8218:3 8209:0 8204:1 8201:0 8198:0 8193:0 8188:1 8185:0 8182:0 8177:0 8172:0 8169:0 8166:1 8159:0 8156:1 8153:0 8147:2 8138:1 8133:0 8130:0 8127:0 8122:0 8117:0 8114:0 8111:0 8106:0 8101:1 8098:0 8095:0 8088:1 8085:0 8082:0 8076:1 8067:0 8062:1 8059:0 8056:0 8051:0 8046:0 8043:0 8040:0 8035:0 8030:0 8027:0 8024:0 8017:0 8014:0 8011:0 8005:0 8000:) 7997:) 7994:c 7991:( 7988:~ 7982:p 7979:( 7973:) 7970:d 7964:p 7961:( 7955:) 7952:c 7946:d 7943:( 7940:( 7937:c 7934:d 7931:p 7705:q 7663:1 7658:0 7655:0 7652:1 7645:1 7642:1 7639:1 7634:1 7629:1 7626:1 7623:0 7616:1 7613:1 7610:1 7604:7 7584:1 7579:0 7576:0 7573:0 7566:1 7563:1 7560:1 7555:1 7550:1 7547:0 7544:0 7537:0 7534:1 7531:1 7525:6 7506:0 7501:1 7498:1 7495:1 7488:0 7485:0 7482:1 7477:0 7472:0 7469:0 7466:1 7459:1 7456:0 7453:1 7447:5 7427:0 7422:1 7419:0 7416:0 7409:1 7406:1 7403:1 7398:1 7393:0 7390:0 7387:0 7380:0 7377:0 7374:1 7368:4 7348:1 7343:0 7340:0 7337:1 7330:1 7327:0 7324:0 7319:1 7314:1 7311:1 7308:1 7301:1 7298:1 7295:0 7289:3 7270:1 7265:0 7262:0 7259:0 7252:1 7249:0 7246:0 7241:0 7236:1 7233:0 7230:0 7223:0 7220:1 7217:0 7211:2 7192:0 7187:1 7184:1 7181:1 7174:0 7171:0 7168:0 7163:0 7158:0 7155:0 7152:1 7145:1 7142:0 7139:0 7133:1 7114:0 7109:1 7106:0 7103:0 7096:1 7093:0 7090:0 7085:0 7080:0 7077:0 7074:0 7067:0 7064:0 7061:0 7055:0 7044:) 7041:) 7038:) 7035:) 7032:) 7029:d 7026:( 7023:~ 7017:c 7014:( 7011:( 7008:~ 7002:p 6999:( 6993:) 6990:d 6984:c 6981:( 6978:( 6975:c 6972:d 6969:p 6900:0 6897:0 6894:0 6891:0 6883:0 6880:0 6877:1 6874:4 6866:1 6863:0 6860:1 6857:5 6849:1 6846:1 6843:1 6840:7 6832:0 6829:1 6826:1 6823:6 6815:0 6812:1 6809:0 6806:2 6798:1 6795:1 6792:0 6789:3 6781:1 6778:0 6775:0 6772:1 6764:0 6761:0 6758:0 6755:0 6747:a 6744:b 6741:c 6701:10 6632:. 6574:1 6571:1 6566:1 6561:0 6556:1 6549:1 6546:0 6541:1 6536:0 6531:1 6526:1 6523:1 6520:1 6509:1 6506:1 6503:1 6491:0 6488:0 6483:1 6478:0 6473:1 6466:1 6463:0 6458:1 6453:0 6448:0 6443:0 6440:0 6437:1 6426:1 6423:0 6420:1 6408:1 6405:1 6400:0 6395:1 6390:1 6383:1 6380:1 6375:0 6370:1 6365:1 6360:1 6357:0 6354:0 6343:1 6340:1 6337:0 6325:0 6322:1 6317:0 6312:1 6307:1 6300:1 6297:1 6292:0 6287:1 6282:1 6277:0 6274:0 6271:0 6260:1 6257:0 6254:0 6246:) 6243:) 6240:b 6237:V 6234:) 6231:c 6228:( 6225:~ 6222:( 6219:≡ 6216:) 6213:) 6210:a 6204:) 6201:c 6198:( 6195:~ 6192:( 6189:V 6186:) 6183:b 6177:c 6174:( 6171:( 6168:( 6163:a 6160:b 6157:c 6143:d 6109:d 5990:, 5807:: 5787:. 5691:, 5636:1 5633:1 5628:1 5625:1 5620:1 5617:1 5614:1 5603:1 5600:1 5593:1 5590:1 5585:0 5582:0 5577:0 5574:0 5571:1 5560:0 5557:1 5550:0 5547:0 5542:1 5539:1 5534:1 5531:1 5528:0 5517:1 5514:0 5507:0 5504:1 5499:0 5496:0 5491:0 5488:1 5485:0 5474:0 5471:0 5466:) 5463:a 5457:) 5454:b 5448:) 5445:b 5439:a 5436:( 5433:( 5430:( 5425:b 5422:a 5388:G 5385:W 5353:is 5289:0 5286:1 5283:2 5280:3 5277:3 5274:3 5271:3 5268:3 5265:3 5262:3 5259:2 5256:2 5253:3 5250:4 5247:4 5244:4 5241:4 5238:3 5235:3 5232:4 5229:4 5226:4 5223:4 5220:3 5217:2 5214:1 5211:1 5208:3 5205:3 5202:4 5199:5 5196:6 5193:6 5190:5 5187:5 5184:5 5181:5 5178:4 5175:3 5172:3 5169:3 5166:3 5163:2 5160:2 5157:3 5154:3 5151:3 5148:3 5145:2 5142:1 5139:0 5131:) 5128:) 5125:) 5122:) 5119:c 5116:( 5113:~ 5107:p 5104:( 5101:V 5098:) 5095:) 5092:d 5086:p 5083:( 5080:V 5077:) 5074:d 5068:c 5065:( 5062:( 5059:( 5056:= 5053:) 5050:) 5047:) 5044:) 5041:) 5038:d 5035:( 5032:~ 5026:c 5023:( 5020:( 5017:~ 5011:p 5008:( 5005:V 5002:) 4999:d 4993:c 4990:( 4987:( 4984:( 4966:: 4908:) 4898:↔ 4878:→ 4858:∨ 4838:∧ 4793:: 4718:0 4715:1 4708:1 4703:0 4700:0 4697:1 4688:1 4681:0 4678:1 4671:0 4666:1 4663:0 4660:0 4651:0 4646:) 4643:0 4640:≡ 4637:) 4634:) 4631:a 4628:( 4625:~ 4619:a 4616:( 4613:( 4608:a 4601:c 4585:c 4567:Df 4470:: 4383:∃x 4377:∀x 4312:1 4307:0 4304:0 4299:1 4294:0 4289:1 4284:1 4281:1 4278:1 4273:0 4266:1 4263:1 4252:0 4247:1 4244:0 4239:1 4234:0 4229:1 4224:0 4221:1 4218:1 4213:0 4206:0 4203:1 4192:1 4187:0 4184:0 4179:0 4174:1 4169:1 4164:1 4161:1 4158:0 4153:0 4146:1 4143:0 4132:0 4127:1 4124:1 4119:0 4114:1 4109:1 4104:0 4101:0 4098:0 4093:1 4086:0 4083:0 4078:) 4075:) 4072:) 4069:a 4066:( 4063:~ 4057:) 4054:b 4051:( 4048:~ 4045:( 4042:≡ 4039:) 4036:a 4033:V 4030:b 4027:( 4024:~ 4021:( 4016:a 4013:b 3996:Q 3970:P 3927:XX 3855:, 3658:: 3653:XX 3646:XX 3338:Df 3263:Df 3255:Df 3251:Df 3244:Df 3209:Df 3202:Df 3195:Df 3188:Df 3181:Df 3170:Df 3121:T 3118:T 3115:T 3106:F 3103:F 3100:T 3091:T 3088:T 3085:F 3076:F 3073:T 3070:F 3063:) 3057:→ 3051:( 3028:) 3025:ii 3013:ii 3006:(~ 2988:ii 2970:ii 2942:→ 2911:(~ 2830:. 2784:1 2777:1 2774:0 2769:1 2764:0 2759:1 2754:1 2751:1 2748:1 2739:1 2732:1 2729:1 2724:1 2719:0 2714:1 2709:1 2706:1 2703:1 2694:1 2691:1 2688:1 2685:7 2680:1 2673:0 2670:0 2665:1 2660:0 2655:1 2650:1 2647:1 2644:1 2635:1 2628:0 2625:1 2620:1 2615:0 2610:1 2605:1 2602:1 2599:1 2590:0 2587:1 2584:1 2581:6 2576:0 2569:1 2566:0 2561:1 2556:0 2551:0 2546:0 2543:0 2540:1 2531:0 2524:1 2521:1 2516:1 2511:0 2506:0 2501:0 2498:0 2495:1 2486:1 2483:0 2480:1 2477:5 2472:0 2465:0 2462:0 2457:1 2452:0 2447:0 2442:0 2439:0 2436:1 2427:0 2420:0 2417:1 2412:1 2407:0 2402:0 2397:0 2394:0 2391:1 2382:0 2379:0 2376:1 2373:4 2368:1 2361:1 2358:1 2353:0 2348:1 2343:1 2338:1 2335:0 2332:0 2323:1 2316:1 2313:1 2308:0 2303:1 2298:1 2293:1 2290:1 2287:0 2278:1 2275:1 2272:0 2269:3 2264:0 2257:0 2254:0 2249:0 2244:1 2239:0 2234:1 2231:0 2228:0 2219:0 2212:0 2209:0 2204:0 2199:1 2194:0 2189:1 2186:1 2183:0 2174:0 2171:1 2168:0 2165:2 2160:1 2153:1 2150:1 2145:0 2140:1 2135:1 2130:0 2127:0 2124:0 2115:1 2108:1 2105:1 2100:0 2095:1 2090:1 2085:0 2082:1 2079:0 2070:1 2067:0 2064:0 2061:1 2056:0 2049:0 2046:0 2041:0 2036:1 2031:0 2026:0 2023:0 2020:0 2011:0 2004:0 2001:0 1996:0 1991:1 1986:0 1981:0 1978:1 1975:0 1966:0 1963:0 1960:0 1957:0 1949:) 1946:) 1943:a 1937:) 1934:c 1931:( 1928:~ 1925:( 1919:) 1916:b 1910:c 1907:( 1904:( 1896:) 1893:) 1890:a 1887:→ 1884:) 1881:c 1878:( 1875:~ 1872:( 1866:) 1863:b 1860:→ 1857:c 1854:( 1851:( 1846:a 1843:b 1840:c 1747:. 1639:0 1636:0 1633:0 1630:1 1627:1 1624:0 1621:0 1618:1 1615:1 1612:3 1607:1 1604:0 1601:1 1598:1 1595:0 1592:1 1589:0 1586:0 1583:1 1580:2 1575:1 1572:0 1569:1 1566:1 1563:0 1560:0 1557:1 1554:1 1551:0 1548:1 1543:0 1540:1 1537:1 1534:0 1531:0 1528:1 1525:1 1522:0 1519:0 1516:0 1511:⊕ 1490:a 1487:b 1361:F 1358:F 1355:F 1352:T 1349:T 1346:T 1343:T 1340:T 1337:F 1334:F 1331:T 1328:T 1323:T 1320:T 1317:F 1314:T 1311:F 1308:F 1305:T 1302:F 1299:T 1296:F 1293:F 1290:T 1285:T 1282:T 1279:F 1276:T 1273:F 1270:T 1267:T 1264:F 1261:F 1258:T 1255:T 1252:F 1247:F 1244:T 1241:T 1238:T 1235:T 1232:T 1229:F 1226:F 1223:T 1220:T 1217:F 1214:F 1179:a 1176:b 763:. 732:am 683:. 671:, 663:, 638:1 618:7 613:0 593:6 588:0 568:5 563:1 543:4 538:0 518:3 513:1 493:2 488:1 468:1 463:0 443:0 438:Σ 435:co 427:ci 127:+ 114:a 94:). 51:. 13249:/ 13164:P 12919:) 12705:) 12701:( 12598:∀ 12593:! 12588:∃ 12549:= 12544:↔ 12539:→ 12534:∧ 12529:∨ 12524:¬ 12247:/ 12243:/ 12217:/ 12028:) 12024:( 11911:∞ 11901:3 11689:) 11587:e 11580:t 11573:v 11385:. 11275:. 11192:C 11188:C 11184:u 11180:C 11176:M 11172:M 11168:u 11164:M 11160:C 11156:M 11152:C 11144:M 11140:u 11093:. 10765:; 10763:i 10759:i 10755:i 10751:i 10745:i 10741:i 10737:i 10733:i 10726:i 10722:i 10718:i 10714:i 10710:i 10708:a 9739:q 9735:q 9728:q 9724:p 9033:q 9019:. 7853:. 6697:2 6690:2 5950:) 5943:| 5936:( 5909:) 5906:) 5903:a 5899:| 5895:a 5892:( 5888:| 5884:a 5881:( 5775:} 5769:, 5763:{ 5743:} 5737:, 5731:{ 5711:} 5705:, 5699:{ 5679:} 5673:, 5667:{ 4954:y 4950:x 4946:x 4942:y 4925:( 4915:x 4451:) 4407:' 4401:* 4395:+ 4389:= 4371:~ 4353:→ 4347:≡ 3947:n 3934:V 3929:V 3923:V 3897:E 3866:E 3835:E 3812:) 3809:z 3803:y 3800:( 3780:) 3777:z 3774:, 3771:y 3768:( 3757:E 3744:z 3740:y 3735:. 3723:) 3720:z 3714:( 3694:) 3691:z 3688:( 3677:E 3664:z 3655:V 3648:V 3642:V 3637:V 3635:X 3631:V 3618:. 3603:, 3597:, 3591:, 3508:) 3494:( 3452:) 3443:( 3410:, 3404:, 3398:, 3392:, 3308:2 3304:1 3300:2 3296:1 3289:2 3285:1 3183:s 3168:= 3019:i 3008:A 3004:v 2997:A 2995:( 2993:v 2982:i 2972:) 2968:( 2960:B 2958:( 2956:v 2952:A 2950:( 2948:v 2944:B 2940:A 2938:( 2936:v 2925:) 2923:i 2921:( 2915:) 2913:A 2909:v 2905:A 2903:( 2901:v 2892:3 2888:2 2884:1 2874:v 2870:B 2866:A 2847:3 2843:2 2839:1 1741:n 1702:a 1698:b 1691:a 1687:b 1680:a 1676:b 1665:C 971:) 939:. 927:) 915:( 852:, 846:, 840:, 681:q 677:p 673:Q 669:P 665:q 661:p 635:1 632:3 627:1 624:1 621:1 610:1 607:2 602:0 599:1 596:1 585:1 582:2 577:1 574:0 571:1 560:0 557:1 552:0 549:0 546:1 535:1 532:2 527:1 524:1 521:0 510:0 507:1 502:0 499:1 496:0 485:0 482:1 477:1 474:0 471:0 460:0 457:0 452:0 449:0 446:0 424:a 421:b 409:2 319:) 313:( 308:) 304:( 300:. 157:. 129:y 125:x 92:q 88:p 84:q 80:p 78:( 68:q 64:p

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

Index