Greco (2020): On the Syntax of Surprise Negation Sentences

This file formalizes Greco's analysis of Italian surprise negation sentences (Snegs) such as E non mi è scesa dal treno Maria?! 'Mary got off the train!', affirmative sentences carrying the negative marker non. The paper places Snegs in the strong class of expletive negation, the class licensing no polarity-sensitive element (Tables 1 and 2), separates them from negative rhetorical questions and expletive negative exclamatives by wh-elements, answerhood, dopo tutto, and factive embedding (sneg_not_nrq, sneg_not_ene), and derives their properties from one representation, (59) and (65): non is a head externally merged in the CP field after the CP-phase head has closed the vP phase, selecting the focus phrase whose specifier hosts the whole TP. Merged after the phase head, non cannot bind into the vP (Closed, the Phase Impenetrability Condition read off the spine (68)), which excludes n-words, NPIs, not-also conjunctions, NEG-raising, and Aux-to-Comp while admitting positive polarity items; the occupied focus position excludes further foci, wh-elements, quantifier raising, and answers to entity questions while licensing expletive e and answers to propositional questions; and whole-TP focalization, impossible in embedded clauses and in structures without TP, makes Snegs a root phenomenon. rows_sneg checks every judgment of the pool against the requirement its construction places on the structure, and phase_heads is the paper's (68): Fin°, Top°, or Foc° as CP-phase head gives the derivation, Force° does not.

Implementation notes

The spine (68) is a planar syntactic object over tokens, and Closed p reads the Phase Impenetrability Condition off it: non is outside the interior of the phase headed by p exactly when p merged first. The representation (73) carries the raised TP in the specifier of the focus phrase, and the focus-side requirements read Sisters off it. The requirement a construction places on the clause is a feature of its example row, so the predictions are stated once over Requirement and checked against the rows; the section 3 rows carry the diagnostic they test instead, and the embedded-focus rows (83) to (85) the focalized constituent.

References

• [Gre20]
• [Riz97]
• [Cho01]

Polarity-sensitive elements

inductive Greco2020.PolarityClass : Type

The four classes of polarity-sensitive element that Table 1 tests in each EN environment: weak NPIs (alzare un dito 'lift a finger'), strong NPIs (affatto 'at all'), not-also conjunctions (e neanche), and n-words (nessuno 'nobody').

• weakNPI : PolarityClass
• strongNPI : PolarityClass
• notAlsoConj : PolarityClass
• nWord : PolarityClass

@[instance_reducible]

instance Greco2020.instDecidableEqPolarityClass : DecidableEq PolarityClass

Equations

• Greco2020.instDecidableEqPolarityClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Greco2020.instReprPolarityClass : Repr PolarityClass

Equations

• Greco2020.instReprPolarityClass = { reprPrec := Greco2020.instReprPolarityClass.repr }

def Greco2020.instReprPolarityClass.repr : PolarityClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Greco2020.instFintypePolarityClass : Fintype PolarityClass

Equations

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

inductive Greco2020.ENStrength : Type

The two classes of EN environment. Weak EN keeps some of the licensing of standard negation, and strong EN keeps none.

• weak : ENStrength
• strong : ENStrength

@[instance_reducible]

instance Greco2020.instDecidableEqENStrength : DecidableEq ENStrength

Equations

• Greco2020.instDecidableEqENStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Greco2020.instReprENStrength : Repr ENStrength

Equations

• Greco2020.instReprENStrength = { reprPrec := Greco2020.instReprENStrength.repr }

def Greco2020.instReprENStrength.repr : ENStrength → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Greco2020.instReprENStrength.repr Greco2020.ENStrength.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Greco2020.ENStrength.weak")).group prec✝

def Greco2020.ENStrength.licensed : ENStrength → Finset PolarityClass

The polarity classes an EN environment of each strength licenses (Table 1, whose rows are uniform within each class): weak EN licenses weak NPIs and n-words.

Equations

• Greco2020.ENStrength.weak.licensed = {Greco2020.PolarityClass.weakNPI, Greco2020.PolarityClass.nWord}
• Greco2020.ENStrength.strong.licensed = ∅

Tables 1 and 2: the Italian expletive negation environments

inductive Greco2020.ENEnvironment : Type

The eleven Italian EN environments of [Gre20] Tables 1 and 2.

• untilClauses : ENEnvironment
• whoKnowsClauses : ENEnvironment
• unlessClauses : ENEnvironment
• indirectInterrogatives : ENEnvironment
• comparativeClauses : ENEnvironment
• negativeExclamatives : ENEnvironment
• rhetoricalQuestions : ENEnvironment
• notThatClauses : ENEnvironment
• ratherThanClauses : ENEnvironment
• beforeClauses : ENEnvironment
• snegs : ENEnvironment

@[instance_reducible]

instance Greco2020.instDecidableEqENEnvironment : DecidableEq ENEnvironment

Equations

• Greco2020.instDecidableEqENEnvironment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Greco2020.instReprENEnvironment.repr : ENEnvironment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Greco2020.instReprENEnvironment : Repr ENEnvironment

Equations

• Greco2020.instReprENEnvironment = { reprPrec := Greco2020.instReprENEnvironment.repr }

def Greco2020.ENEnvironment.strength : ENEnvironment → ENStrength

The weak or strong class of each environment ([Gre20] Tables 1 and 2).

Equations

• Greco2020.ENEnvironment.untilClauses.strength = Greco2020.ENStrength.weak
• Greco2020.ENEnvironment.whoKnowsClauses.strength = Greco2020.ENStrength.weak
• Greco2020.ENEnvironment.unlessClauses.strength = Greco2020.ENStrength.weak
• Greco2020.ENEnvironment.indirectInterrogatives.strength = Greco2020.ENStrength.weak
• Greco2020.ENEnvironment.comparativeClauses.strength = Greco2020.ENStrength.weak
• Greco2020.ENEnvironment.negativeExclamatives.strength = Greco2020.ENStrength.strong
• Greco2020.ENEnvironment.rhetoricalQuestions.strength = Greco2020.ENStrength.strong
• Greco2020.ENEnvironment.notThatClauses.strength = Greco2020.ENStrength.strong
• Greco2020.ENEnvironment.ratherThanClauses.strength = Greco2020.ENStrength.strong
• Greco2020.ENEnvironment.beforeClauses.strength = Greco2020.ENStrength.strong
• Greco2020.ENEnvironment.snegs.strength = Greco2020.ENStrength.strong

The judged sentences

inductive Greco2020.Construction : Type

The construction a row instantiates.

• sneg : Construction
• nrq : Construction

  A negative rhetorical question, section 3.1.

• ene : Construction

  An expletive negative exclamative, section 3.2.

• embeddedFocus : Construction

  Focalization inside an embedded clause, (83) to (85).

@[instance_reducible]

instance Greco2020.instDecidableEqConstruction : DecidableEq Construction

Equations

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

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

Equations

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

@[instance_reducible]

instance Greco2020.instReprConstruction : Repr Construction

Equations

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

inductive Greco2020.Requirement : Type

What the construction tested in a row needs of the clause it occurs in.

• negScope : Requirement

  Negation binding into the v*P, as negative-scope elements, NEG-raising and Aux-to-Comp need.

• noNegScope : Requirement

  The v*P outside the negation's scope, as positive polarity items need.

• freeFocP : Requirement

  An empty focus position, as foci, wh-elements, quantifier raising and entity answers need.

• activeFocP : Requirement

  A filled focus position, as expletive e and answers to propositional questions need.

• embedded : Requirement

  Embedding, which admits the focalization of a part of TP only, (83) to (85).

• noTP : Requirement

  A structure without TP, as in past participle clauses and Absolute Constructions.

• phrasalNegator : Requirement

  A negator with maximal-projection status, no.

• any : Requirement

  Nothing, as for topics of every kind, presuppositional mica and either subject position.

@[instance_reducible]

instance Greco2020.instDecidableEqRequirement : DecidableEq Requirement

Equations

• Greco2020.instDecidableEqRequirement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Greco2020.instReprRequirement.repr : Requirement → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Greco2020.instReprRequirement.repr Greco2020.Requirement.any prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Greco2020.Requirement.any")).group prec✝

@[instance_reducible]

instance Greco2020.instReprRequirement : Repr Requirement

Equations

• Greco2020.instReprRequirement = { reprPrec := Greco2020.instReprRequirement.repr }

@[instance_reducible]

instance Greco2020.instFintypeRequirement : Fintype Requirement

Equations

• Greco2020.instFintypeRequirement = { elems := { val := ↑Greco2020.Requirement.enumList, nodup := Greco2020.Requirement.enumList_nodup }, complete := Greco2020.instFintypeRequirement._proof_1 }

inductive Greco2020.Diagnostic : Type

The diagnostics of section 3 separating Snegs from the other strong EN clauses.

• wh : Diagnostic
• answerhood : Diagnostic
• dopoTutto : Diagnostic
• factiveEmbedding : Diagnostic

@[instance_reducible]

instance Greco2020.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

• Greco2020.instDecidableEqDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Greco2020.instReprDiagnostic : Repr Diagnostic

Equations

• Greco2020.instReprDiagnostic = { reprPrec := Greco2020.instReprDiagnostic.repr }

def Greco2020.instReprDiagnostic.repr : Diagnostic → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Greco2020.instReprDiagnostic.repr Greco2020.Diagnostic.wh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Greco2020.Diagnostic.wh")).group prec✝

def Greco2020.testedJudgment (ex : Datum) : Judgment

A row tests the judgment of the reading it names under reading, as (72b) does, being acceptable on its affirmative reading and testing the negative one, and otherwise the judgment of the sentence.

Equations

• Greco2020.testedJudgment ex = ((ex.feature? "reading").bind fun (x : String) => List.lookup x ex.readings).getD ex.judgment

structure Greco2020.Row : Type

A judged sentence, or reading, with the features the analysis reads off it.

• construction : Construction
• requirement : Option Requirement
• polarity : Option PolarityClass
• diagnostic : Option Diagnostic
• focus : Option Minimalist.Cat

  The focalized constituent of an embedded-focus row.

• judgment : Judgment

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

Equations

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

@[instance_reducible]

instance Greco2020.instDecidableEqRow : DecidableEq Row

Equations

• Greco2020.instDecidableEqRow = Greco2020.instDecidableEqRow.decEq

@[instance_reducible]

instance Greco2020.instReprRow : Repr Row

Equations

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

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

Equations

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

def Greco2020.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Greco2020.rows : List Row

The judged sentences of sections 2 to 4.

Equations

• Greco2020.rows = List.filterMap Greco2020.Row.ofDatum Greco2020.Examples.all

Section 3: Snegs are neither rhetorical questions nor exclamatives

def Greco2020.Differ (c₁ c₂ : Construction) (d : Diagnostic) : Prop

Constructions c₁ and c₂ receive opposite judgments on diagnostic d in the pool.

Equations

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

@[instance_reducible]

instance Greco2020.instDecidableDiffer (c₁ c₂ : Construction) (d : Diagnostic) : Decidable (Differ c₁ c₂ d)

Equations

• Greco2020.instDecidableDiffer c₁ c₂ d = id inferInstance

theorem Greco2020.sneg_not_nrq : Differ Construction.sneg Construction.nrq Diagnostic.wh ∧ Differ Construction.sneg Construction.nrq Diagnostic.answerhood ∧ Differ Construction.sneg Construction.nrq Diagnostic.dopoTutto

Section 3.1: unlike negative rhetorical questions, Snegs reject wh-elements and dopo tutto and serve as answers, (31), (34), (35).

theorem Greco2020.sneg_not_ene : Differ Construction.sneg Construction.ene Diagnostic.wh ∧ Differ Construction.sneg Construction.ene Diagnostic.answerhood ∧ Differ Construction.sneg Construction.ene Diagnostic.factiveEmbedding

Section 3.2: unlike expletive negative exclamatives, Snegs reject wh-elements and factive embedding and serve as answers, (40) to (42).

The representation: (59), (65), (68), and (73)

def Greco2020.non : Minimalist.LexicalItem.Token

The negative marker non of (59), a head selecting the focus phrase.

Equations

• Greco2020.non = { item := Minimalist.LexicalItem.of Minimalist.Cat.Neg [Minimalist.Cat.Foc] "non", id := 0 }

def Greco2020.force : Minimalist.LexicalItem.Token

Force°, the highest head of the CP field in (68).

Equations

• Greco2020.force = { item := Minimalist.LexicalItem.of Minimalist.Cat.Force [Minimalist.Cat.Neg], id := 1 }

def Greco2020.foc : Minimalist.LexicalItem.Token

Foc°, whose specifier hosts the raised TP.

Equations

• Greco2020.foc = { item := Minimalist.LexicalItem.of Minimalist.Cat.Foc [Minimalist.Cat.Top], id := 2 }

def Greco2020.top : Minimalist.LexicalItem.Token

The lower Top° of (68), between Foc° and Fin°.

Equations

• Greco2020.top = { item := Minimalist.LexicalItem.of Minimalist.Cat.Top [Minimalist.Cat.Fin], id := 3 }

def Greco2020.fin : Minimalist.LexicalItem.Token

Fin°, the lowest head of the CP field.

Equations

• Greco2020.fin = { item := Minimalist.LexicalItem.of Minimalist.Cat.Fin [Minimalist.Cat.T], id := 4 }

def Greco2020.t : Minimalist.LexicalItem.Token

T°.

Equations

• Greco2020.t = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [Minimalist.Cat.v], id := 5 }

def Greco2020.v : Minimalist.LexicalItem.Token

v*, the phase head of the verbal domain.

Equations

• Greco2020.v = { item := Minimalist.LexicalItem.of Minimalist.Cat.v [Minimalist.Cat.D], id := 6 }

def Greco2020.arg : Minimalist.LexicalItem.Token

An argument inside the v*P, the site of a negative-scope element.

Equations

• Greco2020.arg = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 7 }

def Greco2020.vP : Minimalist.PlanarSyntacticObject

The v*P.

Equations

• Greco2020.vP = ↑Greco2020.v * ↑Greco2020.arg

def Greco2020.spine : Minimalist.PlanarSyntacticObject

The spine (68) with non in place: Force° over Neg° over Foc° over Top° over Fin° over TP.

Equations

• Greco2020.spine = ↑Greco2020.force * (↑Greco2020.non * (↑Greco2020.foc * (↑Greco2020.top * (↑Greco2020.fin * (↑Greco2020.t * Greco2020.vP)))))

def Greco2020.Closed (p : Minimalist.LexicalItem.Token) : Prop

The vP is closed to non under the CP-phase head p: the vP lies in the interior of the phase p heads and non does not, so p merged first and transferred the v*P before non could bind into it ([Cho01]'s Phase Impenetrability Condition).

Equations

• Greco2020.Closed p = ((↑Greco2020.spine).WithinComplement p ↑Greco2020.vP ∧ ¬(↑Greco2020.spine).WithinComplement p ↑Greco2020.non)

@[instance_reducible]

instance Greco2020.instDecidableClosed (p : Minimalist.LexicalItem.Token) : Decidable (Closed p)

Equations

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

theorem Greco2020.phase_heads : Closed fin ∧ Closed top ∧ Closed foc ∧ ¬Closed force

(68): with Fin°, Top°, or Foc° as CP-phase head the v*P is closed when non merges; with Force°, merged after non, it is not.

def Greco2020.tp : Minimalist.PlanarSyntacticObject

The raised TP of (73).

Equations

• Greco2020.tp = ↑Greco2020.t * Greco2020.vP

def Greco2020.focBar : Minimalist.PlanarSyntacticObject

Foc° over the trace of the raised TP.

Equations

• Greco2020.focBar = ↑Greco2020.foc * Minimalist.PlanarSyntacticObject.traceOf Greco2020.t

def Greco2020.sneg : Minimalist.PlanarSyntacticObject

The representation (73): non selects the focus phrase whose specifier hosts the TP.

Equations

• Greco2020.sneg = ↑Greco2020.non * (Greco2020.tp * Greco2020.focBar)

def Greco2020.FocOccupied : Prop

Some constituent occupies the specifier of the unique focus phrase ([Riz97]).

Equations

• Greco2020.FocOccupied = ∃ x ∈ (↑Greco2020.sneg).accessibleTerms, (↑Greco2020.sneg).Sisters x ↑Greco2020.focBar

@[instance_reducible]

instance Greco2020.instDecidableFocOccupied : Decidable FocOccupied

Equations

• Greco2020.instDecidableFocOccupied = Multiset.decidableExistsMultiset

def Greco2020.WholeTPFocused : Prop

The whole TP is focalized.

Equations

• Greco2020.WholeTPFocused = (↑Greco2020.sneg).Sisters ↑Greco2020.tp ↑Greco2020.focBar

@[instance_reducible]

instance Greco2020.instDecidableWholeTPFocused : Decidable WholeTPFocused

Equations

• Greco2020.instDecidableWholeTPFocused = Greco2020.instDecidableWholeTPFocused._aux_1

def Greco2020.Allows (p : Minimalist.LexicalItem.Token) : Requirement → Prop

Whether the representation meets a requirement, under CP-phase head p. A phrasal negator is excluded because the negator of (59) selects the focus phrase, which only a head does.

Equations

• Greco2020.Allows p Greco2020.Requirement.negScope = ¬Greco2020.Closed p
• Greco2020.Allows p Greco2020.Requirement.noNegScope = Greco2020.Closed p
• Greco2020.Allows p Greco2020.Requirement.freeFocP = ¬Greco2020.FocOccupied
• Greco2020.Allows p Greco2020.Requirement.activeFocP = Greco2020.FocOccupied
• Greco2020.Allows p Greco2020.Requirement.embedded = ¬Greco2020.WholeTPFocused
• Greco2020.Allows p Greco2020.Requirement.noTP = ¬Greco2020.WholeTPFocused
• Greco2020.Allows p Greco2020.Requirement.phrasalNegator = (Greco2020.non.item.sel = [])
• Greco2020.Allows p Greco2020.Requirement.any = True

@[instance_reducible]

instance Greco2020.instDecidableAllows (p : Minimalist.LexicalItem.Token) (q : Requirement) : Decidable (Allows p q)

Equations

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

theorem Greco2020.allows_of_closed {p p' : Minimalist.LexicalItem.Token} (hp : Closed p) (hp' : Closed p') (q : Requirement) : Allows p q ↔ Allows p' q

The predictions depend on the phase head only through Closed.

theorem Greco2020.rows_sneg {p : Minimalist.LexicalItem.Token} (hp : Closed p) (r : Row) : r ∈ rows → r.construction = Construction.sneg → ∀ (q : Requirement), r.requirement = some q → (r.judgment = Judgment.acceptable ↔ Allows p q)

Sections 2 and 4: under any admissible CP-phase head, a Sneg row is acceptable exactly when the representation meets the requirement of the construction it tests.

theorem Greco2020.embedded_focus (r : Row) : r ∈ rows → r.construction = Construction.embeddedFocus → (r.judgment = Judgment.acceptable ↔ r.focus ≠ some Minimalist.Cat.T)

Section 4.2.5's premise, (83) to (85): an embedded clause admits the focalization of a constituent of TP, never of the whole TP.

theorem Greco2020.table2_snegs {p : Minimalist.LexicalItem.Token} (hp : Closed p) (c : PolarityClass) : c ∉ ENEnvironment.snegs.strength.licensed ∧ ¬Allows p Requirement.negScope ∧ ∃ r ∈ rows, r.polarity = some c ∧ r.requirement = some Requirement.negScope ∧ r.judgment = Judgment.ungrammatical

Table 2's Sneg row from the derivation: the strong class licenses no polarity class, the closed v*P excludes negative-scope elements, and (9a) to (9d) witness the rejection of each class.