Editing Higher order grammar (section)

==Key features==

* There is a [[Propositional calculus|propositional logic]] of '''types''', which denote sets of linguistic (phonological, syntactic, or semantic) entities. For example, the type NP denotes the syntactic category (or form class) of [[noun phrase]]s.
* HOG maintains [[Haskell Curry]]'s distinction between '''tectogrammatical structure''' (abstract [[syntax]]) and '''phenogrammatical structure''' (concrete syntax).
* Abstract syntactic entities are identified with [[Structuralism#Structuralism in linguistics|structuralist]] ([[Leonard Bloomfield|Bloomfield]]-[[Charles F. Hockett|Hockett]]) free forms (words and phrases). For example, the NP ''your cat'' is distinct from its [[phonology]] or its [[semantics]].
* Concrete syntax is identified with [[phonology]], broadly construed to include word order.
* The modelling of [[Sense and reference|Fregean senses]] is broadly similar to [[Montague grammar|Montague]]'s, but with intensions replaced by finer-grained '''hyperintensions'''.
* There is a ([[Curry-Howard]]) '''proof term calculus''', whose terms denote linguistic (phonological, syntactic, or semantic) entities.
* The term calculus is embedded in a classical [[higher-order logic]] (HOL).
* The syntax-phonology and [[Syntax‐semantics interface|syntax-semantics interface]]s are expressed as axiomatic theories in the HOL.
* The HOL admits (separation-style) [[subtyping]], e.g. NPacc, the type of [[accusative case|accusative]] noun phrases, is a subtype of NP, and denotes a subset of the category denoted by NP.