English Auxiliary Diagnostics: NICE Properties

@cite{huddleston-1976} @cite{palmer-2001}

@cite{huddleston-1976} coined the NICE acronym for four properties of English auxiliaries identified by @cite{palmer-2001}: Negation, Inversion, Code, Emphasis.

Property	Test	Example
Negation	Direct negation with not	He can not go
Inversion	Subject-aux inversion in questions	Can he go?
Code	VP ellipsis (stranding)	He can and she can too
Emphasis	Emphatic stress for verum focus	He CAN go

End-to-end chain

AuxEntry (Fragment) → AuxClass (Huddleston classification) → NICEProfile (4-Bool feature vector) → predictSAI → SAIDatum.acceptability.

Each link is a function, not a stipulated table. Changing a Fragment entry's form reroutes its AuxClass; changing predictSAI's rule breaks the bridge theorems against the SAI data; changing an SAI datum's acceptability breaks them too.

Types

inductive Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty : Type

The four NICE properties.

• negation : NICEProperty
• inversion : NICEProperty
• code : NICEProperty
• emphasis : NICEProperty

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Diagnostics.instDecidableEqNICEProperty : DecidableEq NICEProperty

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.instDecidableEqNICEProperty x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.AuxiliaryVerbs.Diagnostics.instReprNICEProperty.repr : NICEProperty → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Diagnostics.instReprNICEProperty : Repr NICEProperty

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.instReprNICEProperty = { reprPrec := Phenomena.AuxiliaryVerbs.Diagnostics.instReprNICEProperty.repr }

structure Phenomena.AuxiliaryVerbs.Diagnostics.NICEProfile : Type

A NICE profile records which of the 4 properties a form exhibits.

• negation : Bool
• inversion : Bool
• code : Bool
• emphasis : Bool

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Diagnostics.instReprNICEProfile : Repr NICEProfile

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.instReprNICEProfile = { reprPrec := Phenomena.AuxiliaryVerbs.Diagnostics.instReprNICEProfile.repr }

def Phenomena.AuxiliaryVerbs.Diagnostics.instReprNICEProfile.repr : NICEProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Diagnostics.instBEqNICEProfile : BEq NICEProfile

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.instBEqNICEProfile = { beq := Phenomena.AuxiliaryVerbs.Diagnostics.instBEqNICEProfile.beq }

def Phenomena.AuxiliaryVerbs.Diagnostics.instBEqNICEProfile.beq : NICEProfile → NICEProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.AuxiliaryVerbs.Diagnostics.instBEqNICEProfile.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Diagnostics.instDecidableEqNICEProfile : DecidableEq NICEProfile

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.instDecidableEqNICEProfile = Phenomena.AuxiliaryVerbs.Diagnostics.instDecidableEqNICEProfile.decEq

def Phenomena.AuxiliaryVerbs.Diagnostics.instDecidableEqNICEProfile.decEq (x✝ x✝¹ : NICEProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.AuxiliaryVerbs.Diagnostics.NICEProfile.has (p : NICEProfile) : NICEProperty → Bool

Project a profile by NICE property.

Equations

• p.has Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty.negation = p.negation
• p.has Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty.inversion = p.inversion
• p.has Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty.code = p.code
• p.has Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty.emphasis = p.emphasis

def Phenomena.AuxiliaryVerbs.Diagnostics.NICEProfile.count (p : NICEProfile) : ℕ

How many NICE properties does this profile exhibit?

Equations

• p.count = (((if p.negation = true then 1 else 0) + if p.inversion = true then 1 else 0) + if p.code = true then 1 else 0) + if p.emphasis = true then 1 else 0

def Phenomena.AuxiliaryVerbs.Diagnostics.NICEProfile.isFull (p : NICEProfile) : Bool

Full auxiliary: exhibits all 4 NICE properties.

Equations

• p.isFull = (p.count == 4)

def Phenomena.AuxiliaryVerbs.Diagnostics.NICEProfile.isSemi (p : NICEProfile) : Bool

Semi-auxiliary: some but not all.

Equations

• p.isSemi = decide (0 < p.count ∧ p.count < 4)

def Phenomena.AuxiliaryVerbs.Diagnostics.NICEProfile.isLexical (p : NICEProfile) : Bool

Lexical verb (no NICE properties).

Equations

• p.isLexical = (p.count == 0)

Huddleston classification

@cite{huddleston-1976} groups English auxiliaries into three NICE classes:

• Full: modals + do/be/have — all four properties.
• Semi (N+I): dare, need — Negation and Inversion only.
• Semi (N+E): ought — Negation and Emphasis only (Inversion is conservative; Ought he to go? is grammatical for many BrE speakers).

inductive Phenomena.AuxiliaryVerbs.Diagnostics.AuxClass : Type

NICE-diagnostic class of an auxiliary.

• full : AuxClass
• semiNI : AuxClass
• semiNE : AuxClass

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Diagnostics.instDecidableEqAuxClass : DecidableEq AuxClass

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.instDecidableEqAuxClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.AuxiliaryVerbs.Diagnostics.instReprAuxClass.repr : AuxClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.AuxiliaryVerbs.Diagnostics.instReprAuxClass : Repr AuxClass

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.instReprAuxClass = { reprPrec := Phenomena.AuxiliaryVerbs.Diagnostics.instReprAuxClass.repr }

def Phenomena.AuxiliaryVerbs.Diagnostics.AuxClass.toNICE : AuxClass → NICEProfile

The NICE feature vector predicted by Huddleston's class.

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.AuxClass.full.toNICE = { negation := true, inversion := true, code := true, emphasis := true }
• Phenomena.AuxiliaryVerbs.Diagnostics.AuxClass.semiNI.toNICE = { negation := true, inversion := true, code := false, emphasis := false }
• Phenomena.AuxiliaryVerbs.Diagnostics.AuxClass.semiNE.toNICE = { negation := true, inversion := false, code := false, emphasis := true }

def Phenomena.AuxiliaryVerbs.Diagnostics.auxClass (e : Fragments.English.Auxiliaries.AuxEntry) : AuxClass

Classify a Fragment auxiliary entry per Huddleston's NICE diagnostic. Only dare, need, ought are semi; everything else in the Fragment auxiliary inventory is full.

Equations

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

def Phenomena.AuxiliaryVerbs.Diagnostics.nice (e : Fragments.English.Auxiliaries.AuxEntry) : NICEProfile

NICE profile for a Fragment auxiliary entry, derived from its class.

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.nice e = (Phenomena.AuxiliaryVerbs.Diagnostics.auxClass e).toNICE

def Phenomena.AuxiliaryVerbs.Diagnostics.lexicalVerbNICE : NICEProfile

NICE profile for a non-auxiliary lexical verb (no NICE properties).

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.lexicalVerbNICE = { negation := false, inversion := false, code := false, emphasis := false }

Contracted negation (Fragment-derived)

@cite{huddleston-1976} notes that NICE Negation concerns direct not- negation; contracted negation (-n't) is a stronger sub-property with paradigm gaps at may and am. The negForm : Option String field in AuxEntry records each entry's contracted form (or absence).

def Phenomena.AuxiliaryVerbs.Diagnostics.hasContractedNeg (e : Fragments.English.Auxiliaries.AuxEntry) : Bool

Whether a Fragment entry has a contracted negative form.

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.hasContractedNeg e = e.negForm.isSome

theorem Phenomena.AuxiliaryVerbs.Diagnostics.can_has_neg : hasContractedNeg Fragments.English.Auxiliaries.can = true

theorem Phenomena.AuxiliaryVerbs.Diagnostics.will_has_neg : hasContractedNeg Fragments.English.Auxiliaries.will = true

theorem Phenomena.AuxiliaryVerbs.Diagnostics.is_has_neg : hasContractedNeg Fragments.English.Auxiliaries.is_ = true

theorem Phenomena.AuxiliaryVerbs.Diagnostics.do_has_neg : hasContractedNeg Fragments.English.Auxiliaries.do_ = true

theorem Phenomena.AuxiliaryVerbs.Diagnostics.have_has_neg : hasContractedNeg Fragments.English.Auxiliaries.have_ = true

theorem Phenomena.AuxiliaryVerbs.Diagnostics.need_has_neg : hasContractedNeg Fragments.English.Auxiliaries.need = true

theorem Phenomena.AuxiliaryVerbs.Diagnostics.dare_has_neg : hasContractedNeg Fragments.English.Auxiliaries.dare = true

theorem Phenomena.AuxiliaryVerbs.Diagnostics.ought_has_neg : hasContractedNeg Fragments.English.Auxiliaries.ought = true

theorem Phenomena.AuxiliaryVerbs.Diagnostics.may_lacks_neg : hasContractedNeg Fragments.English.Auxiliaries.may = false

theorem Phenomena.AuxiliaryVerbs.Diagnostics.am_lacks_neg : hasContractedNeg Fragments.English.Auxiliaries.am = false

Aggregate collections

def Phenomena.AuxiliaryVerbs.Diagnostics.allFullAuxiliaries : List Fragments.English.Auxiliaries.AuxEntry

Full auxiliaries (modals + do/be/have).

Equations

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

def Phenomena.AuxiliaryVerbs.Diagnostics.allSemiModals : List Fragments.English.Auxiliaries.AuxEntry

Semi-modals (Huddleston's N+I and N+E classes combined).

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.allSemiModals = [Fragments.English.Auxiliaries.need, Fragments.English.Auxiliaries.dare, Fragments.English.Auxiliaries.ought]

def Phenomena.AuxiliaryVerbs.Diagnostics.allAuxiliaries : List Fragments.English.Auxiliaries.AuxEntry

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.allAuxiliaries = Phenomena.AuxiliaryVerbs.Diagnostics.allFullAuxiliaries ++ Phenomena.AuxiliaryVerbs.Diagnostics.allSemiModals

theorem Phenomena.AuxiliaryVerbs.Diagnostics.all_full_classify_full : (allFullAuxiliaries.all fun (e : Fragments.English.Auxiliaries.AuxEntry) => (nice e).isFull) = true

Every full auxiliary classifies as full under nice.

theorem Phenomena.AuxiliaryVerbs.Diagnostics.all_semi_classify_semi : (allSemiModals.all fun (e : Fragments.English.Auxiliaries.AuxEntry) => (nice e).isSemi) = true

Every semi-modal classifies as semi under nice.

SAI prediction from NICE profile

NICE properties predict participation in specific SAI contexts:

NICE Property	SAI Context	Aux example	Lex verb (do-support)
Inversion	matrixWh / matrixYN	Can he go?	Does he go?
Negation	sententialNegation	Sue is not eating	Sue does not eat
Code	vpEllipsis	She can too	He does too
Emphasis	emphatic	She IS eating	Sue DOES eat

Other SAI contexts (embedded, echo, conditional inversion, ...) are not directly diagnosed by NICE — for those, predictSAI defers to grammatical since NICE does not constrain them.

def Phenomena.AuxiliaryVerbs.Diagnostics.saiContextNICE : WordOrder.SubjectAuxInversion.SAIContext → Option NICEProperty

The NICE property that an SAI context diagnoses (if any).

Equations

• Phenomena.AuxiliaryVerbs.Diagnostics.saiContextNICE Phenomena.WordOrder.SubjectAuxInversion.SAIContext.matrixWh = some Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty.inversion
• Phenomena.AuxiliaryVerbs.Diagnostics.saiContextNICE Phenomena.WordOrder.SubjectAuxInversion.SAIContext.matrixYN = some Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty.inversion
• Phenomena.AuxiliaryVerbs.Diagnostics.saiContextNICE Phenomena.WordOrder.SubjectAuxInversion.SAIContext.sententialNegation = some Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty.negation
• Phenomena.AuxiliaryVerbs.Diagnostics.saiContextNICE Phenomena.WordOrder.SubjectAuxInversion.SAIContext.vpEllipsis = some Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty.code
• Phenomena.AuxiliaryVerbs.Diagnostics.saiContextNICE Phenomena.WordOrder.SubjectAuxInversion.SAIContext.emphatic = some Phenomena.AuxiliaryVerbs.Diagnostics.NICEProperty.emphasis
• Phenomena.AuxiliaryVerbs.Diagnostics.saiContextNICE x✝ = none

def Phenomena.AuxiliaryVerbs.Diagnostics.predictSAI (p : NICEProfile) (ctx : WordOrder.SubjectAuxInversion.SAIContext) : WordOrder.SubjectAuxInversion.Acceptability

Predict SAI acceptability from a NICE profile. The verb's profile must license the NICE property the context diagnoses; otherwise the prediction is ungrammatical (do-support is the standard repair — modeled by giving do_ the auxiliary profile and predicting from that, rather than via predicate-internal repair logic).

Equations

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

Bridge: predictSAI agrees with the SAI table

A representative sample of (NICE-profile, SAIDatum) pairs covering auxiliary-passes and lexical-verb-fails for each NICE property, plus do-support successes (where do itself is the auxiliary).

def Phenomena.AuxiliaryVerbs.Diagnostics.predictionTable : List (NICEProfile × WordOrder.SubjectAuxInversion.SAIDatum)

Pairs of (NICE profile, SAI datum) where predictSAI should reproduce the datum's acceptability.

Equations

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

theorem Phenomena.AuxiliaryVerbs.Diagnostics.predictSAI_agrees : (predictionTable.all fun (x : NICEProfile × WordOrder.SubjectAuxInversion.SAIDatum) => match x with | (p, d) => predictSAI p d.context == d.acceptability) = true

predictSAI agrees with the SAI table on every entry of predictionTable. Changing nice, predictSAI, saiContextNICE, or any SAIDatum.acceptability referenced above breaks this theorem.