Spanish Negation Fragment

[Mie05] [Has13b] [DH13a] [Zan97]

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 Spanish.Negation.no : Syntax.Negation.NegMarkerEntry

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

Equations

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

def Spanish.Negation.negationSystem : Syntax.Negation.NegationSystem

The Spanish negation system: a single preverbal particle.

Equations

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

structure Spanish.Negation.NegExample : Type

A Spanish negation example.

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

@[instance_reducible]

instance Spanish.Negation.instReprNegExample : Repr NegExample

Equations

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

def Spanish.Negation.instReprNegExample.repr : NegExample → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Spanish.Negation.instBEqNegExample : BEq NegExample

Equations

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

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

Equations

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

def Spanish.Negation.present : NegExample

Equations

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

def Spanish.Negation.preterite : NegExample

Equations

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

def Spanish.Negation.imperfect : NegExample

Equations

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

def Spanish.Negation.future : NegExample

Equations

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

def Spanish.Negation.subjunctive : NegExample

Equations

• 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 Spanish.Negation.allExamples : List NegExample

Equations

• Spanish.Negation.allExamples = [Spanish.Negation.present, Spanish.Negation.preterite, Spanish.Negation.imperfect, Spanish.Negation.future, Spanish.Negation.subjunctive]

structure Spanish.Negation.NegConcordExample : Type

A negative concord example showing the position-dependent pattern.

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

@[instance_reducible]

instance Spanish.Negation.instReprNegConcordExample : Repr NegConcordExample

Equations

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

def Spanish.Negation.instReprNegConcordExample.repr : NegConcordExample → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Spanish.Negation.instBEqNegConcordExample : BEq NegConcordExample

Equations

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

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

Equations

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

def Spanish.Negation.preverbalNadie : NegConcordExample

Preverbal n-word: no absent.

Equations

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

def Spanish.Negation.postverbalNada : NegConcordExample

Postverbal n-word: no required.

Equations

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

Verification

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

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