French Negation Fragment

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

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. Phonologically a clitic on the finite verb (or auxiliary); syntactically the head of NegP per @cite{zanuttini-1997}'s cartography. Near-categorically dropped in spoken French (Jespersen cycle stage III), categorically present in formal written French.

Equations

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

def Fragments.French.Negation.pasReinforcer : String

The French postverbal negative reinforcer pas. Originally a noun 'step' grammaticalized via the Jespersen cycle into the load-bearing negation marker of modern French. Sits in the specifier of NegP per @cite{zanuttini-1997}.

Equations

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

def Fragments.French.Negation.bipartite : Typology.Negation.NegMarkerEntry

(ne) pas — French's bipartite standard negation. The two morphemes flank the finite verb: Je ne mange pas (formal), Je mange pas (colloquial, ne-drop). Encoded as a single NegMarkerEntry with discontinuous position because ne and pas together constitute one logical negation construction (one WALS Ch 112A value, one Ch 143A value). The constituent forms neClitic and pasReinforcer are exposed separately for downstream consumers that need them (JinKoenig2021 uses ne alone as the EN marker; Miestamo2005 lists both as negMarkers).

Equations

• Fragments.French.Negation.bipartite = { form := "(ne) pas", morphemeType := Typology.Negation.NegMorphemeType.doubleNeg, position := Typology.Negation.NegMarkerPosition.discontinuous }

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

The French negation system: a single bipartite construction. Length-1 markers list — ne and pas are not alternative markers but two morphemes of one bipartite construction. The Fragment-side joint consumed by Phenomena/Negation/Studies/Dryer2013.lean.

Equations

• Fragments.French.Negation.negationSystem = Typology.Negation.NegationSystem.ofISO "fra" [Fragments.French.Negation.bipartite]

structure Fragments.French.Negation.NegExample : Type

A French negation example.

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

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

Equations

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

@[implicit_reducible]

instance Fragments.French.Negation.instReprNegExample : Repr NegExample

Equations

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

@[implicit_reducible]

instance Fragments.French.Negation.instBEqNegExample : BEq NegExample

Equations

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

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

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.

Verification

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)

@[implicit_reducible]

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.

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

@[implicit_reducible]

instance Fragments.French.Negation.instBEqENTriggerNegator : BEq ENTriggerNegator

Equations

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

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.

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

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

Equations

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