The Secret Logic That Lives Inside Every Sentence
A Computer’s Headache Becomes a Logic Puzzle
Imagine you are a computer program trying to read the sentence “The green frog jumped.” You don’t have a human brain’s instinct for language. All you see are five symbols. Which words hook together first? Does “green” attach to “frog,” or does “green frog” act as one unit? If you guess wrong, you end up thinking “jumped” is a frog-like color. In 1958, the Canadian mathematician Jim Lambek (1922–2014) proposed a radical answer: treat grammar as a kind of mathematical logic, where words are pieces that fit together only in strictly limited ways. His idea would eventually help computers understand language—and reveal a hidden logical skeleton inside every sentence we speak.
Lambek’s goal was to find an algorithm that can tell sentences apart from random word soup, not just for tidy formal languages but for messy everyday speech. He turned familiar parts of speech into formulas of a logic—a system of symbols and rules designed to reason about how words combine. In this view, deciding that a phrase is well-formed is the result of a proof, much like showing that a mathematical statement is true.
Types: The Building Blocks That Decide What Fits
Lambek’s system gives every word a type. Think of types as specially shaped puzzle pieces. Some pieces are complete by themselves, while others have slots that demand exactly one kind of neighbor. The atomic (basic) types represent grammatically “complete” phrases: a sentence gets the type s, a noun phrase gets np, and a common noun like “girl” gets n.
Complex types use three operations: product (⊗) and two kinds of division (slash and backslash). The product A ⊗ B says you have put together an A and a B in that order. The division B / A (pronounced “B over A”) is the type of an expression that still wants an A on its right to form a B. The A \ B (“A under B”) wants an A on its left.
Picture the verb “dreams.” It needs a subject noun phrase to its left to make a sentence. That requirement is captured by the type np \ s: give it an np on the left, and you get an s. The name “Mary” already is a complete noun phrase, so it gets the plain type np. When we put them together, we multiply the types: np ⊗ (np \ s) yields s—the proof that “Mary dreams” is a full sentence. A determiner like “the” gets np / n: it wants a common noun on its right to produce a noun phrase.
All of this is driven by logical rules called residuation laws. They tell us that A ⊢ C / B if and only if A ⊗ B ⊢ C, and so on. The symbol ⊢ means “is derivable from.” In ordinary talk, we can’t just throw words together; the types must prove that the combination works.
A Logic Without Copying or Shuffling
Ordinary logic often allows structural rules that would be a disaster for grammar. Contraction would let you copy a word for free, so “Mary Mary dreams” would be fine. Weakening would let you delete any word, turning “Mary dreams” into just “dreams.” Exchange (commutativity) would allow you to scramble word order, so “dreams Mary” would be as good as “Mary dreams.” And associativity would let you rebracket any phrase, ignoring how words actually group together.
Lambek threw out all these rules. His pure logic, called NL (Non-associative Lambek calculus), treats sentences as binary-branching trees. You can’t flatten the tree or swap its branches. This minimal system respects phrase structure and word order—the grammar of a particular language keeps a tight grip.
From this pure base, one obtains a family of logics by adding back structural options in controlled ways. The L calculus (Lambek 1958) adds associativity: the sentence “the green frog jumped” can be rebracketed as “(the green) (frog jumped)” freely. Some linguists worry that this overgenerates—it would let a rebracketing pattern that makes no sense. LP adds commutativity on top, turning word order into a multiset; left and right divisions collapse, so “Mary dreams” and “dreams Mary” are equivalent. LP is too wild for syntax, but it turns out to be perfect for representing the meaning of sentences, as we will see.
Lambek’s big insight was to reformulate the grammar logic as a Gentzen-style sequent calculus with a cut-elimination property. That means every valid proof can be found by a well-behaved search process—exactly what a computer needs to recognize a sentence.
From Grammar to Meaning: The Calculus of Ideas
Grammatical structure is only half the story. Sentences have meanings, too. In the 1980s, logician Johan van Benthem (born 1949) noticed a deep parallel: Lambek’s grammatical deductions line up perfectly with a system for building meanings, using the Curry-Howard correspondence (“proofs as programs”). The idea is that a proof of a grammatical combination can be seen as a program that assembles the meaning of the parts.
In the meaning side, we use a simpler logic called linear lambda calculus (matching LP, since meaning doesn’t care about word order). Types on this side are basic semantic types: e for entity (a person or thing) and t for truth value. A noun phrase like “Mary” translates to type e; an intransitive verb like “dreams” to e → t, a function from entities to truth values. The deduction step that combines “Mary” and “dreams” gives a term dreams(mary): a truth value.
The mapping from syntax to semantics is a homomorphism: each syntactic type is sent to a semantic type, and each syntactic proof becomes a semantic program. A transitive verb like “sees” gets (np\s)/np, which maps to e → e → t. When you plug in a subject and an object, the proof term builds sees(john,mary). The beautiful thing is that any proof in the syntactic calculus will produce a well-formed meaning recipe, automatically.
But there are limits. Some natural meaning combinations require the semantic target logic LP to do things that have no image in the syntactic source calculus NL or L. For example, the transformation called argument raising (turning an e type into a higher-order quantifier type) is needed to handle scope ambiguities like “Everyone loves someone”—but that combination is not valid in any syntactic calculus without global commutativity. This mismatch would drive the next wave of innovations.
When Grammar Gets Tricky: Gaps and Hidden Scope
Real language throws up challenges that simple NL or L cannot handle. Consider the sentence “I know what Mary put there.” The word “what” acts as if it fills a gap where a noun phrase should be, but that gap sits buried inside “Mary put — there.” In Lambek’s basic calculi, you cannot prove that “Mary put there” is of type np\s with an internal missing np, because the gap is not at the left or right edge.
To solve this, linguists extended the type logic with multimodal systems and control operators (written ◊, □). Think of these as licenses that let a word “move” through the structure under strict conditions, while still forbidding the free-for-all of global commutativity. For example, a special extraction mode allows a hypothesis to jump to a non-peripheral position before settling into its grammatical home. A word like “what” receives a type that mentions the control operator: wh / (s / ◊□ np). The ◊ on the np hypothesis says, “this np can travel across the tree until it’s needed,” and then the □ blocks further movement.
A related line of work, the Discontinuous Lambek Calculus, enriches the ontology with split strings—phrases that have built-in gaps, like “take — to task.” The wrapping product ⊙ and its residual operations allow a determinate handling of infixation and discontinuities, treating sentences as having internal split points that can be targeted.
These extensions also explained scope ambiguities. In “Alice thinks someone is cheating,” the quantifier “someone” can be understood narrowly (Alice thinks a specific person exists, but she’s wrong) or widely (there is a real person that Alice suspects). The extended proof system can produce both readings by varying the order of logical rules, yielding different meaning recipes—all while being disciplined enough to avoid nonsense.
Why This Still Matters: Machines, Brains, and the Logic of Thought
When you ask a voice assistant a question or use a translation app, part of what happens in the background is a variant of Lambek’s logic. The proof net approach—a way of representing grammatical deductions as geometric graphs—allows computers to parse sentences in real time, without getting lost in irrelevant bookkeeping. Proof nets for the associative Lambek calculus can be read off incrementally as you hear each word left-to-right, which matches how our own brains seem to process language.
These logical grammars also connect to deep questions about language learning. Because the type logic is radically lexicalized, the entire grammar of a language is boiled down to the types assigned to each word. There are no construction-specific rules. If a child can figure out the types of a few hundred words, the logic automatically determines which combinations are grammatical. This fits with evidence that young children learn language rapidly from noisy input, often without explicit correction.
The typelogical tradition has also opened a bridge between grammar and logic that goes both ways. Insights from linear logic (invented in 1987) fed back into linguistics, providing controlled structural rules through modalities. Meanwhile, the symmetric Lambek-Grishin calculus introduced a multiple-conclusion logic with co-implications, bringing classical logic to bear on grammar in ways that are still being explored for anaphora and ellipsis.
Next time you hear a sentence, consider that under the surface, a silent proof is running—a dance of types, residues, and deductions that orchestrates meaning. The hidden logic that lives inside every sentence is not just a philosophical curiosity; it’s a blueprint for how we, and the machines we build, learn to make sense of words.
Think about it
- If you invented a secret code where word order could be completely free, would that code be harder or easier for a computer to interpret? What about for a human child?
- Can you think of an English sentence that has two different meanings depending on how you group the words, like “I saw the man with a telescope”? How might a logic system assign two different proofs to it without getting confused?
- Do you think the basic shape of grammar—the way words combine in trees—is something our brains are born with, or do we learn it entirely from the speech around us? What evidence would convince you one way or the other?
