Documentation

Linglib.Phenomena.Negation.Studies.Greco2020

Phase-Based Analysis of Surprise Negation #

@cite{greco-2020} @cite{chomsky-2001}

Greco, M. (2020). On the syntax of surprise negation sentences: A case study on expletive negation. NLLT 38(3), 775–825.

Overview #

Surprise negation (Sneg) arises when a negative morpheme merges in the CP layer rather than in the standard TP-internal NegP position. Greco's analysis rests on four factors:

A negative morpheme α exists in the language
α is a syntactic head (X°), not a phrase (XP)
α merges in the CP phase after vP-phase exhaustion (Transfer)
TP is focused (moves to Spec-FocP)

The head requirement (2) explains why Italian (non, X°) has Sneg but Spanish (no, XP) does not: only heads can merge directly into the functional spine without projecting their own phrase. The phase-based account (3) explains why Sneg negation is non-truth-conditional: by the time the neg head merges, the vP complement has been transferred to LF, so the negation cannot scope into the propositional content.

Connections #

Phenomena.Negation.Studies.Rett2026.ENType — high vs low EN
Phenomena.Negation.Typology.NegationProfile.negIsHead — head status
Minimalism.fValue — f-value classification (Extended Projection)
Minimalism.isPhaseHead — phase head identification

inductive Phenomena.Negation.Studies.Greco2020.NegMergePosition :

Where a negation head is merged in the extended projection. Standard NegP is in the inflectional domain (F2, between v and C). In surprise negation, non merges in the CP layer (F3+, between Fin and Foc).

tp : NegMergePosition
cp : NegMergePosition

Instances For

instance Phenomena.Negation.Studies.Greco2020.instDecidableEqNegMergePosition :

DecidableEq NegMergePosition

Equations

Phenomena.Negation.Studies.Greco2020.instDecidableEqNegMergePosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Negation.Studies.Greco2020.instBEqNegMergePosition :

BEq NegMergePosition

Equations

Phenomena.Negation.Studies.Greco2020.instBEqNegMergePosition = { beq := Phenomena.Negation.Studies.Greco2020.instBEqNegMergePosition.beq }

def Phenomena.Negation.Studies.Greco2020.instBEqNegMergePosition.beq :

NegMergePosition → NegMergePosition → Bool

Equations

Phenomena.Negation.Studies.Greco2020.instBEqNegMergePosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Negation.Studies.Greco2020.instReprNegMergePosition.repr :

NegMergePosition → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Negation.Studies.Greco2020.instReprNegMergePosition :

Repr NegMergePosition

Equations

Phenomena.Negation.Studies.Greco2020.instReprNegMergePosition = { reprPrec := Phenomena.Negation.Studies.Greco2020.instReprNegMergePosition.repr }

def Phenomena.Negation.Studies.Greco2020.isCPArea (c : Minimalism.Cat) :

A category is in the CP area iff its f-value is at or above Fin (F3). @cite{rizzi-1997}: Fin is the boundary between the inflectional domain and the left periphery.

Equations

Phenomena.Negation.Studies.Greco2020.isCPArea c = decide (Minimalism.fValue c ≥ Minimalism.fValue Minimalism.Cat.Fin)

Instances For

theorem Phenomena.Negation.Studies.Greco2020.neg_in_tp :

isCPArea Minimalism.Cat.Neg = false

Standard NegP (F2) is in TP, not CP.

theorem Phenomena.Negation.Studies.Greco2020.foc_in_cp :

isCPArea Minimalism.Cat.Foc = true

Foc (F4) is in the CP area.

theorem Phenomena.Negation.Studies.Greco2020.force_in_cp :

isCPArea Minimalism.Cat.Force = true

Force (F6) is in the CP area.

theorem Phenomena.Negation.Studies.Greco2020.fin_is_cp_boundary :

isCPArea Minimalism.Cat.Fin = true

Fin (F3) is the boundary (inclusive — it's the lowest CP head).

def Phenomena.Negation.Studies.Greco2020.NegMergePosition.scopesIntoVP :

NegMergePosition → Bool

Whether a Neg head at this merge position can scope into the vP domain. Under weak PIC: vP complement is accessible until the NEXT phase head (C) is merged. Standard NegP (F2) is merged before C, so vP is still accessible. CP-area Neg is merged during/after C-phase assembly, when vP complement has been transferred.

Equations

Instances For

def Phenomena.Negation.Studies.Greco2020.NegMergePosition.toENEffect :

NegMergePosition → Rett2026.ENType

CP-area negation is non-truth-conditional (= high EN). TP-area negation is truth-conditional (standard or low EN).

Equations

Instances For

theorem Phenomena.Negation.Studies.Greco2020.tp_neg_scopes :

NegMergePosition.tp.scopesIntoVP = true

TP-area negation scopes into vP.

theorem Phenomena.Negation.Studies.Greco2020.cp_neg_no_scope :

NegMergePosition.cp.scopesIntoVP = false

CP-area negation does NOT scope into vP.

theorem Phenomena.Negation.Studies.Greco2020.cp_is_high_en :

NegMergePosition.cp.toENEffect = Rett2026.ENType.high

CP-area negation maps to high EN.

theorem Phenomena.Negation.Studies.Greco2020.tp_is_low_en :

NegMergePosition.tp.toENEffect = Rett2026.ENType.low

TP-area negation maps to low EN.

structure Phenomena.Negation.Studies.Greco2020.SnegConditions :

@cite{greco-2020}: four necessary conditions for surprise negation. (i) a negative morpheme α, (ii) α is a syntactic head (X°), (iii) α merges in the CP-phase after vP-phase exhaustion, (iv) TP is focused (moves to Spec-FocP).

hasNegMorpheme : Bool
negIsHead : Bool
mergePosition : NegMergePosition
tpIsFocused : Bool

Instances For

instance Phenomena.Negation.Studies.Greco2020.instDecidableEqSnegConditions :

DecidableEq SnegConditions

Equations

Phenomena.Negation.Studies.Greco2020.instDecidableEqSnegConditions = Phenomena.Negation.Studies.Greco2020.instDecidableEqSnegConditions.decEq

def Phenomena.Negation.Studies.Greco2020.instDecidableEqSnegConditions.decEq (x✝ x✝¹ : SnegConditions) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Phenomena.Negation.Studies.Greco2020.instBEqSnegConditions :

BEq SnegConditions

Equations

Phenomena.Negation.Studies.Greco2020.instBEqSnegConditions = { beq := Phenomena.Negation.Studies.Greco2020.instBEqSnegConditions.beq }

def Phenomena.Negation.Studies.Greco2020.instBEqSnegConditions.beq :

SnegConditions → SnegConditions → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Negation.Studies.Greco2020.instBEqSnegConditions.beq x✝¹ x✝ = false

Instances For

instance Phenomena.Negation.Studies.Greco2020.instReprSnegConditions :

Repr SnegConditions

Equations

Phenomena.Negation.Studies.Greco2020.instReprSnegConditions = { reprPrec := Phenomena.Negation.Studies.Greco2020.instReprSnegConditions.repr }

def Phenomena.Negation.Studies.Greco2020.instReprSnegConditions.repr :

SnegConditions → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Negation.Studies.Greco2020.SnegConditions.yieldsSnegs (c : SnegConditions) :

A set of conditions yields surprise negation iff all four are satisfied.

Equations

c.yieldsSnegs = (c.hasNegMorpheme && c.negIsHead && c.mergePosition == Phenomena.Negation.Studies.Greco2020.NegMergePosition.cp && c.tpIsFocused)

Instances For

def Phenomena.Negation.Studies.Greco2020.italianSnegConditions :

Italian satisfies all four Sneg conditions.

Equations

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

Instances For

theorem Phenomena.Negation.Studies.Greco2020.italian_yields_snegs :

italianSnegConditions.yieldsSnegs = true

def Phenomena.Negation.Studies.Greco2020.spanishSnegConditions :

Spanish fails condition (ii): no is XP, not X°.

Equations

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

Instances For

theorem Phenomena.Negation.Studies.Greco2020.spanish_no_snegs :

spanishSnegConditions.yieldsSnegs = false

structure Phenomena.Negation.Studies.Greco2020.SnegAttestation :

Sneg attestation datum: links a language's negation profile to whether surprise negation is attested.

language : String
attested : Bool
negIsHead : Option Bool

Instances For

instance Phenomena.Negation.Studies.Greco2020.instDecidableEqSnegAttestation :

DecidableEq SnegAttestation

Equations

Phenomena.Negation.Studies.Greco2020.instDecidableEqSnegAttestation = Phenomena.Negation.Studies.Greco2020.instDecidableEqSnegAttestation.decEq

def Phenomena.Negation.Studies.Greco2020.instDecidableEqSnegAttestation.decEq (x✝ x✝¹ : SnegAttestation) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Phenomena.Negation.Studies.Greco2020.instBEqSnegAttestation.beq :

SnegAttestation → SnegAttestation → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Negation.Studies.Greco2020.instBEqSnegAttestation.beq x✝¹ x✝ = false

Instances For

instance Phenomena.Negation.Studies.Greco2020.instBEqSnegAttestation :

BEq SnegAttestation

Equations

Phenomena.Negation.Studies.Greco2020.instBEqSnegAttestation = { beq := Phenomena.Negation.Studies.Greco2020.instBEqSnegAttestation.beq }

instance Phenomena.Negation.Studies.Greco2020.instReprSnegAttestation :

Repr SnegAttestation

Equations

Phenomena.Negation.Studies.Greco2020.instReprSnegAttestation = { reprPrec := Phenomena.Negation.Studies.Greco2020.instReprSnegAttestation.repr }

def Phenomena.Negation.Studies.Greco2020.instReprSnegAttestation.repr :

SnegAttestation → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Negation.Studies.Greco2020.italianSnegs :

SnegAttestation

Equations

Phenomena.Negation.Studies.Greco2020.italianSnegs = { language := "Italian", attested := true, negIsHead := Phenomena.Negation.Typology.italian.negIsHead }

Instances For

def Phenomena.Negation.Studies.Greco2020.spanishSnegs :

SnegAttestation

Equations

Phenomena.Negation.Studies.Greco2020.spanishSnegs = { language := "Spanish", attested := false, negIsHead := Phenomena.Negation.Typology.spanish.negIsHead }

Instances For

def Phenomena.Negation.Studies.Greco2020.brazilianPortugueseSnegs :

SnegAttestation

Equations

Phenomena.Negation.Studies.Greco2020.brazilianPortugueseSnegs = { language := "Brazilian Portuguese", attested := true, negIsHead := some true }

Instances For

def Phenomena.Negation.Studies.Greco2020.allSnegAttestations :

List SnegAttestation

Equations

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

Instances For

theorem Phenomena.Negation.Studies.Greco2020.sneg_requires_head :

(allSnegAttestations.all fun (s : SnegAttestation) => if s.attested = true then s.negIsHead == some true else true) = true

Greco's prediction: Snegs are attested only when negIsHead = true.

theorem Phenomena.Negation.Studies.Greco2020.head_predicts_snegs :

(allSnegAttestations.all fun (s : SnegAttestation) => if (s.negIsHead == some false) = true then !s.attested else true) = true

Converse: head-status neg predicts Sneg availability (in our sample).

theorem Phenomena.Negation.Studies.Greco2020.italian_snegs_from_profile :

italianSnegs.negIsHead = Typology.italian.negIsHead

The Italian Sneg attestation derives its head status from the NegationProfile, not by stipulation.

theorem Phenomena.Negation.Studies.Greco2020.spanish_snegs_from_profile :

spanishSnegs.negIsHead = Typology.spanish.negIsHead

The Spanish Sneg attestation derives its head status from the NegationProfile.

theorem Phenomena.Negation.Studies.Greco2020.cp_area_above_neg :

Minimalism.fValue Minimalism.Cat.Fin > Minimalism.fValue Minimalism.Cat.Neg

The f-value boundary: anything at F3+ (CP area) is above the inflectional domain where standard NegP resides.

theorem Phenomena.Negation.Studies.Greco2020.neg_t_same_fvalue :

Minimalism.fValue Minimalism.Cat.Neg = Minimalism.fValue Minimalism.Cat.T

NegP and T share the same f-value (both F2, inflectional domain).

theorem Phenomena.Negation.Studies.Greco2020.scope_determines_entype (pos : NegMergePosition) :

pos.scopesIntoVP = true ↔ pos.toENEffect = Rett2026.ENType.low

The merge position determines scope: TP-area neg is truth-conditional, CP-area neg is non-truth-conditional. This is consistent: CP-area maps to high EN, TP-area maps to low EN.