Horn 1989: Negation ambiguity for metalinguistic negation

@cite{horn-1989} @cite{horn-1985} @cite{burton-roberts-1989}

Horn, L. R. (1989). A Natural History of Negation. Univ. of Chicago Press. Foundation: Horn, L. R. (1985). Metalinguistic negation and pragmatic ambiguity. Language 61(1), 121–174.

Defining commitment

There are TWO negations in natural language: descriptive negation (truth-functional, targets at-issue content) and metalinguistic negation (objects to the appropriateness of the negated utterance, NOT to its truth conditions). The lexical item not is ambiguous between these two. Selection between them is constrained by syntactic and prosodic context.

This is the alternative analysis K-G argues against in §5 (paper p.29):

"The apparently metalinguistic character of metalinguistic negation is explained by the presence of covertly quoted material in the scope of the negation rather than by positing anything unusual about the negation operator itself, as suggested by Horn (1989) and Potts (2007)."

K-G's view: ONE negation operator + covert mixed quotation 𝔐 + appropriateness operator 𝔄 derives the same truth conditions and syntactic restrictions WITHOUT positing lexical ambiguity in not.

Three syntactic predictions Horn 1989 / Burton-Roberts 1989 identify

These are the empirical generalisations that any analysis of metalinguistic negation must derive. K-G (paper p.32) shows that the covert-mixed-quotation analysis derives all three; Horn's ambiguity analysis is committed to them by stipulating that metalinguistic negation is a distinct lexical item with these distributional restrictions baked in.

1. Morpheme incorporation failure (Horn 1989 p.392; @cite{horn-1985}): morphologically incorporated negation (unhappy) cannot host metalinguistic readings. "She's not happy, she's ecstatic" is fine; "#She's unhappy, she's ecstatic" is anomalous.

2. NPI licensing failure (Horn 1989): metalinguistic negation does not license NPIs. "John didn't manage to solve some of the problems" has a metalinguistic reading; "#John didn't manage to solve any of the problems" does not.

3. Double-negation-elimination failure (Burton-Roberts 1989, @cite{burton-roberts-1989}): when both negations are metalinguistic, ¬¬p is NOT equivalent to p. "She's not not happy, she's inconsolable" is fine; "#She's happy, she's inconsolable" is not.

Note on scope

Stub formalisation. Encodes Horn's two-negation commitment plus the three syntactic predictions as named theorems. Sufficient to host the K-G consilience theorem in KirkGiannini2024.lean: K-G derives the same three predictions WITHOUT lexical ambiguity in not.

inductive Horn1989.NegationKind : Type

Horn's two negations. The lexical item not is ambiguous between these.

• descriptive : NegationKind

  Descriptive (truth-functional) negation: targets at-issue.

• metalinguistic : NegationKind

  Metalinguistic negation: targets appropriateness of the utterance.

@[implicit_reducible]

instance Horn1989.instDecidableEqNegationKind : DecidableEq NegationKind

Equations

• Horn1989.instDecidableEqNegationKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Horn1989.instReprNegationKind : Repr NegationKind

Equations

• Horn1989.instReprNegationKind = { reprPrec := Horn1989.instReprNegationKind.repr }

def Horn1989.instReprNegationKind.repr : NegationKind → Nat → Std.Format

Equations

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

structure Horn1989.NegOccurrence (P : Type) : Type

A negation occurrence is one of the two kinds, plus the propositional target it scopes over.

• kind : NegationKind
• target : P

def Horn1989.instReprNegOccurrence.repr {P✝ : Type} [Repr P✝] : NegOccurrence P✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Horn1989.instReprNegOccurrence {P✝ : Type} [Repr P✝] : Repr (NegOccurrence P✝)

Equations

• Horn1989.instReprNegOccurrence = { reprPrec := Horn1989.instReprNegOccurrence.repr }

def Horn1989.IncorporatedNegation (P : Type) : Type

Horn 1989 prediction 1: morphological incorporation blocks metalinguistic readings. unhappy-style incorporated negations are necessarily descriptive — they cannot host metalinguistic correction.

Equations

• Horn1989.IncorporatedNegation P = { n : Horn1989.NegOccurrence P // n.kind = Horn1989.NegationKind.descriptive }

theorem Horn1989.incorporated_neg_is_descriptive (P : Type) (n : IncorporatedNegation P) : n.val.kind = NegationKind.descriptive

theorem Horn1989.incorporated_neg_blocks_metalinguistic (P : Type) (n : IncorporatedNegation P) : n.val.kind ≠ NegationKind.metalinguistic

inductive Horn1989.PolarityItem : Type

Horn 1989 prediction 2: NPIs are not licensed by metalinguistic negation. An NPI in the scope of metalinguistic not is ungrammatical. We encode this as a structural disallowance.

• npi : PolarityItem

  Negative polarity item (e.g., any, ever).

• ppi : PolarityItem

  Positive polarity item (e.g., some, already).

• neutral : PolarityItem

  Polarity-neutral.

@[implicit_reducible]

instance Horn1989.instDecidableEqPolarityItem : DecidableEq PolarityItem

Equations

• Horn1989.instDecidableEqPolarityItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Horn1989.instReprPolarityItem : Repr PolarityItem

Equations

• Horn1989.instReprPolarityItem = { reprPrec := Horn1989.instReprPolarityItem.repr }

def Horn1989.instReprPolarityItem.repr : PolarityItem → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Horn1989.instReprPolarityItem.repr Horn1989.PolarityItem.npi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Horn1989.PolarityItem.npi")).group prec✝
• Horn1989.instReprPolarityItem.repr Horn1989.PolarityItem.ppi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Horn1989.PolarityItem.ppi")).group prec✝

structure Horn1989.NegScopeOccurrence (P : Type) : Type

A polarity-marked occurrence in the scope of a negation.

• neg : NegOccurrence P
• polarity : PolarityItem

def Horn1989.instReprNegScopeOccurrence.repr {P✝ : Type} [Repr P✝] : NegScopeOccurrence P✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Horn1989.instReprNegScopeOccurrence {P✝ : Type} [Repr P✝] : Repr (NegScopeOccurrence P✝)

Equations

• Horn1989.instReprNegScopeOccurrence = { reprPrec := Horn1989.instReprNegScopeOccurrence.repr }

def Horn1989.NegScopeOccurrence.licit {P : Type} (occ : NegScopeOccurrence P) : Prop

An occurrence is licit iff NPIs only appear under descriptive negation.

Equations

• occ.licit = (occ.polarity = Horn1989.PolarityItem.npi → occ.neg.kind = Horn1989.NegationKind.descriptive)

theorem Horn1989.metalinguistic_neg_blocks_npi_licensing {P : Type} (occ : NegScopeOccurrence P) (h_meta : occ.neg.kind = NegationKind.metalinguistic) (h_npi : occ.polarity = PolarityItem.npi) : ¬occ.licit

@[reducible, inline]

abbrev Horn1989.NegChain (P : Type) : Type

Burton-Roberts 1989 prediction: DN-elimination fails for metalinguistic negations. When both ¬s in ¬¬p are metalinguistic, the result does NOT reduce to p. We encode this by tracking the negation chain and requiring that any pure descriptive double negation reduces, while a chain containing any metalinguistic negation does not.

Equations

• Horn1989.NegChain P = List (Horn1989.NegOccurrence P)

def Horn1989.NegChain.allDescriptive {P : Type} (chain : NegChain P) : Prop

All negations in the chain are descriptive.

Equations

• chain.allDescriptive = ∀ (n : Horn1989.NegOccurrence P), n ∈ chain → n.kind = Horn1989.NegationKind.descriptive

def Horn1989.NegChain.containsMetalinguistic {P : Type} (chain : NegChain P) : Prop

At least one negation in the chain is metalinguistic.

Equations

• chain.containsMetalinguistic = ∃ (n : Horn1989.NegOccurrence P), n ∈ chain ∧ n.kind = Horn1989.NegationKind.metalinguistic

def Horn1989.NegChain.dneEliminates {P : Type} (chain : NegChain P) : Prop

The DN-elimination condition: a chain reduces iff it's all-descriptive and length 2. (Length-2 condition is the prototypical DN case "not not happy"; the substantive predicate is allDescriptive.)

Equations

• chain.dneEliminates = (List.length chain = 2 ∧ chain.allDescriptive)

theorem Horn1989.metalinguistic_neg_blocks_dn_elimination {P : Type} (chain : NegChain P) (h : chain.containsMetalinguistic) : ¬chain.dneEliminates

Burton-Roberts 1989's syntactic prediction. A chain containing any metalinguistic negation fails DN-elimination — the surface "not not p" does NOT reduce to p when either negation has metalinguistic force.