Willard Van Orman Quine’s Mathematical Logic builds mathematics out of a deliberately narrow logical foundation. Written for readers with no prior training in logic, it grew out of his Harvard course and was first published in 1940, then substantially revised in 1951 after a flaw in its class theory was discovered; the 1981 preface looks back on the whole enterprise. The book is expository and technical rather than narrative: its subject is not events or people but the machinery of statements, quantifiers, classes, relations, and number, and its aim is to show how the language of mathematics can be constructed step by step from a handful of primitive notions.
“Great pioneer works are proverbially easy to improve.”
Quine’s guiding conviction is that much of what logic formalizes already lies half-formed in ordinary speech, and that a rigorous notation can sharpen it. He treats the field as a frontier rather than a settled textbook subject, so the book combines the roles of manual and treatise. The opening chapters reduce the connectives of everyday argument to a single primitive, clarify the pronoun-like work of variables, and set out an explicit axiom system with modus ponens as its only rule of inference. From there the construction widens into membership and classes, identity and descriptions, then relations, functions, and finally the natural numbers and the real continuum, with a closing chapter that turns the whole apparatus on itself to prove Gödel’s incompleteness theorem.
How the Logical System Is Built
The Prefaces and the Making of a Logic
Quine opens the Revised Edition by tracing the book’s lineage. As a new doctor in 1932 he was wholly under the spell of Principia Mathematica—the work of his teacher Whitehead and Whitehead’s pupil Russell—which he treated as the datum plane of mathematical logic; progress meant improving it, correcting its confusion of use and mention and its muddles over propositional functions, implication, and ramified types. Only the next year, in Prague and Warsaw, did Carnap, Tarski, and others widen his view. His A System of Logistic of 1934 stayed inside the Principia tradition; Mathematical Logic, six years later, differs in sweep and independence, yet still shares the old traits: a monolithic deductive system on fixed axioms and rules, explicit proofs in rigid notation, and set theory subsumed under logic. Barkley Rosser showed the 1940 set theory inconsistent; a corrigendum slip was pasted in, Harvard University Press rescued the book for a 1947 printing, and Hao Wang supplied the emendation consecrated in 1951. The early drafts used the set theory of Quine’s 1937 “New Foundations”; he liberalized it by a device of von Neumann’s, overdid it, and Wang brought it back into line, proving either system consistent if the other is. Rosser proved the natural numbers cannot be shown an “element” if the system is consistent, so an added axiom is acquiesced in. Quine used no schemata, only their instances, and insisted on closed sentences, since logic is for closed sentences; quasi-quotation (“corners”) let him write about arbitrary predicates without confusing use and mention. The final chapter formalizes metalogic and proves Gödel’s incompleteness theorem via protosyntax, a case of Tarski’s theorem, then correlates protosyntax with number theory. The 1951 preface records revisions to half the pages, Wang’s repair of the class-theory axioms, Berry’s simplification of closure, and an appendix easing two reader difficulties—the theorem/metatheorem distinction and incompletability. The 1940 preface presents the book as textbook and treatise at once, grown from his Harvard course Mathematics 19, and sketches the chapters: truth-functions reduced to Sheffer’s joint denial, quantification with modus ponens as sole rule, classes by contextual definition, and axioms of membership avoiding Russell’s antinomy by a method less restrictive than types.
Logic as Technique
The Introduction argues that where number is irrelevant, regimented mathematical technique has been lacking; measurement ties subject matter to the real numbers, but no science rests entirely on measurement. Mathematical logic offers explicit techniques for manipulating the basic ingredients of discourse, sharpening concepts so hidden consequences and subtle errors surface. Its most important applications, Quine says, are still to come, and applicational needs should drive further theory.
Truth-Functions and the Conditional
Elementary logic deals with statements and their compounding. Conjunction is true only if both components are true; alternation, taken inclusively after ‘vel’, is false only if both are false; denial is true iff the original is false. Each mode is fixed by a truth table, and all modes needed for mathematics are truth-functional. The conditional is false only with true antecedent and false consequent, so “If France is in Australia then the sea is sweet” comes out true—idle, not false. The subjunctive conditional resists the table and is shelved, since mathematics makes no use of it. The truth-functional conditional goes back to Philo of Megara, revived by Frege and Peirce.
Statements About Statements
Quine separates statements about statements from statements about objects: ‘is true’ and ‘is false’ are predicates attaching to names of statements, while connectives attach to statements. Hence “‘All men are mortal’ implies ‘all white men are mortal'” is correct, but “All men are mortal implies all white men are mortal” is not. Logical implication holds when the corresponding conditional is logically true; material implication when it is merely true—so broad it scarcely deserves the name, yet still a binary predicate, not a connective. Whitehead and Russell’s ‘⊃’ is criticized for sliding between “if—then” and “implies”; Lewis’s systems describe non-truth-functional modes of composition, not implication relations. Statements are not names, and quotation cannot make buried statements into constituents.
Reduction to Primitives, Tautology, and Selected Forms
Every truth table can be built from denial, conjunction, and alternation: conjoin or alternate the case-descriptions marked true, and where none is true use a self-contradictory conjunction. Joint denial, “neither-nor,” suffices alone—denial as “(φ|φ)”, conjunction and alternation by further nestings—so it may be the sole primitive, with the other signs introduced as shorthand.
The Quantifier and the Pronominal Variable
The move from truth-functional composition to generality begins with a simple observation: “9 is less than, equal to, or greater than 0” is one thing, but “every number is less than, equal to, or greater than 0” cannot be rendered as a disjunction of three universal claims, since that would say one category exhausts all numbers. What is needed is a prefix meaning “whatever number you may select,” and the trouble is that nested quantifiers require keeping track of which “it” refers to which prefix. Subscripts solve this, and then a more compact device replaces subscripts with distinct letters. “All men are mortal” becomes a quantified conditional; “no man has seen every city” becomes a quantified denial. The range-indicator notation is eventually dropped altogether, so that “(x)(x is a man ⊃ x is mortal)” stands as standard. Quine calls the prefixes quantifiers, their use quantification, and the letters variables—a term he keeps only out of deference to usage, since the “variation” is a metaphor best forgotten. Variables have purely pronominal meaning, marking cross-references to positions of quantification, which could in principle be shown by curved lines or bonds, too cumbersome for practice. Quantification cuts across the vernacular “all,” “every,” “any,” “some,” clearing ambiguities—Smith outrunning men on the team can be said several ways, and only some of them are equivalent. A footnote credits Frege with first devising a general quantification notation with auxiliary variables, so important that Frege rather than Boole might be seen as the founder of modern logic.
Formulae and the Demarcation of Quantificational Truth
Formulae are built from atomic formulae by joint denial and quantification; those with no free variables are statements, true or false. There are no atomic logical statements, and the shortest true ones deny that every entity is a member of itself—a truth not available as a theorem until much later. Quantificational truths are marked out by a generative principle: certain axiom sets are recognized on sight, and further truths are generated by modus ponens. Four sets are specified. Set A comprises closures of tautologous formulae, where the quantifier is essential, since without it we have only a matrix, neither true nor false. Set B distributes a universal quantifier through a conditional. Set C covers vacuous quantification. Set D′ proves defective: it admits “(x)(y)(y = x) ⊃ ~(y)(y = y),” whose antecedent is true and consequent false, because the substituted variable gets captured by a quantifier lurking inside. The revised set D requires substituted occurrences to remain free.
Theorems and Metatheorems
Theorems are the axioms plus ponentials of axioms, plus ponentials of that totality, and so on—recursively characterized. Tautologous statements, axioms, and theorems form successively broader classes; unlike the first two, theorems have no complete test, so failure to find a proof is no evidence. Only a partial test exists: given a sequence, one can check whether it makes a formula a theorem. The mathematician hits on proofs by insight and fortune; others can check them. Metatheorems record general conditions under which statements are theorems, establishing theorems wholesale. The rule that ponentials of theorems are theorems is proved by induction on the number of free variables, and a condensed notation with square brackets indicates deletion of antecedents. The convention of abbreviating metatheorems by their numerals came from Leigh D. Steinhardt.
Substitutivity of the Biconditional
If two statements agree in truth value, one can replace the other without affecting truth value—but generalizing to closures fails, since substituted variables get captured by new quantifiers. The corrected principle requires free occurrences, and the recalcitrant cases with quantifiers attached to the antecedent are handled separately, the single-occurrence case proved by induction over subformulae. The general metatheorem then yields interchangeability of free occurrences, and from that the deletion of conditionals, conjunctions, alternations, and negations from any position within any theorem—extending the square-bracket device beyond the limited use justified earlier.
Existential Quantification and Distribution
To say nothing fulfills a condition is to say everything fulfills its denial; denying that there are none yields “there is at least one object x such that.” Quine defines the existential quantifier accordingly, and a run of metatheorems relates it to universal quantification. Order matters when one quantifier is existential and the other universal: “(∃x)(y)(x=y)” is false whereas “(y)(∃x)(x=y)” is true, and only one direction of the conditional holds. A universal quantifier distributes through a conjunction, an existential through an alternation; distribution of a universal through an alternation, or an existential through a conjunction, is not generally valid.
Identity and the Machinery of Proof
Quine opens with identity, naming *182 and *183 the principles of reflexivity and symmetry, carried over by analogy from statement composition, and *184 a strengthened transitivity. The theorem *185, asserting that y belongs to x exactly when some z contains y and equals x, gets an elaborate proof meant to display the notation for theorems as opposed to metatheorems: lines in a proof are formulae whose closures are theorems, numerals abbreviate lines, brackets flag uses of *124, and a theorem’s numeral stripped of its dagger stands for the theorem minus its initial quantifiers. Combining *100 with *163 or *117 lets existential or universal quantifiers be introduced when the rest is tautologous and the variable free nowhere in the consequent. A footnote distinguishes total reflexivity of predicates, after Carnap, from the broader reflexive.
Abstraction Completed, V and Λ
D12 defines membership of an abstract in a class, completing the explanation of φ ∈ ψ for variables and abstracts; D13 and D14 add non-membership and multiple membership. Every abstract ultimately reduces to the form y ∈ x̂φ, which D9 then eliminates, and the prefix x̂ binds like a quantifier. Metatheorems 186–188 mirror 121–123, and *189 shows x̂(x ∈ x) cancels y ∈. D15 defines V as the class of all elements, D16 the null class Λ; theorems follow, including that a universal condition gives V and a universally false one gives Λ. Quine credits Kaplansky and Norris for a short proof of *192, and a footnote traces contextual definition of terms to Russell, the signs V and Λ to Boole and Peano, while claiming the present use of V to affirm elementhood as new.
Descriptions and the Elimination of Names
The description operator (ιx)(…x…) means the one and only object satisfying a condition; ordinary usage leaves unclear cases, so Quine defines it to be significant always, treating waste cases as Λ. D17 gives the formal definition, *195 shows every x is the sole self-identical object, and 196–197 establish that the definition yields the unique object when there is one and Λ otherwise. Frege gets credit for the first explicit formulation. Quine then argues that all names can be replaced by abstracts and descriptions, dodging primitive names like Pegasus and their existence puzzles, with Russell’s treatment of ‘exists’ discussed; terms comprise names and name matrices.
Stratification and Axioms of Membership
So far theoremhood depends only on quantifiers and joint denial, with ∈ idle. New membership axioms are needed, but Quine rejects axiomatizing every φ̂ ∈ V whose denial is unprovable: the broad sense of ‘theorem’ is circular, and no test decides non-theoremhood. What is wanted is a checkable condition. The cyclic clause α₀ ∈ α₁ … αₙ ∈ α₀ is too mild, since x̂~(y)(x = y ⊃ x ∈ y) names the non-element x̂(x ∉ x) without any cycle. The real mark is that numerals cannot be assigned so that ∈ always joins consecutive ascending numerals; a formula is stratified when they can. A step-by-step test is given. Taking stratified φ as sufficient fails, since it would admit all classes as elements; instead φ̂ ∈ V is assumed only for elements as values of free variables. Rosser showed the first edition’s system inconsistent, and Wang suggested restricting bound variables to elements too.
Substitutivity, Class Algebra, Inclusion, Unit Classes
Substitutivity of identity is adopted for atomic contexts, classed among membership axioms; with 200–202 added, V ∈ V, Λ ∈ V, and the existence of more than one entity are proved. A long note compares Russell’s types, Zermelo’s scheme, and Quine’s New Foundations. Later metatheorems extend substitution to many quantifiers, with daggered numerals tacitly invoking *233. Class product, sum, and complement are defined, with De Morgan-style laws; inclusion is distinguished from membership and shown reflexive, transitive, and identical with mutual inclusion. Unit classes are defined, and every non-element is shown to differ from every element in infinitely many members, so finite classes are elements.
Relations as Classes of Ordered Pairs
Conditions on two variables determine relations, but the relation z of x to y such that x does not bear x to y breeds contradiction. The fix mirrors classes: countenance only relations of elements. A relation pairs elements off with elements—less than pairs 0 with 1, father of pairs Abraham with Isaac—and is thought of as a class of ordered pairs. D23 defines x;y as the class whose sole members are ιx and ιx ∪ ιy, meeting elementhood and distinctness (1417). D24 defines x(y,z), the clause y, z ∈ V not superfluous.
The Ancestral and Its Proper Form
Quine resumes the theory of the ancestral by examining the class x″y, the objects bearing x to members of y—ancestors of lawyers, when x is parenthood. Theorem 1520 shows this class is closed under x. A characteristic inference follows: if every parent of a person born before 1800 was born before 1800, and Fiorecchio is an ancestor of Napoleon, who was born before 1800, then Fiorecchio was born before 1800. Metatheorems *521 and *522 formalize such reasoning. Theorems 1523–1524 turn to x̌, the ancestor relation counting each person as ancestor of himself; the relative products x̌|x and x|x̌ prove identical, yielding the narrower proper ancestral that excludes oneself. A footnote credits Frege with both notions and notes how Whitehead and Russell’s notation differs.
Functions as Single-Valued Relations
Functions are relations, Quine insists—”quadruple of” is a relation like any other. The element z’x bearing z to x is defined by description, and a function is single-valued: no two elements bear it to the same element. The range of functionality τx collects the y for which uniqueness holds; theorems 1530–1538 paraphrase membership in it, and where y lies outside the range, x’y collapses to Λ. Relative products enter through an illustration of father, son, and Eve. Functions of several arguments are simply triadic, tetradic relations, and the definition extends accordingly.
Functional Abstraction
Functional abstraction, λ̂α φ, builds functions from name matrices: quadruple of becomes λ̂x(4×x). Mathematicians conflate name matrices with functional abstracts, though the former contain free variables and designate nothing. Constant functions like λ̂x5 differ in meaning from the number 5. Metatheorems 540–546 govern abstracts, including the unit-class function λ̂xιx, which returns y for any y. Frege and Church, Quine notes, construe abstraction more broadly, class abstraction included.
Identity and Membership as Relations
The identity function I is λ̂x x, with V as its range; I(x,y) holds only where x and y are the same element, unlike x = y. Theorems 1550–1563 establish that I is its own converse, that imaging by I changes nothing, that I is included in every ancestral, and that I ∪ (x̌|x) = x̌. A footnote extends the vocabulary of transitivity, reflexivity, symmetry, idempotence, commutativity, and associativity to relations and functions. The membership relation Q diverges from ε just as I diverges from =; Q″x is the class of members of members of x.
Zero, One, Successor, and the Natural Numbers
Natural numbers are classes of classes: 7 is the class of all seven-member classes, and 0 is ιΛ. Successor is defined, with 1 and 2 following; theorems 1610–1616 show 1 = S’0 and 2 = S’1, that the range of S is V, that S’Λ = Λ, and that 0 is no successor. Nn is defined as Š″0, closed under S and containing 0, 1, 2; any class closed under S and containing 0 contains Nn. Mathematical induction arrives as metatheorem *636, illustrated with a general schema. A footnote traces the principle through Pascal and Fermat to Frege’s 1879 definition of the ancestral. The stronger *637 yields theorem 1638, and 1641 shows that finite classes with the same number of members coincide when one includes the other.
Counter Sets and the Infinite
Augmenting a class by throwing in the class itself gives the self-augment, and iterating from Λ produces the counter sets Cs—von Neumann’s natural numbers, one member for each natural number. This guarantees a class of z members for every z, and so the infinitude of V. Theorems 1653–1664 mirror the earlier arithmetic: no counter set is a member of itself, Cs falls inside Russell’s class, V is no counter set, and every natural number has a counter set as member. Finitude is membership in a natural number; V belongs to none, so V is infinite and every finite class omits some element. Theorem 1677, that natural numbers with the same successor are equal, depends on V’s infinitude—a hypothetical finite V of 93 elements would collapse 93 and 94 alike to Λ.
Powers, Arithmetic, and the Number Systems
Relative powers x⁰, x¹, x² iterate a relation: grandparent, great-grandparent, with Kenan and Methuselah supplying a biblical illustration.
Defining the Protosyntax Anew
Quine closes the constructive work by laying down schemata A67 through A77, which turn the informal machinery of earlier sections into a single formal apparatus. A67 abbreviates a quantified joint denial; A68 and A69 build the identity and membership idioms by slotting variables into the blanks of earlier definitions; A70 and A71 define elementhood and its two-place relative. The predicate “Rx” is then introduced to say that every quantification inside an expression is restricted to elements, save where such clauses appear only as definitional expansions, and A72 gives this the formal shape “RE.” From there the membership axioms are sorted into three kinds—elementhood, and the two further varieties captured by A73 through A75—with the note that the elementhood axioms are read more broadly than in §28, though the widening adds no theorems. A76 collects all three kinds under the general notion of axiom, and A77 defines “Thm”: an expression is a theorem when it stands in a sequence whose every member is an axiom or a ponential of earlier members.
Protosyntax Turned on Itself
The argument then performs its decisive pivot. Instead of talking about expressions built over an alphabet containing “e,” protosyntax now speaks about expressions over the very alphabet in which protosyntax is written, so the ninth letter becomes “M” rather than “e.” The definition of a protosyntactical formula mirrors the logical one, with atomic formulae “Mxy” replacing “(a e B)”; definitions A1–30 carry over, except that A23 and A28 yield to new versions and A31 reappears with “PFmla₁” and “PFmla” in place of the old symbols. The theorems of this protosyntax would be ponentials of ponentials of the quantification axioms together with axioms governing “M.” An ideal set of axioms for “M” would make the theorems coincide exactly with the true protosyntactical statements—but Quine sets out to show that no protosyntactically definable notion of theorem can do this.
The Self-Referential Formula
The proof turns on constructing a statement that says of itself that it is not a theorem. If “PThm” were translatable into protosyntax, there would be a protosyntactical statement true just in case it is not a theorem: true, and the theorems fail to exhaust truths; false, and they fail to exclude falsehoods. Allowing quotation, the target is reformulated as a sentence declaring that a certain result is not a theorem, where the result comes from substituting a quotation for the variable “w” in a matrix. Carrying out that substitution returns the same sentence, so it says of itself that it is unprovable. To purge the talk of “result of putting” and “quotation of,” Quine observes that putting an expression u for the free variable in a matrix is equivalent to a substitution idiom in which z is “w =” followed by u. Quotation itself lies outside protosyntax, but for any x one can construct a matrix equivalent to “w =” followed by the quotation of x—the identity matrix of x, written “im x.” Supposing “PThm” and “im” have protosyntactical definitions, the matrix expands into primitive notation, which can be named by spelling it out; that name, abbreviated “H,” serves as a quotation, and the self-referential formula becomes “~PThm S₁qu(imH cd H).” True iff it is not a protosyntactical theorem, it proves that any protosyntactically definable concept of theorem either misses some truths or admits falsehoods. The remaining chore is defining “im x”: new definitions parallel A47–49, A62–64, and A66, with “x idp y” introduced, and the primitive expansion of “(x)(y) ~ Mxy” is put through successive blanks to yield Z₁ through Z₉, so that im Sᵢ is explained as Zᵢ for i from 1 to 9, while longer expressions are handled by a further definition of “z cid z′.”
The Apparatus at the Back
The edition’s back matter opens with a list of definitions D1–D48, each with its page—from “~p” for “(el p)” on p. 47 through the numerals and “Nn,” “Fin,” and the arithmetic definitions of pp. 237–259.
The Primitives and the Discipline of Notation
The intellectual spine of the book is a commitment to saying exactly what one means, and Quine enforces it by shrinking his vocabulary to the bone. Joint denial—”neither-nor”—serves as the sole connective, with negation, conjunction, alternation, and the conditional introduced only as abbreviations; membership and quantification complete the primitive stock, and everything else, including identity, is defined away. This economy is not decoration. It lets Quine measure what mathematics actually presupposes, and it forces the distinction he returns to again and again: the difference between using a statement and mentioning it. His “quasi-quotation,” the corner notation, exists precisely to let him talk about arbitrary expressions without sliding into that confusion, and his insistence on closed sentences rather than open ones reflects the same discipline—logic, he holds, is for statements that can be true or false, not for fragments awaiting a subject.
The treatment of the conditional shows the method at its most characteristic. Quine adopts the truth-functional reading, concedes that it departs from ordinary usage in the cases where we would not affirm an “if-then” at all, and argues that the departure is unavoidable for any complete formulation. The subjunctive conditional, so important to the philosophy of science through dispositional terms like “soluble” or “intelligent,” is set aside as calling for a more elaborate analysis than mathematics requires. Where a subjunctive seems needed, he suggests, one can often talk about statements instead—saying that one statement implies another rather than that something would be the case if something else were.
Classes, Paradox, and the Cost of Consistency
The middle of the book confronts the problem that made its early editions precarious. Naive class abstraction, which lets any condition on a variable determine a class, generates Russell’s paradox, and Quine’s response is to restrict membership rather than abandon classes. Borrowing a device from von Neumann, he distinguishes entities that can be members—elements—from those that cannot, so that the troublesome class of all non-self-membered classes is simply barred from membership in anything. The criterion for admitting a class is stratification: a formula qualifies when its variables can be assigned numerals so that membership always relates consecutive levels. This is a testable, mechanical condition, and Quine is explicit about why he wants one—an axiom no one can recognize as an axiom is useless for proof.
The honesty of the book lies in how it handles its own failure. The 1940 set theory turned out inconsistent, as Barkley Rosser showed, and the revised edition says so plainly, crediting Hao Wang with the repair and noting that the consistency of either system guarantees the consistency of the other. Quine’s remark that intuitive obviousness is the last, fallible arbiter of such matters captures the tone: confidence without complacency. The same care governs his treatment of descriptions and names, where “the so-and-so” is defined so as to be meaningful even when nothing or more than one thing fits, and ordinary names are eliminated in favor of abstracts—a move that dissolves puzzles about Pegasus and existence rather than solving them one by one.
What the Construction Is For
Quine’s ontology is deliberately spare and deliberately liberal at once. He countenances concrete objects and classes, and nothing else—no relations, functions, or numbers except as these are construed as classes. Relations become classes of ordered pairs, following the definition of the pair that Wiener and Kuratowski supplied; functions become single-valued relations; the natural numbers become classes of classes, with zero as the unit class of the null class and the successor relation doing the counting. The payoff is a demonstration that arithmetic needs no primitive notions of its own, only logic and the theory of classes. That this makes “1 + 1 = 2” a formula many pages long is a price Quine accepts cheerfully, since the point is not convenience but the measurement of conceptual presuppositions.
The final chapter turns the system inward. By formalizing metalogic and correlating syntax with number theory, Quine proves Gödel’s incompleteness theorem, and he notes that the argument is a case of Tarski’s theorem. Here the book’s economy of primitives earns its keep: metamathematics becomes manageable precisely because the subject matter has been reduced to a few kinds of expression. The incompleteness result also marks a boundary—the quantificational truths admit a generative demarcation, but logical truth in the broader sense resists even that.
The Book’s Place in the Tradition
Mathematical Logic sits at a particular moment in the history of the subject, and its 1981 preface is candid about that. Quine recalls beginning under the spell of Principia Mathematica, treating it as the datum plane against which progress meant correction—of the use-mention confusion, of the muddles over propositional functions and ramified types. His own book keeps Principia‘s monolithic architecture, its explicit proofs in rigid notation, and its subsumption of set theory under logic, while departing from it in sweep and independence. The footnotes trace a longer lineage: Frege as the true founder of modern quantification, Peirce and Sheffer for joint denial, Boole and the Stoics behind the tautologies, von Neumann and Zermelo and Skolem behind the class axioms.
What the book offers a reader now is less a doctrine than a demonstration of how to think under constraint. Its refusal of schemata in favor of their instances, its insistence that variables mean nothing beyond cross-reference, its willingness to let a system’s defects stand in the record—these are habits of mind as much as results. Quine’s hope, stated in the introduction, was that mathematical logic might bring to non-quantitative inquiry the rigor that measurement brought to natural science, sharpening concepts and exposing hidden consequences. The book is his attempt to supply the techniques for that work, and to show, in the doing, what a completely explicit language looks like.
