English nouns

The English noun as a lexical entry is a ClassifiedNoun over no classifiers, which a numeral counts directly or not at all, with its lexical gender and its plural where it has them; a regular plural is the noun with the suffix English.Inflection.s. Names are the root ProperName. English nouns have no grammatical gender; the label recorded for man, woman and the names is the natural gender their pronouns agree with. Bare plurals and bare mass nouns are arguments and a bare singular count noun is not, which Chierchia derives from the Nominal Mapping Parameter (Studies/Chierchia1998.lean).

Main definitions

• numberSystem: the singular and the plural.
• Noun: the entry, with Noun.realize giving its form at a number.
• Noun.toWordSg, Noun.toWord: the entry as a Word token.

Implementation notes

Whether a numeral counts a noun and whether the noun has a plural are separate fields, since oats has a plural and no numeral counts it. A noun with a plural and no singular, such as oats, is not yet recorded: Noun.realize gives every entry its citation form as the singular.

References

• [Chi98]

structure English.Nouns.Nounextends ClassifiedNoun Empty : Type

An English noun is a classified noun over no classifiers, with its lexical gender and its plural where it has them.

• form : String
• gloss : String
• counters : Finset (Option Empty)
• gender : Option Gender

  The natural gender the noun's pronouns agree with, where it has one.

• plural : Option String

  The plural, where the noun has one.

@[instance_reducible]

instance English.Nouns.instDecidableEqNoun : DecidableEq Noun

Equations

• English.Nouns.instDecidableEqNoun = English.Nouns.instDecidableEqNoun.decEq

def English.Nouns.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def English.Nouns.Noun.common (form : String) : Noun

A common count noun, counted directly and with the regular -s plural; English is the metalanguage, so the gloss is the form.

Equations

• English.Nouns.Noun.common form = { form := form, gloss := form, counters := {none}, plural := some (English.Inflection.spell [Morphology.Morph.root form, English.Inflection.s]) }

def English.Nouns.Noun.mass (form : String) : Noun

A mass noun, which no numeral counts and which has no plural.

Equations

• English.Nouns.Noun.mass form = { form := form, gloss := form, counters := ∅ }

def English.Nouns.numberSystem : Number.System

English nouns distinguish two numbers, the singular and the plural.

Equations

• English.Nouns.numberSystem = { values := {Number.singular, Number.plural} }

def English.Nouns.Noun.realize (n : Noun) : Number → Option String

The form at a number is the citation form in the singular and the plural where the noun has one.

Equations

• n.realize Number.singular = some n.form
• n.realize Number.plural = n.plural
• n.realize x✝ = none

theorem English.Nouns.Noun.realize_eq_none (n : Noun) {m : Number} (hm : m ∉ numberSystem.values) : n.realize m = none

A noun has no form at a number outside the system.

def English.Nouns.Noun.toWordSg (n : Noun) : Morphology.Word

The singular word token is a NOUN with the gender where the entry has one.

Equations

• n.toWordSg = { form := n.form, cat := UD.UPOS.NOUN, features := Morphology.Features.of none (some Number.singular) n.gender }

def English.Nouns.Noun.toWord (n : Noun) (num : Number) : Option Morphology.Word

The entry as a word token at a number, where it has a form there.

Equations

• One or more equations did not get rendered due to their size.

theorem English.Nouns.Noun.toWord_singular (n : Noun) : n.toWord Number.singular = some n.toWordSg

Count nouns

def English.Nouns.pizza : Noun

Equations

• English.Nouns.pizza = English.Nouns.Noun.common "pizza"

def English.Nouns.book : Noun

Equations

• English.Nouns.book = English.Nouns.Noun.common "book"

def English.Nouns.cat : Noun

Equations

• English.Nouns.cat = English.Nouns.Noun.common "cat"

def English.Nouns.dog : Noun

Equations

• English.Nouns.dog = English.Nouns.Noun.common "dog"

def English.Nouns.girl : Noun

Equations

• English.Nouns.girl = English.Nouns.Noun.common "girl"

def English.Nouns.boy : Noun

Equations

• English.Nouns.boy = English.Nouns.Noun.common "boy"

def English.Nouns.ball : Noun

Equations

• English.Nouns.ball = English.Nouns.Noun.common "ball"

def English.Nouns.table : Noun

Equations

• English.Nouns.table = English.Nouns.Noun.common "table"

def English.Nouns.squirrel : Noun

Equations

• English.Nouns.squirrel = English.Nouns.Noun.common "squirrel"

def English.Nouns.kitchen : Noun

Equations

• English.Nouns.kitchen = English.Nouns.Noun.common "kitchen"

def English.Nouns.story : Noun

Equations

• English.Nouns.story = English.Nouns.Noun.common "story"

def English.Nouns.lawyer : Noun

Equations

• English.Nouns.lawyer = English.Nouns.Noun.common "lawyer"

def English.Nouns.student : Noun

Equations

• English.Nouns.student = English.Nouns.Noun.common "student"

def English.Nouns.teacher : Noun

Equations

• English.Nouns.teacher = English.Nouns.Noun.common "teacher"

def English.Nouns.soldier : Noun

Equations

• English.Nouns.soldier = English.Nouns.Noun.common "soldier"

def English.Nouns.horse : Noun

Equations

• English.Nouns.horse = English.Nouns.Noun.common "horse"

def English.Nouns.brother : Noun

Equations

• English.Nouns.brother = English.Nouns.Noun.common "brother"

def English.Nouns.spy : Noun

Equations

• English.Nouns.spy = English.Nouns.Noun.common "spy"

def English.Nouns.idea : Noun

Equations

• English.Nouns.idea = English.Nouns.Noun.common "idea"

def English.Nouns.lot : Noun

Equations

• English.Nouns.lot = English.Nouns.Noun.common "lot"

def English.Nouns.bean : Noun

Equations

• English.Nouns.bean = English.Nouns.Noun.common "bean"

def English.Nouns.lentil : Noun

Equations

• English.Nouns.lentil = English.Nouns.Noun.common "lentil"

def English.Nouns.spider : Noun

Equations

• English.Nouns.spider = English.Nouns.Noun.common "spider"

def English.Nouns.pollenGrain : Noun

Equations

• English.Nouns.pollenGrain = English.Nouns.Noun.common "pollen grain"

def English.Nouns.father : Noun

Equations

• English.Nouns.father = { toClassifiedNoun := (English.Nouns.Noun.common "father").toClassifiedNoun, gender := some Gender.masculine, plural := (English.Nouns.Noun.common "father").plural }

def English.Nouns.mother : Noun

Equations

• English.Nouns.mother = { toClassifiedNoun := (English.Nouns.Noun.common "mother").toClassifiedNoun, gender := some Gender.feminine, plural := (English.Nouns.Noun.common "mother").plural }

def English.Nouns.man : Noun

Equations

• English.Nouns.man = { toClassifiedNoun := (English.Nouns.Noun.common "man").toClassifiedNoun, gender := some Gender.masculine, plural := some "men" }

def English.Nouns.woman : Noun

Equations

• English.Nouns.woman = { toClassifiedNoun := (English.Nouns.Noun.common "woman").toClassifiedNoun, gender := some Gender.feminine, plural := some "women" }

def English.Nouns.fireman : Noun

Equations

• English.Nouns.fireman = { toClassifiedNoun := (English.Nouns.Noun.common "fireman").toClassifiedNoun, gender := (English.Nouns.Noun.common "fireman").gender, plural := some "firemen" }

def English.Nouns.person : Noun

Equations

• English.Nouns.person = { toClassifiedNoun := (English.Nouns.Noun.common "person").toClassifiedNoun, gender := (English.Nouns.Noun.common "person").gender, plural := some "people" }

def English.Nouns.child : Noun

Equations

• English.Nouns.child = { toClassifiedNoun := (English.Nouns.Noun.common "child").toClassifiedNoun, gender := (English.Nouns.Noun.common "child").gender, plural := some "children" }

Mass nouns

def English.Nouns.water : Noun

Equations

• English.Nouns.water = English.Nouns.Noun.mass "water"

def English.Nouns.sand : Noun

Equations

• English.Nouns.sand = English.Nouns.Noun.mass "sand"

def English.Nouns.trash : Noun

Equations

• English.Nouns.trash = English.Nouns.Noun.mass "trash"

def English.Nouns.furniture : Noun

Equations

• English.Nouns.furniture = English.Nouns.Noun.mass "furniture"

def English.Nouns.rice : Noun

Equations

• English.Nouns.rice = English.Nouns.Noun.mass "rice"

def English.Nouns.gold : Noun

Equations

• English.Nouns.gold = English.Nouns.Noun.mass "gold"

def English.Nouns.air : Noun

Equations

• English.Nouns.air = English.Nouns.Noun.mass "air"

def English.Nouns.wine : Noun

Equations

• English.Nouns.wine = English.Nouns.Noun.mass "wine"

def English.Nouns.coffee : Noun

Equations

• English.Nouns.coffee = English.Nouns.Noun.mass "coffee"

def English.Nouns.beer : Noun

Equations

• English.Nouns.beer = English.Nouns.Noun.mass "beer"

def English.Nouns.milk : Noun

Equations

• English.Nouns.milk = English.Nouns.Noun.mass "milk"

def English.Nouns.tea : Noun

Equations

• English.Nouns.tea = English.Nouns.Noun.mass "tea"

def English.Nouns.pollen : Noun

Equations

• English.Nouns.pollen = English.Nouns.Noun.mass "pollen"

def English.Nouns.mold : Noun

Equations

• English.Nouns.mold = English.Nouns.Noun.mass "mold"

Proper names

def English.Nouns.name (form : String) (gender : Option Gender := none) : ProperName

A name glossed by itself.

Equations

• English.Nouns.name form gender = { form := form, gloss := form, gender := gender }

def English.Nouns.john : ProperName

Equations

• English.Nouns.john = English.Nouns.name "John" (some Gender.masculine)

def English.Nouns.mary : ProperName

Equations

• English.Nouns.mary = English.Nouns.name "Mary" (some Gender.feminine)

def English.Nouns.bill : ProperName

Equations

• English.Nouns.bill = English.Nouns.name "Bill" (some Gender.masculine)

def English.Nouns.sue : ProperName

Equations

• English.Nouns.sue = English.Nouns.name "Sue" (some Gender.feminine)

def English.Nouns.fred : ProperName

Equations

• English.Nouns.fred = English.Nouns.name "Fred" (some Gender.masculine)

def English.Nouns.sam : ProperName

Equations

• English.Nouns.sam = English.Nouns.name "Sam"

def English.Nouns.pat : ProperName

Equations

• English.Nouns.pat = English.Nouns.name "Pat"