Napoli & Nespor (1976): Negatives in Comparatives

This file formalizes [NN76]'s account of the Italian non that appears in comparative clauses without reversing truth conditions, Maria è più intelligente di quanto non sia Carlo 'Maria is more intelligent than Carlo is'. Against [AP71]'s pleonastic element and [Seu69]'s underlyingly negative than-clause, the paper takes this non₂ to be real negation licensed by the discourse move: the speaker presupposes that the assertion contradicts a belief inferred from the interlocutor's prior discourse, the move is an assertion, the matrix clause is not negated, and the construction does not demand precise knowledge of the compared degrees (Move.Licensed). The acceptability paradigm of dialogues between Dario and Paolo, comparative constructions, and an indirect question records the facts of each move with the reported judgment, and paradigm_licensed_iff shows the four conditions reproduce every judgment. Six morphosyntactic diagnostics witness the underlying negation: subjunctive mood and non-specific indefinites in the than-clause, the complementizer che, the predicative clitic lo, neanche-conjunction, and the weak NPI pur. The NPI affatto, which requires precise knowledge of the listener's belief, is excluded from every non₂-comparative by the precision condition (pur_admissible, affatto_blocked).

Implementation notes

The paper's own implementation, a Generative Semantics abstract higher clause hosting non₂ and optionally deleted, is not formalized; only the licensing conditions and their surface diagnostics are. The paper's condition on precision splits into two facts of a move: whether the contradicted belief was inferred or stated explicitly, and whether the construction, an equality comparative or an explicit degree modifier, demands precise knowledge of the degrees.

References

• [NN76]
• [AP71]
• [Seu69]

TODO

The paradigm's moves are typed from the paper's descriptions of its dialogues; the dialogues themselves are not yet rows of Data/Examples/NapoliNespor1976.json.

The licensing condition

inductive NapoliNespor1976.PriorBelief : Type

The speaker's relation to the belief the assertion contradicts.

• inferred : PriorBelief

  The interlocutor's prior discourse implies a contrary belief.

• explicit : PriorBelief

  The interlocutor stated the contrary belief explicitly.

• absent : PriorBelief

  No contrary belief is in play.

@[instance_reducible]

instance NapoliNespor1976.instDecidableEqPriorBelief : DecidableEq PriorBelief

Equations

• NapoliNespor1976.instDecidableEqPriorBelief x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NapoliNespor1976.instReprPriorBelief : Repr PriorBelief

Equations

• NapoliNespor1976.instReprPriorBelief = { reprPrec := NapoliNespor1976.instReprPriorBelief.repr }

def NapoliNespor1976.instReprPriorBelief.repr : PriorBelief → ℕ → Std.Format

Equations

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

inductive NapoliNespor1976.Construction : Type

The constructions hosting a non₂ candidate.

• piu : Construction

  più … di quanto.

• meno : Construction

  meno … di quanto.

• equality : Construction

  The equality comparative tanto … quanto.

• explicitDegree : Construction

  A comparative with an explicit degree modifier, molto più, due metri più.

• indirectQuestion : Construction

  An indirect question, chissà se.

@[instance_reducible]

instance NapoliNespor1976.instDecidableEqConstruction : DecidableEq Construction

Equations

• NapoliNespor1976.instDecidableEqConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NapoliNespor1976.instReprConstruction.repr : Construction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NapoliNespor1976.instReprConstruction : Repr Construction

Equations

• NapoliNespor1976.instReprConstruction = { reprPrec := NapoliNespor1976.instReprConstruction.repr }

def NapoliNespor1976.Construction.Precise (c : Construction) : Prop

The construction demands precise knowledge of the compared degrees.

Equations

• c.Precise = (c = NapoliNespor1976.Construction.equality ∨ c = NapoliNespor1976.Construction.explicitDegree)

@[instance_reducible]

instance NapoliNespor1976.instDecidablePrecise (c : Construction) : Decidable c.Precise

Equations

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

structure NapoliNespor1976.Move : Type

A discourse move hosting a non₂ candidate.

• priorBelief : PriorBelief
• force : Discourse.SpeechAct.Force
• matrix : Polarity
• construction : Construction

def NapoliNespor1976.instDecidableEqMove.decEq (x✝ x✝¹ : Move) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance NapoliNespor1976.instDecidableEqMove : DecidableEq Move

Equations

• NapoliNespor1976.instDecidableEqMove = NapoliNespor1976.instDecidableEqMove.decEq

def NapoliNespor1976.instReprMove.repr : Move → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NapoliNespor1976.instReprMove : Repr Move

Equations

• NapoliNespor1976.instReprMove = { reprPrec := NapoliNespor1976.instReprMove.repr }

def NapoliNespor1976.Move.Licensed (m : Move) : Prop

The licensing condition on non₂: the assertion contradicts a belief the speaker inferred from the interlocutor's discourse, the move is an assertion, the matrix is affirmative, and the construction does not demand precision.

Equations

• m.Licensed = (m.priorBelief = NapoliNespor1976.PriorBelief.inferred ∧ m.force = Discourse.SpeechAct.Force.declarative ∧ m.matrix = Polarity.positive ∧ ¬m.construction.Precise)

@[instance_reducible]

instance NapoliNespor1976.instDecidableLicensed (m : Move) : Decidable m.Licensed

Equations

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

The acceptability paradigm

Four dialogues between Dario and Paolo vary the speaker's epistemic state, comparative constructions isolate the remaining conditions, with meno-comparatives as the positive control, and an indirect question shows the condition is a property of the move rather than of comparative syntax.

structure NapoliNespor1976.Row : Type

A row of the paradigm: the move and the reported acceptability of non₂.

• move : Move
• judgment : Judgment

def NapoliNespor1976.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

• NapoliNespor1976.instDecidableEqRow.decEq { move := a, judgment := a_1 } { move := b, judgment := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance NapoliNespor1976.instDecidableEqRow : DecidableEq Row

Equations

• NapoliNespor1976.instDecidableEqRow = NapoliNespor1976.instDecidableEqRow.decEq

def NapoliNespor1976.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NapoliNespor1976.instReprRow : Repr Row

Equations

• NapoliNespor1976.instReprRow = { reprPrec := NapoliNespor1976.instReprRow.repr }

def NapoliNespor1976.assertion (b : PriorBelief) : Move

An assertion of Maria è più intelligente di quanto non sia Carlo against a prior belief of the given status.

Equations

• NapoliNespor1976.assertion b = { priorBelief := b, force := Discourse.SpeechAct.Force.declarative, matrix := Polarity.positive, construction := NapoliNespor1976.Construction.piu }

def NapoliNespor1976.noOpinionContext : Row

Dario gives no opinion of Maria or Carlo; Paolo asserts that Maria is more intelligent.

Equations

• NapoliNespor1976.noOpinionContext = { move := NapoliNespor1976.assertion NapoliNespor1976.PriorBelief.absent, judgment := Judgment.unacceptable }

def NapoliNespor1976.chessContext : Row

Dario implies Carlo would beat Maria at chess; Paolo asserts that Maria is more intelligent.

Equations

• NapoliNespor1976.chessContext = { move := NapoliNespor1976.assertion NapoliNespor1976.PriorBelief.inferred, judgment := Judgment.acceptable }

def NapoliNespor1976.explicitCriticismContext : Row

Dario calls Maria stupid in so many words; Paolo disagrees.

Equations

• NapoliNespor1976.explicitCriticismContext = { move := NapoliNespor1976.assertion NapoliNespor1976.PriorBelief.explicit, judgment := Judgment.unacceptable }

def NapoliNespor1976.complaintContext : Row

Dario's complaint implies he expects Maria cannot help; Paolo asserts she is smart enough to ask.

Equations

• NapoliNespor1976.complaintContext = { move := NapoliNespor1976.assertion NapoliNespor1976.PriorBelief.inferred, judgment := Judgment.acceptable }

def NapoliNespor1976.questionedComparative : Row

È più intelligente di quanto non sia Carlo?: the move is a question.

Equations

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

def NapoliNespor1976.matrixNegatedComparative : Row

Maria non è più intelligente di quanto non sia Carlo: the matrix is negated.

Equations

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

def NapoliNespor1976.equalityComparative : Row

Maria è tanto intelligente quanto è Carlo: an equality comparative demands precise knowledge of the compared degrees.

Equations

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

def NapoliNespor1976.precisionComparative : Row

Molto più intelligente, due metri più alta: an explicit degree modifier demands precise knowledge of the gap.

Equations

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

def NapoliNespor1976.menoComparative : Row

Maria è meno intelligente di quanto tu non creda: a meno-comparative admits non₂ under the same conditions as più, while a negated equality comparative, semantically close to it, rejects non₂, so the equality restriction cannot reduce to equality linking two similar things (contra [Seu69] and [AP71]).

Equations

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

def NapoliNespor1976.chissaSeNon : Row

Chissà se non vale la pena di comprarlo: an indirect question whose negated proposition the speaker presupposes to be contrary to expectation.

Equations

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

def NapoliNespor1976.paradigm : List Row

The paper's acceptability paradigm.

Equations

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

theorem NapoliNespor1976.paradigm_licensed_iff (r : Row) : r ∈ paradigm → (r.move.Licensed ↔ r.judgment = Judgment.acceptable)

The four conditions reproduce the paper's judgment on every row, each condition failing on its own row.

Morphosyntactic diagnostics for underlying negation

Two diagnostics are forced choices in the than-clause, mood and the specificity of indefinites; four are admissibility asymmetries, in which the marked alternant (the complementizer che, the predicative clitic lo, neanche-conjunction, the weak NPI pur) is possible only under licensed non₂ while the default (di quanto, a repeated predicate, plain conjunction) remains available throughout.

inductive NapoliNespor1976.SpecificityProfile : Type

Specificity of indefinites embedded in the than-clause.

• unrestricted : SpecificityProfile

  Both specific and non-specific readings are available.

• nonspecificOnly : SpecificityProfile

  Only the non-specific reading, under the scope of underlying negation.

@[instance_reducible]

instance NapoliNespor1976.instDecidableEqSpecificityProfile : DecidableEq SpecificityProfile

Equations

• NapoliNespor1976.instDecidableEqSpecificityProfile x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NapoliNespor1976.instReprSpecificityProfile : Repr SpecificityProfile

Equations

• NapoliNespor1976.instReprSpecificityProfile = { reprPrec := NapoliNespor1976.instReprSpecificityProfile.repr }

def NapoliNespor1976.instReprSpecificityProfile.repr : SpecificityProfile → ℕ → Std.Format

Equations

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

inductive NapoliNespor1976.Complementizer : Type

The Italian comparative complementizers.

• diQuanto : Complementizer

  The default than-complementizer.

• che : Complementizer

  The alternant admissible only under non₂.

@[instance_reducible]

instance NapoliNespor1976.instDecidableEqComplementizer : DecidableEq Complementizer

Equations

• NapoliNespor1976.instDecidableEqComplementizer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NapoliNespor1976.instReprComplementizer : Repr Complementizer

Equations

• NapoliNespor1976.instReprComplementizer = { reprPrec := NapoliNespor1976.instReprComplementizer.repr }

def NapoliNespor1976.instReprComplementizer.repr : Complementizer → ℕ → Std.Format

Equations

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

inductive NapoliNespor1976.Clitic : Type

Whether the predicative clitic lo substitutes for a repeated predicate adjective in the than-clause.

• present : Clitic
• absent : Clitic

@[instance_reducible]

instance NapoliNespor1976.instDecidableEqClitic : DecidableEq Clitic

Equations

• NapoliNespor1976.instDecidableEqClitic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NapoliNespor1976.instReprClitic.repr : Clitic → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NapoliNespor1976.instReprClitic : Repr Clitic

Equations

• NapoliNespor1976.instReprClitic = { reprPrec := NapoliNespor1976.instReprClitic.repr }

def NapoliNespor1976.predictedMood (m : Move) : Mood.Grammatical

Mood of the than-clause: subjunctive exactly under licensed non₂, the paper's optional deletion of non₂ deriving surface subjunctive without non; lexical mood control by credere and its kin is abstracted away.

Equations

• NapoliNespor1976.predictedMood m = if m.Licensed then Mood.Grammatical.subjunctive else Mood.Grammatical.indicative

def NapoliNespor1976.predictedSpecificity (m : Move) : SpecificityProfile

Embedded indefinites are restricted to the non-specific reading under licensed non₂.

Equations

• NapoliNespor1976.predictedSpecificity m = if m.Licensed then NapoliNespor1976.SpecificityProfile.nonspecificOnly else NapoliNespor1976.SpecificityProfile.unrestricted

def NapoliNespor1976.ComplementizerAdmissible (m : Move) : Complementizer → Prop

Di quanto occurs with and without non₂; che only with it.

Equations

• NapoliNespor1976.ComplementizerAdmissible m NapoliNespor1976.Complementizer.diQuanto = True
• NapoliNespor1976.ComplementizerAdmissible m NapoliNespor1976.Complementizer.che = m.Licensed

def NapoliNespor1976.CliticAdmissible (m : Move) : Clitic → Prop

A clitic-less comparative is always available; lo only under non₂, and optionally.

Equations

• NapoliNespor1976.CliticAdmissible m NapoliNespor1976.Clitic.present = m.Licensed
• NapoliNespor1976.CliticAdmissible m NapoliNespor1976.Clitic.absent = True

def NapoliNespor1976.NegationAdmissible (m : Move) (e : PolarityItem) : Prop

An item that needs its clause negated at some level, neanche in a conjunction or the NPI pur, is admissible in a comparative iff non₂ is licensed there; the negation requirement is the item's Fragment entry.

Equations

• NapoliNespor1976.NegationAdmissible m e = (m.Licensed ∧ PolarityItem.LicensingContext.negation ∈ e.licensingContexts)

def NapoliNespor1976.AffattoAdmissible (m : Move) : Prop

Affatto 'at all' needs its clause negated and requires precise knowledge of the listener's belief, which a belief only inferred from the listener's discourse does not give.

Equations

• NapoliNespor1976.AffattoAdmissible m = (NapoliNespor1976.NegationAdmissible m Italian.PolarityItems.affatto ∧ m.priorBelief ≠ NapoliNespor1976.PriorBelief.inferred)

theorem NapoliNespor1976.neanche_admissible : NegationAdmissible chessContext.move Italian.PolarityItems.neanche

Neanche-conjunction is admissible in the chess dialogue.

theorem NapoliNespor1976.pur_admissible {m : Move} (h : m.Licensed) : NegationAdmissible m Italian.PolarityItems.pur

Pur is admissible wherever non₂ is licensed.

theorem NapoliNespor1976.negationAdmissible_affatto {m : Move} (h : m.Licensed) : NegationAdmissible m Italian.PolarityItems.affatto

Affatto meets the negation requirement wherever non₂ is licensed, like pur.

theorem NapoliNespor1976.affatto_blocked (m : Move) : ¬AffattoAdmissible m

Affatto is inadmissible in every non₂-comparative: non₂ requires inferred and imprecise knowledge of the listener's belief, affatto precise knowledge.