Spanish Negation Fragment

@cite{miestamo-2005} @cite{haspelmath-2013} @cite{dryer-haspelmath-2013} @cite{zanuttini-1997}

Spanish expresses standard negation with the preverbal particle no. Negation is symmetric: adding no introduces no structural changes to the clause — no finiteness change, no TAM restrictions, no paradigmatic gaps.

Examples

Tense	Affirmative	Negative
Present	Juan come	Juan no come
Preterite	Juan comió	Juan no comió
Imperfect	Juan comía	Juan no comía
Future	Juan comerá	Juan no comerá
Subjunctive	que Juan coma	que Juan no coma

Negative concord (n-words)

Spanish has position-dependent negative concord (WALS Ch 115: mixed):

• Preverbal n-words preclude no: Nadie vino 'Nobody came'
• Postverbal n-words require no: No vi nada 'NEG saw nothing'

The pattern parallels Italian (nessuno/non). N-word lexemes — nadie, nada, nunca, ninguno — live in the sibling Fragments/Spanish/PolarityItems.lean per the operator/lexical-reactive split documented in Core/Lexical/NegMarker.lean. The NegConcordExample data below illustrates the marker's interaction with the n-word system at the sentence level (operator-side typology).

def Fragments.Spanish.Negation.no : Typology.Negation.NegMarkerEntry

no — Spanish's standard preverbal negation particle. A free word, syntactically immediately preverbal: Juan no come 'Juan doesn't eat'.

Equations

• Fragments.Spanish.Negation.no = { form := "no", morphemeType := Typology.Negation.NegMorphemeType.particle, position := Typology.Negation.NegMarkerPosition.preverbal }

def Fragments.Spanish.Negation.negationSystem : Typology.Negation.NegationSystem

The Spanish negation system: a single preverbal particle. The Fragment-side joint consumed by Phenomena/Negation/Studies/Dryer2013.lean.

Equations

• Fragments.Spanish.Negation.negationSystem = Typology.Negation.NegationSystem.ofISO "spa" [Fragments.Spanish.Negation.no]

structure Fragments.Spanish.Negation.NegExample : Type

A Spanish negation example.

• affirmative : String
• negative : String
• gloss : String
• tenseLabel : String

def Fragments.Spanish.Negation.instReprNegExample.repr : NegExample → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Spanish.Negation.instReprNegExample : Repr NegExample

Equations

• Fragments.Spanish.Negation.instReprNegExample = { reprPrec := Fragments.Spanish.Negation.instReprNegExample.repr }

@[implicit_reducible]

instance Fragments.Spanish.Negation.instBEqNegExample : BEq NegExample

Equations

• Fragments.Spanish.Negation.instBEqNegExample = { beq := Fragments.Spanish.Negation.instBEqNegExample.beq }

def Fragments.Spanish.Negation.instBEqNegExample.beq : NegExample → NegExample → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Spanish.Negation.instBEqNegExample.beq x✝¹ x✝ = false

def Fragments.Spanish.Negation.present : NegExample

Equations

• Fragments.Spanish.Negation.present = { affirmative := "Juan come", negative := "Juan no come", gloss := "Juan eats / Juan NEG eats", tenseLabel := "present" }

def Fragments.Spanish.Negation.preterite : NegExample

Equations

• Fragments.Spanish.Negation.preterite = { affirmative := "Juan comió", negative := "Juan no comió", gloss := "Juan ate / Juan NEG ate", tenseLabel := "preterite" }

def Fragments.Spanish.Negation.imperfect : NegExample

Equations

• Fragments.Spanish.Negation.imperfect = { affirmative := "Juan comía", negative := "Juan no comía", gloss := "Juan ate.IMPF / Juan NEG ate.IMPF", tenseLabel := "imperfect" }

def Fragments.Spanish.Negation.future : NegExample

Equations

• Fragments.Spanish.Negation.future = { affirmative := "Juan comerá", negative := "Juan no comerá", gloss := "Juan will.eat / Juan NEG will.eat", tenseLabel := "future" }

def Fragments.Spanish.Negation.subjunctive : NegExample

Equations

• Fragments.Spanish.Negation.subjunctive = { affirmative := "que Juan coma", negative := "que Juan no coma", gloss := "that Juan eat.SUBJ / that Juan NEG eat.SUBJ", tenseLabel := "subjunctive" }

def Fragments.Spanish.Negation.allExamples : List NegExample

Equations

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

structure Fragments.Spanish.Negation.NegConcordExample : Type

A negative concord example showing the position-dependent pattern.

• sentence : String
• translation : String
• hasNo : Bool
• nwordPosition : String

def Fragments.Spanish.Negation.instReprNegConcordExample.repr : NegConcordExample → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Spanish.Negation.instReprNegConcordExample : Repr NegConcordExample

Equations

• Fragments.Spanish.Negation.instReprNegConcordExample = { reprPrec := Fragments.Spanish.Negation.instReprNegConcordExample.repr }

def Fragments.Spanish.Negation.instBEqNegConcordExample.beq : NegConcordExample → NegConcordExample → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Spanish.Negation.instBEqNegConcordExample.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Fragments.Spanish.Negation.instBEqNegConcordExample : BEq NegConcordExample

Equations

• Fragments.Spanish.Negation.instBEqNegConcordExample = { beq := Fragments.Spanish.Negation.instBEqNegConcordExample.beq }

def Fragments.Spanish.Negation.preverbalNadie : NegConcordExample

Preverbal n-word: no absent.

Equations

• Fragments.Spanish.Negation.preverbalNadie = { sentence := "Nadie vino", translation := "Nobody came", hasNo := false, nwordPosition := "preverbal" }

def Fragments.Spanish.Negation.postverbalNada : NegConcordExample

Postverbal n-word: no required.

Equations

• Fragments.Spanish.Negation.postverbalNada = { sentence := "No vi nada", translation := "I didn't see anything", hasNo := true, nwordPosition := "postverbal" }

Verification

theorem Fragments.Spanish.Negation.all_tenses_available : allExamples.length = 5

All five tenses are available under negation (no paradigmatic gaps).

theorem Fragments.Spanish.Negation.all_negative_contain_no : (allExamples.all fun (e : NegExample) => Fragments.Spanish.Negation.hasSubstr✝ e.negative " no ") = true

All negative examples contain no.

def Fragments.Spanish.Negation.negationProfile : Typology.Negation.NegationProfile

Spanish negation profile (WALS Ch 112-115 + Greco/JinKoenig fields).

Equations

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