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:

1. A negative morpheme α exists in the language
2. α is a syntactic head (X°), not a phrase (XP)
3. α merges in the CP phase after vP-phase exhaustion (Transfer)
4. 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.

Two structural primitives

All Sneg predictions derive from exactly two structural consequences of the representation [CP ... [X° non] ... [FocP [TP ...] Foc° ...]]:

• vP transferred: neg merged in CP → PIC → no scope into vP (blocks: NPIs, N-words, NEG-raising, DE inferences, Aux-to-Comp; licenses: PPIs)
• FocP occupied: TP fills [Spec, FocP] → unique FocP exhausted (blocks: other foci, Wh-elements, entity-question answers; forces: root-only, preverbal-subject topicalization; licenses: EE)

Connections

• Core.Negation — framework-agnostic EN types (ENType, ENStrength, PolarityLicensing)
• Minimalist.NegScope — merge position, scope, classification chain (defined below)
• Fragments.Italian.ExpletiveNegation — Italian Table 1 data
• Typology.Negation.NegationProfile.negIsHead — head status
• Minimalist.fValue / isCPArea — f-value classification

Neg-Merge-Position Apparatus (relocated from Minimalism/NegScope.lean)

The NegMergePosition type and its bridges to ENType, ENStrength, and PolarityLicensing are paper-specific to @cite{greco-2020} (with @cite{rett-2026}'s high/low EN distinction and @cite{stankova-2025}'s Czech three-way coarsening). Not consumed elsewhere in the library, so they live here under namespace Minimalist.NegScope for symmetry with other Minimalist apparatus and to support qualified lookup if a future paper picks them up.

inductive Minimalist.NegScope.NegMergePosition : Type

Where a negation head is merged in the extended projection.

Standard NegP is in the inflectional domain (F2, between v and C). In expletive negation, negation may merge in the CP layer (F3+), above the inflectional domain. The merge position determines scope, truth-conditionality, and polarity licensing.

Compare Semantics.Negation.CzechNegation.NegPosition which classifies three LF positions (inner/medial/outer) for Czech negation. This type is coarser: TP subsumes both inner and medial positions.

• tp : NegMergePosition
• cp : NegMergePosition

@[implicit_reducible]

instance Minimalist.NegScope.instDecidableEqNegMergePosition : DecidableEq NegMergePosition

Equations

• Minimalist.NegScope.instDecidableEqNegMergePosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.NegScope.instReprNegMergePosition : Repr NegMergePosition

Equations

• Minimalist.NegScope.instReprNegMergePosition = { reprPrec := Minimalist.NegScope.instReprNegMergePosition.repr }

def Minimalist.NegScope.instReprNegMergePosition.repr : NegMergePosition → ℕ → Std.Format

Equations

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

def Minimalist.NegScope.NegMergePosition.scopesIntoVP : NegMergePosition → Bool

Whether a Neg head at this position can scope into the vP domain.

Under PIC: vP complement is transferred when the CP-phase head is merged. TP-area Neg (F2) is merged before the phase head, so vP is still accessible. CP-area Neg is merged during/after the CP-phase, when vP complement has been transferred.

Equations

• Minimalist.NegScope.NegMergePosition.tp.scopesIntoVP = true
• Minimalist.NegScope.NegMergePosition.cp.scopesIntoVP = false

def Minimalist.NegScope.NegMergePosition.equivBool : NegMergePosition ≃ Bool

NegMergePosition ≃ Bool: tp ↦ false, cp ↦ true. Aligned with the LinearOrder (tp < cp) and the ENType/ENStrength equivalences (low/weak ↦ false, high/strong ↦ true).

Equations

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

@[implicit_reducible]

instance Minimalist.NegScope.instFintypeNegMergePosition : Fintype NegMergePosition

Equations

• Minimalist.NegScope.instFintypeNegMergePosition = Fintype.ofEquiv Bool Minimalist.NegScope.NegMergePosition.equivBool.symm

def Minimalist.NegScope.NegMergePosition.toNat : NegMergePosition → ℕ

Numeric embedding: tp ↦ 0, cp ↦ 1 (by f-value position).

Equations

• Minimalist.NegScope.NegMergePosition.tp.toNat = 0
• Minimalist.NegScope.NegMergePosition.cp.toNat = 1

@[implicit_reducible]

instance Minimalist.NegScope.instLinearOrderNegMergePosition : LinearOrder NegMergePosition

Equations

• Minimalist.NegScope.instLinearOrderNegMergePosition = LinearOrder.lift' Minimalist.NegScope.NegMergePosition.toNat Minimalist.NegScope.instLinearOrderNegMergePosition._proof_1

def Minimalist.NegScope.NegMergePosition.toENType : NegMergePosition → Phenomena.Negation.ExpletiveNegation.ENType

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

Equations

• Minimalist.NegScope.NegMergePosition.tp.toENType = Phenomena.Negation.ExpletiveNegation.ENType.low
• Minimalist.NegScope.NegMergePosition.cp.toENType = Phenomena.Negation.ExpletiveNegation.ENType.high

def Minimalist.NegScope.NegMergePosition.toENStrength : NegMergePosition → Phenomena.Negation.ExpletiveNegation.ENStrength

Merge position determines EN strength.

Equations

• Minimalist.NegScope.NegMergePosition.tp.toENStrength = Phenomena.Negation.ExpletiveNegation.ENStrength.weak
• Minimalist.NegScope.NegMergePosition.cp.toENStrength = Phenomena.Negation.ExpletiveNegation.ENStrength.strong

def Minimalist.NegScope.NegMergePosition.polarityProfile : NegMergePosition → Phenomena.Negation.ExpletiveNegation.PolarityLicensing

Merge position determines polarity licensing profile.

CP-area negation cannot create a downward-entailing context in vP (the vP phase complement has been transferred), so it cannot license any polarity-sensitive elements. TP-area negation retains scope into vP, preserving some licensing ability (weak NPIs, N-words).

This is @cite{greco-2020}'s core theoretical claim: the weak/strong EN distinction reduces to where negation merges relative to the vP-phase boundary.

Equations

• Minimalist.NegScope.NegMergePosition.tp.polarityProfile = Phenomena.Negation.ExpletiveNegation.weakENProfile
• Minimalist.NegScope.NegMergePosition.cp.polarityProfile = Phenomena.Negation.ExpletiveNegation.strongENProfile

def Minimalist.NegScope.NegMergePosition.equivENType : NegMergePosition ≃ Phenomena.Negation.ExpletiveNegation.ENType

NegMergePosition ≃ ENType: tp ↦ low, cp ↦ high.

Equations

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

def Minimalist.NegScope.NegMergePosition.equivENStrength : NegMergePosition ≃ Phenomena.Negation.ExpletiveNegation.ENStrength

NegMergePosition ≃ ENStrength: tp ↦ weak, cp ↦ strong.

Equations

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

theorem Minimalist.NegScope.equiv_factors_entype (p : NegMergePosition) : NegMergePosition.equivENType p = Phenomena.Negation.ExpletiveNegation.ENType.equivBool.invFun (NegMergePosition.equivBool p)

The Equiv chain factors through Bool: toENType p = equivBool.symm (scopesIntoVP p) pointwise.

theorem Minimalist.NegScope.equiv_factors_enstrength (p : NegMergePosition) : NegMergePosition.equivENStrength p = Phenomena.Negation.ExpletiveNegation.ENStrength.equivBool.invFun (NegMergePosition.equivBool p)

The Equiv chain factors through Bool: equivENStrength = equivBool ∘ ENStrength.equivBool⁻¹ pointwise.

theorem Minimalist.NegScope.merge_position_semantic_bridge (pos : NegMergePosition) : Semantics.Negation.scopeToENType pos.scopesIntoVP = pos.toENType

Merge position's scopesIntoVP determines EN type via the semantic chain from Defs.lean.

theorem Minimalist.NegScope.merge_position_licensing (pos : NegMergePosition) : Semantics.Negation.scopeToLicensing pos.scopesIntoVP = pos.polarityProfile

Merge position determines licensing via the full semantic chain: merge → scopesIntoVP → scopeToENType → enTypeToLicensing.

All classifications are in bijection

NegMergePosition, ENType, ENStrength, and Bool (via scopesIntoVP) are all two-element types. The bridge functions between them are bijections. Rather than proving each pairwise, we state a single theorem: all four two-valued properties agree on which merge position they classify as "active" (scope-bearing, low, weak, NPI-licensing).

theorem Minimalist.NegScope.classifications_agree (pos : NegMergePosition) : (pos.scopesIntoVP = true) = ((pos.toENType == Phenomena.Negation.ExpletiveNegation.ENType.low) = true) ∧ (pos.toENType == Phenomena.Negation.ExpletiveNegation.ENType.low) = (pos.toENStrength == Phenomena.Negation.ExpletiveNegation.ENStrength.weak) ∧ (pos.toENStrength == Phenomena.Negation.ExpletiveNegation.ENStrength.weak) = pos.polarityProfile.licenses Phenomena.Negation.ExpletiveNegation.PolarityClass.weakNPI

The classification chain: all four two-valued properties of NegMergePosition are in bijection. Scope access, EN type, EN strength, and weak-NPI licensing all partition merge positions the same way.

This means any result proved about one classification automatically constrains the others.

theorem Minimalist.NegScope.scope_determines_entype (pos : NegMergePosition) : pos.scopesIntoVP = true ↔ pos.toENType = Phenomena.Negation.ExpletiveNegation.ENType.low

Scope determines EN type (Iff form).

theorem Minimalist.NegScope.high_en_is_strong (pos : NegMergePosition) (h : pos.toENType = Phenomena.Negation.ExpletiveNegation.ENType.high) : pos.toENStrength = Phenomena.Negation.ExpletiveNegation.ENStrength.strong

High EN is strong EN.

Grounding scope in the extended projection

The TP/CP distinction in NegMergePosition is not stipulated — it corresponds to position in the extended projection relative to the CP boundary (F3 = Fin). This section connects scopesIntoVP to isCPArea and fValue, showing that scope accessibility follows from f-value ordering under PIC.

theorem Minimalist.NegScope.scope_iff_not_cp_area : NegMergePosition.tp.scopesIntoVP = !isCPArea Cat.Neg ∧ NegMergePosition.cp.scopesIntoVP = !isCPArea Cat.Foc

Scope into vP = NOT in CP area (for the canonical heads).

Standard NegP (F2) is below the CP boundary → scope into vP. FocP (F4) is above the CP boundary → no scope into vP. This grounds the two-way scope distinction in the extended projection's f-value monotonicity.

theorem Minimalist.NegScope.neg_in_tp : isCPArea Cat.Neg = false

Standard NegP (F2) is in the inflectional domain, not the CP area.

theorem Minimalist.NegScope.foc_in_cp : isCPArea Cat.Foc = true

Foc (F4) is in the CP area.

theorem Minimalist.NegScope.fin_is_cp_boundary : isCPArea Cat.Fin = true

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

theorem Minimalist.NegScope.cp_area_above_neg : fValue Cat.Fin > fValue Cat.Neg

The f-value boundary: CP area is strictly above standard NegP.

Coarsening Czech three-way negation

@cite{stankova-2025}

Czech polar questions distinguish three LF positions for negation: inner (TP), medial (ModP), and outer (PolP). The EN-relevant NegMergePosition is coarser: inner and medial are both in the inflectional domain (tp), while outer is in the CP area (cp).

This coercion shows that the two-way EN distinction is a proper abstraction over the three-way Czech distinction — any result proved for NegMergePosition applies to Czech negation positions via this mapping.

def Minimalist.NegScope.NegPosition.toNegMergePosition : Semantics.Negation.CzechNegation.NegPosition → NegMergePosition

Map Czech three-way negation positions to the coarser two-way EN merge position.

• Inner (TP, propositional ¬p): inflectional domain → tp
• Medial (ModP, scopes over □_ev): still inflectional → tp
• Outer (PolP, FALSUM): CP area → cp

Equations

• Minimalist.NegScope.NegPosition.toNegMergePosition Semantics.Negation.CzechNegation.NegPosition.inner = Minimalist.NegScope.NegMergePosition.tp
• Minimalist.NegScope.NegPosition.toNegMergePosition Semantics.Negation.CzechNegation.NegPosition.medial = Minimalist.NegScope.NegMergePosition.tp
• Minimalist.NegScope.NegPosition.toNegMergePosition Semantics.Negation.CzechNegation.NegPosition.outer = Minimalist.NegScope.NegMergePosition.cp

theorem Minimalist.NegScope.inner_is_tp : NegPosition.toNegMergePosition Semantics.Negation.CzechNegation.NegPosition.inner = NegMergePosition.tp

Inner/medial map to tp, outer maps to cp.

theorem Minimalist.NegScope.medial_is_tp : NegPosition.toNegMergePosition Semantics.Negation.CzechNegation.NegPosition.medial = NegMergePosition.tp

theorem Minimalist.NegScope.outer_is_cp : NegPosition.toNegMergePosition Semantics.Negation.CzechNegation.NegPosition.outer = NegMergePosition.cp

theorem Minimalist.NegScope.nci_licensing_matches_scope : Semantics.Negation.CzechNegation.licenses Semantics.Negation.CzechNegation.NegPosition.inner Semantics.Negation.CzechNegation.Diagnostic.nciLicensed = (NegPosition.toNegMergePosition Semantics.Negation.CzechNegation.NegPosition.inner).scopesIntoVP ∧ Semantics.Negation.CzechNegation.licenses Semantics.Negation.CzechNegation.NegPosition.outer Semantics.Negation.CzechNegation.Diagnostic.nciLicensed = (NegPosition.toNegMergePosition Semantics.Negation.CzechNegation.NegPosition.outer).scopesIntoVP

The Czech NCI licensing diagnostic aligns with vP scope: inner licenses NCIs (scopes into vP), outer does not (no vP scope).

theorem Minimalist.NegScope.toNegMergePosition_monotone : Monotone NegPosition.toNegMergePosition

The Czech three-way → two-way coarsening preserves scope ordering: inner ≤ medial ≤ outer maps to tp ≤ tp ≤ cp (monotone).

structure Greco2020.SnegConditions : Type

@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 : Minimalist.NegScope.NegMergePosition
• tpIsFocused : Bool

def Greco2020.instDecidableEqSnegConditions.decEq (x✝ x✝¹ : SnegConditions) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Greco2020.instDecidableEqSnegConditions : DecidableEq SnegConditions

Equations

• Greco2020.instDecidableEqSnegConditions = Greco2020.instDecidableEqSnegConditions.decEq

@[implicit_reducible]

instance Greco2020.instReprSnegConditions : Repr SnegConditions

Equations

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

def Greco2020.instReprSnegConditions.repr : SnegConditions → ℕ → Std.Format

Equations

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

def Greco2020.SnegConditions.yieldsSnegs (c : SnegConditions) : Bool

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

Equations

• c.yieldsSnegs = (c.hasNegMorpheme && c.negIsHead && c.mergePosition == Minimalist.NegScope.NegMergePosition.cp && c.tpIsFocused)

def Greco2020.italianSnegConditions : SnegConditions

Italian satisfies all four Sneg conditions.

Equations

• Greco2020.italianSnegConditions = { hasNegMorpheme := true, negIsHead := true, mergePosition := Minimalist.NegScope.NegMergePosition.cp, tpIsFocused := true }

theorem Greco2020.italian_yields_snegs : italianSnegConditions.yieldsSnegs = true

def Greco2020.spanishSnegConditions : SnegConditions

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

Equations

• Greco2020.spanishSnegConditions = { hasNegMorpheme := true, negIsHead := false, mergePosition := Minimalist.NegScope.NegMergePosition.cp, tpIsFocused := true }

theorem Greco2020.spanish_no_snegs : spanishSnegConditions.yieldsSnegs = false

structure Greco2020.SnegAttestation : Type

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

• language : String
• attested : Bool
• negIsHead : Option Bool

@[implicit_reducible]

instance Greco2020.instDecidableEqSnegAttestation : DecidableEq SnegAttestation

Equations

• Greco2020.instDecidableEqSnegAttestation = Greco2020.instDecidableEqSnegAttestation.decEq

def Greco2020.instDecidableEqSnegAttestation.decEq (x✝ x✝¹ : SnegAttestation) : Decidable (x✝ = x✝¹)

Equations

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

def Greco2020.instReprSnegAttestation.repr : SnegAttestation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Greco2020.instReprSnegAttestation : Repr SnegAttestation

Equations

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

def Greco2020.italianSnegs : SnegAttestation

Equations

• Greco2020.italianSnegs = { language := "Italian", attested := true, negIsHead := Greco2020.italian✝.negIsHead }

def Greco2020.spanishSnegs : SnegAttestation

Equations

• Greco2020.spanishSnegs = { language := "Spanish", attested := false, negIsHead := Greco2020.spanish✝.negIsHead }

def Greco2020.brazilianPortugueseSnegs : SnegAttestation

Equations

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

def Greco2020.allSnegAttestations : List SnegAttestation

Equations

• Greco2020.allSnegAttestations = [Greco2020.italianSnegs, Greco2020.spanishSnegs, Greco2020.brazilianPortugueseSnegs]

theorem 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 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 Greco2020.italian_snegs_from_profile : italianSnegs.negIsHead = Greco2020.italian✝.negIsHead

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

theorem Greco2020.spanish_snegs_from_profile : spanishSnegs.negIsHead = Greco2020.spanish✝.negIsHead

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

theorem Greco2020.neg_t_same_fvalue : Minimalist.fValue Minimalist.Cat.Neg = Minimalist.fValue Minimalist.Cat.T

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

Derived predictions from [CP ... [X° non] ... [FocP [TP ...] Foc° ...]]

@cite{greco-2020} §4.2 derives 11 properties from a single structural representation. Every prediction reduces to one of two structural primitives:

• vpTransferred: neg merged in CP → vP complement transferred by PIC
• focPOccupied: TP fills [Spec, FocP] → FocP projection exhausted

These are the only two structural consequences. Each of Greco's predictions is a one-line derivation from one primitive.

structure Greco2020.SnegRepresentation : Type

The structural representation of a Sneg (@cite{greco-2020} (59)/(106)): the negative head merges in the CP layer, and TP occupies [Spec, FocP].

• negPos : Minimalist.NegScope.NegMergePosition

  The negative head merges in the CP area (F3+).

• negInCP : self.negPos = Minimalist.NegScope.NegMergePosition.cp
• tpFocused : Bool

  TP moves to [Spec, FocP]: the whole predicate is focused.

• tpFocused_eq : self.tpFocused = true

def Greco2020.SnegRepresentation.vpTransferred (s : SnegRepresentation) : Bool

Primitive A: vP complement has been transferred by PIC. Neg merged in CP → past the phase boundary → vP shipped to LF. This blocks all propositional-scope interactions.

Equations

• s.vpTransferred = !s.negPos.scopesIntoVP

def Greco2020.SnegRepresentation.focPOccupied (s : SnegRepresentation) : Bool

Primitive B: FocP projection is occupied by TP. The unique Italian FocP (@cite{rizzi-1997}) is exhausted, blocking any other element that targets [Spec, FocP].

Equations

• s.focPOccupied = s.tpFocused

theorem Greco2020.vp_transferred (s : SnegRepresentation) : s.vpTransferred = true

theorem Greco2020.focp_occupied (s : SnegRepresentation) : s.focPOccupied = true

Predictions that follow from the vP complement being transferred. In each case, the blocked operation requires negation to scope into the propositional content — impossible when vP is gone.

def Greco2020.SnegRepresentation.allowsNegRaising (s : SnegRepresentation) : Bool

Prediction 6 (@cite{greco-2020} §4.2.3): No NEG-raising. NEG-raising requires neg in TP scope domain.

Equations

• s.allowsNegRaising = !s.vpTransferred

def Greco2020.SnegRepresentation.allowsAuxToComp (s : SnegRepresentation) : Bool

Prediction 8 (@cite{greco-2020} §4.2.5, (64)): No Aux-to-Comp. Aux-to-Comp requires neg to originate in TP.

Equations

• s.allowsAuxToComp = !s.vpTransferred

def Greco2020.SnegRepresentation.isDownwardEntailing (s : SnegRepresentation) : Bool

§2.3 (25): Sneg negation is not downward entailing. DE requires neg to scope over the predicate.

Equations

• s.isDownwardEntailing = !s.vpTransferred

theorem Greco2020.snegs_block_neg_raising (s : SnegRepresentation) : s.allowsNegRaising = false

theorem Greco2020.snegs_block_aux_to_comp (s : SnegRepresentation) : s.allowsAuxToComp = false

theorem Greco2020.sneg_not_downward_entailing (s : SnegRepresentation) : s.isDownwardEntailing = false

Predictions that follow from TP filling [Spec, FocP]. In each case, the blocked operation requires access to FocP, which is already occupied.

def Greco2020.SnegRepresentation.allowsFocus (s : SnegRepresentation) : Bool

Prediction 2 (@cite{greco-2020} §4.2.4): Snegs reject foci. FocP is already occupied by TP.

Equations

• s.allowsFocus = !s.focPOccupied

def Greco2020.SnegRepresentation.allowsWh (s : SnegRepresentation) : Bool

Prediction 3 (@cite{greco-2020} §4.2.4): Snegs reject Wh. Wh-phrases target [Spec, FocP], same as TP.

Equations

• s.allowsWh = !s.focPOccupied

def Greco2020.SnegRepresentation.requiresRoot (s : SnegRepresentation) : Bool

Prediction 1 (@cite{greco-2020} §4.2.5): Snegs are root-only. Subordinate clauses block whole-TP focalization.

Equations

• s.requiresRoot = s.focPOccupied

def Greco2020.SnegRepresentation.licensesEE (s : SnegRepresentation) : Bool

Prediction 7 (@cite{greco-2020} §4.2.7): Snegs license EE. EE is parasitic on an active FocP (@cite{poletto-2005}).

Equations

• s.licensesEE = s.focPOccupied

def Greco2020.SnegRepresentation.allowsTopics (_s : SnegRepresentation) : Bool

Topics are freely allowed — TopP is recursive and independent of FocP. This is NOT derived from either primitive.

Equations

• _s.allowsTopics = true

theorem Greco2020.snegs_reject_focus (s : SnegRepresentation) : s.allowsFocus = false

theorem Greco2020.snegs_reject_wh (s : SnegRepresentation) : s.allowsWh = false

theorem Greco2020.snegs_require_root (s : SnegRepresentation) : s.requiresRoot = true

theorem Greco2020.snegs_license_ee (s : SnegRepresentation) : s.licensesEE = true

theorem Greco2020.snegs_allow_topics (s : SnegRepresentation) : s.allowsTopics = true

inductive Greco2020.QuestionType : Type

Prediction 4 (@cite{greco-2020} §4.2.4, (26)–(27)): Snegs answer propositional questions but NOT entity questions.

TP-focalization means the WHOLE predicate is new-information focus. Propositional questions ask about the entire proposition — compatible. Entity questions require sub-TP focus — incompatible.

• propositional : QuestionType
• entity : QuestionType

@[implicit_reducible]

instance Greco2020.instDecidableEqQuestionType : DecidableEq QuestionType

Equations

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

@[implicit_reducible]

instance Greco2020.instReprQuestionType : Repr QuestionType

Equations

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

def Greco2020.instReprQuestionType.repr : QuestionType → ℕ → Std.Format

Equations

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

def Greco2020.SnegRepresentation.answersQuestion (s : SnegRepresentation) : QuestionType → Bool

Equations

• s.answersQuestion Greco2020.QuestionType.propositional = s.focPOccupied
• s.answersQuestion Greco2020.QuestionType.entity = !s.focPOccupied

theorem Greco2020.snegs_answer_propositional (s : SnegRepresentation) : s.answersQuestion QuestionType.propositional = true

theorem Greco2020.snegs_reject_entity (s : SnegRepresentation) : s.answersQuestion QuestionType.entity = false

inductive Greco2020.SubjectPosition : Type

Prediction 5 (@cite{greco-2020} §4.2.6): Preverbal subjects are topicalized. FocP full → subject forced to TopP.

• preverbal : SubjectPosition
• postverbal : SubjectPosition

@[implicit_reducible]

instance Greco2020.instDecidableEqSubjectPosition : DecidableEq SubjectPosition

Equations

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

def Greco2020.instReprSubjectPosition.repr : SubjectPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Greco2020.instReprSubjectPosition : Repr SubjectPosition

Equations

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

def Greco2020.SnegRepresentation.subjectIsTopicalized (s : SnegRepresentation) : SubjectPosition → Bool

Equations

• s.subjectIsTopicalized Greco2020.SubjectPosition.preverbal = s.focPOccupied
• s.subjectIsTopicalized Greco2020.SubjectPosition.postverbal = false

theorem Greco2020.preverbal_subject_topicalized (s : SnegRepresentation) : s.subjectIsTopicalized SubjectPosition.preverbal = true

PPI licensing (@cite{greco-2020} §2.3 (24), @cite{giannakidou-2011})

Snegs CAN host PPIs like già ("already"), despite containing a negative marker. Since vP has been transferred, the PPI inside vP is outside negation's scope — it has already "escaped" by PIC.

theorem Greco2020.ppi_survives_in_sneg (s : SnegRepresentation) : s.vpTransferred = true

PPIs survive because vP has been transferred.

Ethical Dative interaction (@cite{greco-2020} §2.2 (13))

When Ethical Dative (mi/ti) co-occurs with non, only the Sneg reading is available — standard negation is ruled out. ED is associated with the CP layer (discourse-level emotional participation), which is exactly where Sneg non merges.

structure Greco2020.EDDisambiguation : Type

ED disambiguates: presence of ED forces the Sneg reading.

• hasEthicalDative : Bool
• negInterpretation : Minimalist.NegScope.NegMergePosition
• ed_forces_sneg : self.hasEthicalDative = true → self.negInterpretation = Minimalist.NegScope.NegMergePosition.cp

def Greco2020.snegWithED : EDDisambiguation

Equations

• Greco2020.snegWithED = { hasEthicalDative := true, negInterpretation := Minimalist.NegScope.NegMergePosition.cp, ed_forces_sneg := ⋯ }

Parametric variation (@cite{greco-2020} §4.2.9)

Snegs require the conspiracy of four factors. Blocking any one prevents Snegs. French ne is X° (head) but merges in TP, not CP — factor (iii) fails.

def Greco2020.frenchSnegConditions : SnegConditions

French: ne is X° (head), but Snegs are not attested. @cite{greco-2020} §4.2.9: ne merges in TP area (standard NegP), not externally merged in CP, so factor (iii) fails.

Equations

• Greco2020.frenchSnegConditions = { hasNegMorpheme := true, negIsHead := true, mergePosition := Minimalist.NegScope.NegMergePosition.tp, tpIsFocused := false }

theorem Greco2020.french_no_snegs : frenchSnegConditions.yieldsSnegs = false

Differentiation from NRQs and ENEs (@cite{greco-2020} §3)

All three belong to strong EN but differ on four diagnostics:

Property	Sneg	NRQ	ENE
Wh-elements	✗	✓	✓
Answerhood	✓	✗	✗
Embeddable (factive)	✗	—	✓
dopo tutto	✗	✓	—

inductive Greco2020.StrongENType : Type

• sneg : StrongENType
• nrq : StrongENType
• ene : StrongENType

@[implicit_reducible]

instance Greco2020.instDecidableEqStrongENType : DecidableEq StrongENType

Equations

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

@[implicit_reducible]

instance Greco2020.instReprStrongENType : Repr StrongENType

Equations

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

def Greco2020.instReprStrongENType.repr : StrongENType → ℕ → Std.Format

Equations

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

def Greco2020.StrongENType.equivFin : StrongENType ≃ Fin 3

StrongENType ≃ Fin 3.

Equations

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

@[implicit_reducible]

instance Greco2020.instFintypeStrongENType : Fintype StrongENType

Equations

• Greco2020.instFintypeStrongENType = Fintype.ofEquiv (Fin 3) Greco2020.StrongENType.equivFin.symm

def Greco2020.StrongENType.allowsWh : StrongENType → Bool

Equations

• Greco2020.StrongENType.sneg.allowsWh = false
• Greco2020.StrongENType.nrq.allowsWh = true
• Greco2020.StrongENType.ene.allowsWh = true

def Greco2020.StrongENType.isAnswer : StrongENType → Bool

Equations

• Greco2020.StrongENType.sneg.isAnswer = true
• Greco2020.StrongENType.nrq.isAnswer = false
• Greco2020.StrongENType.ene.isAnswer = false

def Greco2020.StrongENType.embeddableUnderFactive : StrongENType → Bool

Equations

• Greco2020.StrongENType.sneg.embeddableUnderFactive = false
• Greco2020.StrongENType.nrq.embeddableUnderFactive = false
• Greco2020.StrongENType.ene.embeddableUnderFactive = true

def Greco2020.StrongENType.enStrength : StrongENType → Phenomena.Negation.ExpletiveNegation.ENStrength

Equations

• Greco2020.StrongENType.sneg.enStrength = Phenomena.Negation.ExpletiveNegation.ENStrength.strong
• Greco2020.StrongENType.nrq.enStrength = Phenomena.Negation.ExpletiveNegation.ENStrength.strong
• Greco2020.StrongENType.ene.enStrength = Phenomena.Negation.ExpletiveNegation.ENStrength.strong

theorem Greco2020.all_strong_en (t : StrongENType) : t.enStrength = Phenomena.Negation.ExpletiveNegation.ENStrength.strong

theorem Greco2020.sneg_unique_answerhood : List.filter StrongENType.isAnswer [StrongENType.sneg, StrongENType.nrq, StrongENType.ene] = [StrongENType.sneg]

Snegs are the only strong EN type that can serve as answers.

theorem Greco2020.sneg_unique_wh_rejection : List.filter (fun (t : StrongENType) => !t.allowsWh) [StrongENType.sneg, StrongENType.nrq, StrongENType.ene] = [StrongENType.sneg]

Snegs are the only strong EN type that rejects Wh-elements.

theorem Greco2020.strongEN_fingerprint_injective : Function.Injective fun (t : StrongENType) => (t.allowsWh, t.isAnswer, t.embeddableUnderFactive)

The three-column diagnostic table (Wh, answerhood, embeddability) uniquely identifies each StrongENType — formalizing @cite{greco-2020} Table 3's claim that sneg, NRQ, and ENE are empirically distinct.