Ontological categories of pro-forms

The members of an interrogative or indefinite series differ in the ontological category they stand for: a person (who, someone), a thing (what, something), a place (where, somewhere) and so on. The category fixes the word class of the member, a pro-adverb for a place, a time or a manner and a pronoun otherwise.

Main definitions

• Pronoun.OntologicalCategory: the categories pro-forms stand for.
• Pronoun.OntologicalCategory.upos: the word class a category fixes.

References

• [Has97]

inductive Pronoun.OntologicalCategory : Type

The ontological categories of pro-forms. Person, thing, property, place, time, manner and amount are the seven Haspelmath finds expressed by simple means in most languages, the cut between person and thing (somebody against something) being made nearly everywhere. Determiners (some N) and reasons (for some reason) are common but not universal, English and German having no somewhy.

• person : OntologicalCategory

  Person is the category of somebody, someone and interrogative who.

• thing : OntologicalCategory

  Thing is the category of something and interrogative what.

• property : OntologicalCategory

  Property or kind is the category of some kind of and interrogative what kind.

• place : OntologicalCategory

  Place is the category of somewhere and interrogative where.

• time : OntologicalCategory

  Time is the category of sometime and interrogative when.

• manner : OntologicalCategory

  Manner is the category of somehow and interrogative how.

• amount : OntologicalCategory

  Amount is the category of some amount and interrogative how much.

• determiner : OntologicalCategory

  Determiner is the category of some N and interrogative which.

• reason : OntologicalCategory

  Reason is the category of for some reason and interrogative why.

@[instance_reducible]

instance Pronoun.instDecidableEqOntologicalCategory : DecidableEq OntologicalCategory

Equations

• Pronoun.instDecidableEqOntologicalCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Pronoun.instReprOntologicalCategory : Repr OntologicalCategory

Equations

• Pronoun.instReprOntologicalCategory = { reprPrec := Pronoun.instReprOntologicalCategory.repr }

def Pronoun.instReprOntologicalCategory.repr : OntologicalCategory → ℕ → Std.Format

Equations

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

def Pronoun.OntologicalCategory.IsAdverbial (c : OntologicalCategory) : Prop

A category is adverbial when its pro-forms are pro-adverbs, of a place, a time or a manner.

Equations

• c.IsAdverbial = (c = Pronoun.OntologicalCategory.place ∨ c = Pronoun.OntologicalCategory.time ∨ c = Pronoun.OntologicalCategory.manner)

@[instance_reducible]

instance Pronoun.OntologicalCategory.instDecidablePredIsAdverbial : DecidablePred IsAdverbial

Equations

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

def Pronoun.OntologicalCategory.upos (c : OntologicalCategory) : UD.UPOS

The word class of a pro-form is an adverb in an adverbial category and a pronoun otherwise.

Equations

• c.upos = if c.IsAdverbial then UD.UPOS.ADV else UD.UPOS.PRON