Greek Negation Fragment

[Tsi25] [Has13b] [DH13a]

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 [Tsi25] argues is cross-linguistically valid.

@[reducible, inline]

abbrev Greek.StandardModern.Negation.World : Type

Equations

• Greek.StandardModern.Negation.World = Fin 4

Negation marker entries

structure Greek.StandardModern.Negation.MoodMarkerEntry : Type

A Greek sentential negation marker, augmented with the mood/NCI properties from [Tsi25]'s NEG₁/NEG₂ analysis.

Distinct from the cross-linguistic Syntax.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 Greek.StandardModern.Negation.instReprMoodMarkerEntry.repr : MoodMarkerEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Greek.StandardModern.Negation.instReprMoodMarkerEntry : Repr MoodMarkerEntry

Equations

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

@[implicit_reducible]

instance Greek.StandardModern.Negation.instBEqMoodMarkerEntry : BEq MoodMarkerEntry

Equations

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

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

Equations

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

def Greek.StandardModern.Negation.dhen : MoodMarkerEntry

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

Equations

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

def 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

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

Cross-linguistic substrate

def Greek.StandardModern.Negation.dhenMarker : Syntax.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

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

def Greek.StandardModern.Negation.minMarker : Syntax.Negation.NegMarkerEntry

min in Core substrate form.

Equations

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

def Greek.StandardModern.Negation.negationSystem : Syntax.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 Studies/Dryer2013Negation.lean.

Equations

• Greek.StandardModern.Negation.negationSystem = Syntax.Negation.NegationSystem.ofISO "ell" [Greek.StandardModern.Negation.dhenMarker, Greek.StandardModern.Negation.minMarker]

Semantics

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

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

Equations

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

def Greek.StandardModern.Negation.minNegSem (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.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

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

def Greek.StandardModern.Negation.minExplSem (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.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

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

def Greek.StandardModern.Negation.allMarkers : List MoodMarkerEntry

Greek has exactly two sentential negation markers.

Equations

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