Spanish Negation Fragment

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

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).

def Fragments.Spanish.Negation.negMarker : String

The Spanish standard negation marker.

Equations

• Fragments.Spanish.Negation.negMarker = "no"

structure Fragments.Spanish.Negation.NegExample : Type

A Spanish negation example.

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

instance Fragments.Spanish.Negation.instReprNegExample : Repr NegExample

Equations

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

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

Equations

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

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.NWordEntry : Type

A Spanish n-word entry.

• form : String
• gloss : String
• preverbalAlone : Bool

  Can this n-word appear preverbally without no?

def Fragments.Spanish.Negation.instReprNWordEntry.repr : NWordEntry → Nat → Std.Format

Equations

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

instance Fragments.Spanish.Negation.instReprNWordEntry : Repr NWordEntry

Equations

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

def Fragments.Spanish.Negation.instBEqNWordEntry.beq : NWordEntry → NWordEntry → Bool

Equations

• Fragments.Spanish.Negation.instBEqNWordEntry.beq { form := a, gloss := a_1, preverbalAlone := a_2 } { form := b, gloss := b_1, preverbalAlone := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Fragments.Spanish.Negation.instBEqNWordEntry.beq x✝¹ x✝ = false

instance Fragments.Spanish.Negation.instBEqNWordEntry : BEq NWordEntry

Equations

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

def Fragments.Spanish.Negation.nadie : NWordEntry

nadie — nobody. Preverbal alone: Nadie vino.

Equations

• Fragments.Spanish.Negation.nadie = { form := "nadie", gloss := "nobody", preverbalAlone := true }

def Fragments.Spanish.Negation.nada : NWordEntry

nada — nothing. Postverbal requires no: No vi nada.

Equations

• Fragments.Spanish.Negation.nada = { form := "nada", gloss := "nothing", preverbalAlone := true }

def Fragments.Spanish.Negation.nunca : NWordEntry

nunca — never. Preverbal alone: Nunca viene.

Equations

• Fragments.Spanish.Negation.nunca = { form := "nunca", gloss := "never", preverbalAlone := true }

def Fragments.Spanish.Negation.ninguno : NWordEntry

ninguno — no one / none.

Equations

• Fragments.Spanish.Negation.ninguno = { form := "ninguno", gloss := "none", preverbalAlone := true }

def Fragments.Spanish.Negation.allNWords : List NWordEntry

Equations

• Fragments.Spanish.Negation.allNWords = [Fragments.Spanish.Negation.nadie, Fragments.Spanish.Negation.nada, Fragments.Spanish.Negation.nunca, Fragments.Spanish.Negation.ninguno]

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.

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

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.negMarker_is_no : negMarker = "no"

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.

theorem Fragments.Spanish.Negation.preverbal_no_absent : preverbalNadie.hasNo = false

Preverbal n-word: no absent.

theorem Fragments.Spanish.Negation.postverbal_no_required : postverbalNada.hasNo = true

Postverbal n-word: no required.