French Negation Fragment

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

French uses bipartite negation ne...pas, with the preverbal clitic ne and the postverbal reinforcer pas. In colloquial speech, ne is frequently dropped (Jespersen cycle stage II→III).

Symmetric negation

WALS classifies French negation as symmetric: adding ne...pas does not change the clause structure, verb form, or paradigm. All TAM distinctions are available under negation.

Jespersen cycle

French is a textbook case of the Jespersen cycle:

1. Latin non (preverbal only)
2. Old French ne...pas (bipartite, pas = reinforcer from 'step')
3. Colloquial French pas (postverbal only, ne dropped)

The ne-drop is sociolinguistically conditioned: near-categorical in informal speech, variable in formal registers.

def Fragments.French.Negation.neClitic : String

The French preverbal negative clitic.

Equations

• Fragments.French.Negation.neClitic = "ne"

def Fragments.French.Negation.pasReinforcer : String

The French postverbal negative reinforcer.

Equations

• Fragments.French.Negation.pasReinforcer = "pas"

structure Fragments.French.Negation.NegExample : Type

A French negation example.

• affirmative : String
• negativeFormal : String
• negativeColloquial : String
• gloss : String
• tenseLabel : String

instance Fragments.French.Negation.instReprNegExample : Repr NegExample

Equations

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

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

Equations

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

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

Equations

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

instance Fragments.French.Negation.instBEqNegExample : BEq NegExample

Equations

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

def Fragments.French.Negation.present : NegExample

Present tense.

Equations

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

def Fragments.French.Negation.passeCompose : NegExample

Passé composé (compound past).

Equations

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

def Fragments.French.Negation.imparfait : NegExample

Imparfait (imperfect).

Equations

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

def Fragments.French.Negation.futurSimple : NegExample

Futur simple (simple future).

Equations

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

def Fragments.French.Negation.subjonctif : NegExample

Subjonctif (subjunctive).

Equations

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

def Fragments.French.Negation.allExamples : List NegExample

Equations

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

structure Fragments.French.Negation.NegReinforcer : Type

Other negative reinforcers (besides pas).

• form : String
• gloss : String
• restrictedNeg : Bool

def Fragments.French.Negation.instReprNegReinforcer.repr : NegReinforcer → Nat → Std.Format

Equations

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

instance Fragments.French.Negation.instReprNegReinforcer : Repr NegReinforcer

Equations

• Fragments.French.Negation.instReprNegReinforcer = { reprPrec := Fragments.French.Negation.instReprNegReinforcer.repr }

instance Fragments.French.Negation.instBEqNegReinforcer : BEq NegReinforcer

Equations

• Fragments.French.Negation.instBEqNegReinforcer = { beq := Fragments.French.Negation.instBEqNegReinforcer.beq }

def Fragments.French.Negation.instBEqNegReinforcer.beq : NegReinforcer → NegReinforcer → Bool

Equations

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

def Fragments.French.Negation.plus : NegReinforcer

plus 'no more/longer'.

Equations

• Fragments.French.Negation.plus = { form := "plus", gloss := "no.more", restrictedNeg := true }

def Fragments.French.Negation.jamais : NegReinforcer

jamais 'never'.

Equations

• Fragments.French.Negation.jamais = { form := "jamais", gloss := "never", restrictedNeg := true }

def Fragments.French.Negation.rien : NegReinforcer

rien 'nothing'.

Equations

• Fragments.French.Negation.rien = { form := "rien", gloss := "nothing", restrictedNeg := true }

def Fragments.French.Negation.personne : NegReinforcer

personne 'nobody'.

Equations

• Fragments.French.Negation.personne = { form := "personne", gloss := "nobody", restrictedNeg := true }

def Fragments.French.Negation.allReinforcers : List NegReinforcer

Equations

• Fragments.French.Negation.allReinforcers = [Fragments.French.Negation.plus, Fragments.French.Negation.jamais, Fragments.French.Negation.rien, Fragments.French.Negation.personne]

Verification

theorem Fragments.French.Negation.neClitic_is_ne : neClitic = "ne"

theorem Fragments.French.Negation.pasReinforcer_is_pas : pasReinforcer = "pas"

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

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

theorem Fragments.French.Negation.formal_contains_pas : (allExamples.all fun (e : NegExample) => Fragments.French.Negation.hasSubstr✝ e.negativeFormal "pas") = true

All formal negatives contain pas.

theorem Fragments.French.Negation.formal_contains_n : (allExamples.all fun (e : NegExample) => Fragments.French.Negation.hasSubstr✝ e.negativeFormal "ne " || Fragments.French.Negation.hasSubstr✝¹ e.negativeFormal "n'") = true

All formal negatives contain the n component (ne or n').

theorem Fragments.French.Negation.colloquial_contains_pas : (allExamples.all fun (e : NegExample) => Fragments.French.Negation.hasSubstr✝ e.negativeColloquial "pas") = true

All colloquial negatives contain pas.

Expletive Negation

@cite{jin-koenig-2021}

French has a dedicated expletive negation marker: the preverbal clitic ne used alone (without pas). This is the grammaticalized form of EN, distinct from standard ne...pas. In a few low-entrenchment contexts (REGRET, FORGET), the full ne...pas appears instead.

Trigger class	EN negator	Entrenchment
FEAR	ne	high
BEFORE	ne	high
UNLESS	ne	high
DENY	ne	high (requires negation/question)
REGRET	ne (pas)	low
FORGET	ne pas	low
COMPARATIVES	ne	high

The distinction between ne (EN) and ne...pas (standard) makes French uniquely transparent: the grammaticalization of EN is visible in the form of the negator itself.

structure Fragments.French.Negation.ENTriggerNegator : Type

An expletive negation marker and its trigger context.

• triggerClass : String

  The trigger class label (from @cite{jin-koenig-2021} Table 5)

• triggerForm : String

  French lexical trigger

• enNegatorForm : String

  EN negator form

• highEntrenchment : Bool

  Whether the EN is highly entrenched (grammaticalized)

instance Fragments.French.Negation.instReprENTriggerNegator : Repr ENTriggerNegator

Equations

• Fragments.French.Negation.instReprENTriggerNegator = { reprPrec := Fragments.French.Negation.instReprENTriggerNegator.repr }

def Fragments.French.Negation.instReprENTriggerNegator.repr : ENTriggerNegator → Nat → Std.Format

Equations

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

instance Fragments.French.Negation.instBEqENTriggerNegator : BEq ENTriggerNegator

Equations

• Fragments.French.Negation.instBEqENTriggerNegator = { beq := Fragments.French.Negation.instBEqENTriggerNegator.beq }

def Fragments.French.Negation.instBEqENTriggerNegator.beq : ENTriggerNegator → ENTriggerNegator → Bool

Equations

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

def Fragments.French.Negation.enMarker : String

ne alone is the dedicated EN marker (grammaticalized).

Equations

• Fragments.French.Negation.enMarker = Fragments.French.Negation.neClitic

def Fragments.French.Negation.enTriggerNegators : List ENTriggerNegator

EN trigger-negator pairings from @cite{jin-koenig-2021}, Table 5 and §6.1–6.4.

Equations

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

theorem Fragments.French.Negation.high_entrenchment_uses_ne_alone : ((List.filter (fun (x : ENTriggerNegator) => x.highEntrenchment) enTriggerNegators).all fun (x : ENTriggerNegator) => x.enNegatorForm == "ne") = true

High-entrenchment EN uses the dedicated ne alone; low-entrenchment EN uses ne...pas (the standard negator).

theorem Fragments.French.Negation.en_marker_is_ne_clitic : enMarker = neClitic

French EN marker = preverbal ne = same clitic as in standard ne...pas, but without the reinforcer.