Natural Logic

Origin. Johan van Benthem, Essays in Logical Semantics (Reidel, 1986) and Language in Action: Categories, Lambdas and Dynamic Logic (North-Holland, 1991), proposed computing entailment on surface forms by marking monotonicity through a categorial parse; Víctor Sánchez Valencia's dissertation Studies on Natural Logic and Categorial Grammar (University of Amsterdam, 1991), written under van Benthem, turned the proposal into the polarity-marking algorithm over Lambek derivations. The dictum de omni et nullo and the terminist conditions of descent and ascent sort term occurrences by the direction of licensed substitution (see Medieval Terminist Logic), Sánchez Valencia's historical chapters trace monotonicity inference through Ockham, Leibniz, De Morgan and Peirce, and Fred Sommers, The Logic of Natural Language (1982), revived term logic with the same ambition of inference on surface form. Icard and Moss, "Recent Progress on Monotonicity" (Linguistic Issues in Language Technology 9, 2014, 167–194), surveys the modern programme.

Models. Entailment computed on the surface string, with no translation into a logical formula: order the denotations at every type by ≤, mark each argument position of a functional type as order-preserving or order-reversing, propagate the marks through a parse, and infer by substitution along ≤. The calculus is the proof-theoretic face of the monotonicity facts of generalized quantifier theory — that every is downward in its restrictor and upward in its scope is at once a model-theoretic property of the determiner and a license to substitute (see Generalized Quantifier Theory) — and it formalizes what the syllogistic and terminist traditions practiced.

Formalism.

The order: ≤ on each base type, lifted pointwise at function types. puppy ≤ dog ≤ animal; waltz ≤ dance ≤ move.

Marked types: Each argument position of a functional type marked ↑ (order-preserving) or ↓ (order-reversing), or unmarked. every: restrictor ↓, scope ↑. some: ↑, ↑. no: ↓, ↓. not: ↓. most: restrictor unmarked, scope ↑.

Polarity marking (Sánchez Valencia 1991): Parse in a categorial grammar. Mark each leaf with its lexical ↑/↓ profile. An occurrence's polarity is the composition of the marks on its path to the root: an even number of ↓ makes it positive, odd negative.

Inference by substitution: Positive occurrence of t, and t ≤ t′: replace t by t′. Negative occurrence of t, and t″ ≤ t: replace t by t″. Every dog↓ barks↑: "Every puppy barks"; "Every dog moves". Not every dog↑ barks↓: each ↓ on the path flips the marks beneath it.

Completeness of the calculus: Icard, Moss and Tune, "A Monotonicity Calculus and Its Completeness" (Mathematics of Language, 2017).

Syllogistic fragments (Moss's programme): Moss, "Completeness Theorems for Syllogistic Fragments" (in Hamm and Kepser, eds., Logics for Linguistic Structures, 2008, 143–173): complete finite rule systems for All/Some fragments and extensions. Pratt-Hartmann and Moss, "Logics for the Relational Syllogistic" (Review of Symbolic Logic 2(4), 2009, 647–683): for fragments with transitive verbs and relative clauses, which have syllogistic proof systems, which need reductio, which have none — with the complexity of each fragment determined. Endrullis and Moss, "Syllogistic Logic with 'Most'" (WoLLIC 2015; Mathematical Structures in Computer Science 29(6), 2019, 763–782): sound and complete for All/Some/Most on finite models; infinitely many rules, provably unavoidable; decidable in polynomial time.

The seven relations (MacCartney and Manning, NatLog, 2007–2009): ≡ equivalence (couch, sofa). ⊏ strict forward entailment (crow, bird); ⊐ its converse. ^ negation: exhaustive exclusion (human, nonhuman). | alternation: non-exhaustive exclusion (cat, dog). ⌣ cover: non-exclusive exhaustion (animal, nonhuman).

independence (hungry, hippo).

Projectivity: how each operator maps each of the seven — the generalization of monotonicity to exclusion. Inference: decompose a premise–hypothesis pair into atomic edits and compose the edits' relations.

Symbols.

Metatheory. Sánchez Valencia (1991) proved the marking algorithm sound with respect to the standard semantics; Icard, Moss and Tune (2017) proved the monotonicity calculus complete. The syllogistic wing has exact results on both sides: complete axiomatizations for the All/Some fragments and extensions (Moss 2008), a map of the relational fragments separating those with syllogistic proof systems from those provably without (Pratt-Hartmann and Moss 2009, with the complexity of each fragment), and for All/Some/Most a system that is complete and provably requires infinitely many rules (Endrullis and Moss 2019) — a completeness theorem and an impossibility theorem about the same fragment. The marking reads off the monotonicity profiles that generalized quantifier theory establishes for determiners, and Ladusaw's negative-polarity diagnostic is the empirical trace of the same ↓ positions (see Generalized Quantifier Theory).

Applies to. Natural language inference: MacCartney and Manning's NatLog composes the seven relations along edit chains. Polarity computation and negative-polarity-item diagnosis. Computational semantics without logical forms. Reading the syllogistic and terminist traditions, which the calculus retrospectively formalizes.

Limitations. No full Boolean reasoning: the calculus substitutes along ≤ and does nothing else, so an inference that rewrites ¬(A ∧ B) as ¬A ∨ ¬B is not a substitution and falls outside it — the de Morgan dualities need machinery the calculus does not have. Containment alone misses contradiction, and the seven-relation repair degrades under composition: chains of edits lose information and collapse toward #, which is why NatLog is a deliberately weak proof procedure. Completeness holds only inside the delimited fragments: multi-premise reasoning beyond them has no completeness theorem, some relational fragments provably lack any syllogistic system (Pratt-Hartmann and Moss 2009), and Most already requires infinitely many rules. Non-monotone positions block the method entirely — the restrictor of most licenses no substitution in either direction. And marking presupposes a parse: a scope-ambiguous sentence carries a distinct marking per reading, so the calculus inherits disambiguation rather than performing it.

© 2026 Lingenic LLC