Greek Negation Fragment

@cite{tsiakmakis-2025}

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.

structure Fragments.Greek.Negation.NegMarkerEntry : Type

A Greek sentential negation marker.

• 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'?

instance Fragments.Greek.Negation.instReprNegMarkerEntry : Repr NegMarkerEntry

Equations

• Fragments.Greek.Negation.instReprNegMarkerEntry = { reprPrec := Fragments.Greek.Negation.instReprNegMarkerEntry.repr }

def Fragments.Greek.Negation.instReprNegMarkerEntry.repr : NegMarkerEntry → ℕ → Std.Format

Equations

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

instance Fragments.Greek.Negation.instBEqNegMarkerEntry : BEq NegMarkerEntry

Equations

• Fragments.Greek.Negation.instBEqNegMarkerEntry = { beq := Fragments.Greek.Negation.instBEqNegMarkerEntry.beq }

def Fragments.Greek.Negation.instBEqNegMarkerEntry.beq : NegMarkerEntry → NegMarkerEntry → Bool

Equations

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

def Fragments.Greek.Negation.dhen : NegMarkerEntry

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

Equations

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

def Fragments.Greek.Negation.min : NegMarkerEntry

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.Negation.min = { form := "min", greek := "μην", isIndicative := false, isStandardNegation := false, licensesNCIs := false }

def Fragments.Greek.Negation.dhenSem (p : Semantics.Attitudes.Intensional.World → Bool) : Semantics.Attitudes.Intensional.World → Bool

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

Equations

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

def Fragments.Greek.Negation.minNegSem (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : Bool

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.Negation.minNegSem f g p w = Semantics.Modality.Kratzer.necessity f g (fun (w' : Semantics.Attitudes.Intensional.World) => !p w') w

def Fragments.Greek.Negation.minExplSem (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : Bool

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.Negation.minExplSem f g p w = Semantics.Modality.Kratzer.necessity f g p w

def Fragments.Greek.Negation.allMarkers : List NegMarkerEntry

Greek has exactly two sentential negation markers.

Equations

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

theorem Fragments.Greek.Negation.mood_complementarity : dhen.isIndicative = true ∧ min.isIndicative = false

The two markers differ in mood selection.

theorem Fragments.Greek.Negation.dhen_is_standard : dhen.isStandardNegation = true ∧ min.isStandardNegation = false

Only dhen is standard truth-reversing negation.

theorem Fragments.Greek.Negation.nci_licensing : dhen.licensesNCIs = true ∧ min.licensesNCIs = false

Only dhen licenses NCIs.