Greek Negation Fragment

@cite{tsiakmakis-2025} @cite{haspelmath-2013} @cite{dryer-haspelmath-2013}

Greek distinguishes two sentential negation markers that are in complementary distribution by mood:

• dhen (δεν): indicative negator (NEG₁). Standard sentential negation reversing truth conditions: ⟦dhen⟧ = λp.¬p.

• min (μην): subjunctive/modal negator (NEG₂). Appears in non-veridical environments (imperatives, subjunctive complements, fear-predicate complements). As canonical negation, ⟦min⟧ = λp.∀w' ∈ Best_g(w) : ¬p(w'). As expletive negation, the negation component is absent: ⟦min_expletive⟧ = λp.∀w' ∈ Best_g(w) : p(w').

The two markers are the overt morphological reflex of the NEG₁/NEG₂ distinction that @cite{tsiakmakis-2025} argues is cross-linguistically valid.

@[reducible, inline]

abbrev Fragments.Greek.StandardModern.Negation.World : Type

Equations

• Fragments.Greek.StandardModern.Negation.World = Fin 4

structure Fragments.Greek.StandardModern.Negation.MoodMarkerEntry : Type

A Greek sentential negation marker, augmented with the mood/NCI properties from @cite{tsiakmakis-2025}'s NEG₁/NEG₂ analysis.

Distinct from the cross-linguistic Typology.Negation.NegMarkerEntry substrate (which carries only form/morphemeType/position): this structure exposes the Tsiakmakis-specific paper apparatus that other languages don't have analogues for. The Core entries dhenMarker and minMarker below are the cross-linguistic typology face.

• form : String

  Surface form (romanization)

• greek : String

  Greek orthography

• isIndicative : Bool

  Indicative (dhen) or subjunctive/modal (min)

• isStandardNegation : Bool

  Does the marker function as standard truth-reversing negation?

• licensesNCIs : Bool

  Can the marker license NCIs like tipota 'nothing'?

def Fragments.Greek.StandardModern.Negation.instReprMoodMarkerEntry.repr : MoodMarkerEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Greek.StandardModern.Negation.instReprMoodMarkerEntry : Repr MoodMarkerEntry

Equations

• Fragments.Greek.StandardModern.Negation.instReprMoodMarkerEntry = { reprPrec := Fragments.Greek.StandardModern.Negation.instReprMoodMarkerEntry.repr }

@[implicit_reducible]

instance Fragments.Greek.StandardModern.Negation.instBEqMoodMarkerEntry : BEq MoodMarkerEntry

Equations

• Fragments.Greek.StandardModern.Negation.instBEqMoodMarkerEntry = { beq := Fragments.Greek.StandardModern.Negation.instBEqMoodMarkerEntry.beq }

def Fragments.Greek.StandardModern.Negation.instBEqMoodMarkerEntry.beq : MoodMarkerEntry → MoodMarkerEntry → Bool

Equations

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

def Fragments.Greek.StandardModern.Negation.dhen : MoodMarkerEntry

dhen (δεν): indicative sentential negation. Negates the verbal predicate of an indicative sentence. Licenses NCIs (tipota, kanenas).

Equations

• Fragments.Greek.StandardModern.Negation.dhen = { form := "dhen", greek := "δεν", isIndicative := true, isStandardNegation := true, licensesNCIs := true }

def Fragments.Greek.StandardModern.Negation.min : MoodMarkerEntry

min (μην): subjunctive/modal negation. Appears in non-veridical environments: imperatives, subjunctive complements, fear-predicate complements, conditionals, biased questions. Does NOT license NCIs when expletive.

Equations

• Fragments.Greek.StandardModern.Negation.min = { form := "min", greek := "μην", isIndicative := false, isStandardNegation := false, licensesNCIs := false }

def Fragments.Greek.StandardModern.Negation.dhenMarker : Typology.Negation.NegMarkerEntry

dhen in Core substrate form. Cross-linguistic typology face of the indicative negator; the paper-specific mood/NCI apparatus lives on MoodMarkerEntry above.

Equations

• Fragments.Greek.StandardModern.Negation.dhenMarker = { form := "dhen", morphemeType := Typology.Negation.NegMorphemeType.particle, position := Typology.Negation.NegMarkerPosition.preverbal }

def Fragments.Greek.StandardModern.Negation.minMarker : Typology.Negation.NegMarkerEntry

min in Core substrate form.

Equations

• Fragments.Greek.StandardModern.Negation.minMarker = { form := "min", morphemeType := Typology.Negation.NegMorphemeType.particle, position := Typology.Negation.NegMarkerPosition.preverbal }

def Fragments.Greek.StandardModern.Negation.negationSystem : Typology.Negation.NegationSystem

The Greek negation system: two mood-conditioned preverbal particles. dhen (indicative, default-context) listed first, min (subjunctive/ modal) second. The Fragment-side joint consumed by Phenomena/Negation/Studies/Dryer2013.lean.

Equations

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

def Fragments.Greek.StandardModern.Negation.dhenSem (p : World → Bool) : World → Bool

Semantics of dhen: standard truth-functional negation. ⟦dhen⟧ = λp.¬p

Equations

• Fragments.Greek.StandardModern.Negation.dhenSem p w = !p w

def Fragments.Greek.StandardModern.Negation.minNegSem (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World) : Prop

Semantics of negative min: modal negation over Best worlds. ⟦min⟧^g(w) = λp. ∀w' ∈ Best_g(w) : ¬p(w') Used in imperatives (Min pas! 'Don't go!') and with canonical dhen (Fovame min dhen efaye 'I fear he maybe didn't eat').

Equations

• Fragments.Greek.StandardModern.Negation.minNegSem f g p w = Semantics.Modality.Kratzer.necessity f g (fun (w' : Fragments.Greek.StandardModern.Negation.World) => ¬p w') w

def Fragments.Greek.StandardModern.Negation.minExplSem (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World) : Prop

Semantics of expletive min: modal without negation. ⟦min_expletive⟧^g(w) = λp. ∀w' ∈ Best_g(w) : p(w') Used in fear complements (Fovame min efaye 'I fear he maybe ate'), conditionals (Min ksexaso kati 'If I forget something'), and biased questions (Min efaye? 'Did he maybe eat?').

Equations

• Fragments.Greek.StandardModern.Negation.minExplSem f g p w = Semantics.Modality.Kratzer.necessity f g p w

def Fragments.Greek.StandardModern.Negation.allMarkers : List MoodMarkerEntry

Greek has exactly two sentential negation markers.

Equations

• Fragments.Greek.StandardModern.Negation.allMarkers = [Fragments.Greek.StandardModern.Negation.dhen, Fragments.Greek.StandardModern.Negation.min]