Tsiakmakis (2025): On the Non-Homogeneity of Expletive Negation in Greek and Beyond

This file formalizes Tsiakmakis's two kinds of expletive negation. Greek has two sentential negators in complementary distribution by mood: indicative dhen, standard negation, (7), the complement, and non-veridical min, (13), a modal negation, neg2, true when the negated proposition holds throughout the best worlds of an ordering source in Kratzer's sense. Both have non-negative uses, (20): dhen in negative exclamatives, rhetorical questions and preposed negation questions, min in fear complements, conditionals and polar questions. Expletive dhen is dhen, (37): its negation is masked by rhetoricity or by the speaker's bias at the level of the utterance. Expletive min keeps the modal component and drops the negation, (58): a biased epistemic modal, neg2Expl. The diagnostics follow from the semantics. Canonical dhen under expletive min yields negative min, (39), (47), (53), neg2Expl_compl, whereas dhen under dhen cancels; expletive min conveys positive bias, every best world being a p-world, so it excludes the ignorance of a min-free question, in which both alternatives are possible, (55), not_ignorant_of_mem_neg2Expl, and it is consistent with negative min only when no world is best, bestWorlds_eq_empty_of_mem_neg2Expl_of_mem_neg2. The survey of section 5 sorts the host inventory into apparent hosts, featuring NEG₁ under a masking factor, ApparentHost and ApparentHost.masking, and hosts proper, featuring NEG₂ as the spell-out of an epistemic or deontic ordering source, ProperHost, the revised inventory (95), Host; every Greek host of expletive negation in the rows features the Greek spell-out of its class's negator, dhen in the apparent hosts and min in the hosts proper, (20) (greek_expletive_negator).

Implementation notes

Propositions are sets of worlds, NEG₁ is their complement, (93), and NEG₂ is the substrate's Modality.necessity, the best worlds of a modal base and an ordering source. Greek spells the two negators with the markers of its fragment (Negator.greek). The flavour of the ordering source varies by host and language, epistemic for Greek min, deontic for French fear-predicate ne, and is not fixed here. The NCI-licensing and left-periphery diagnostics, (40) and (44), are syntactic and recorded by the rows, as are the arguments that negative exclamatives are rhetorical questions, (23)–(24), that preposed and non-preposed negation questions collapse, (32)–(35), and that conditionals and free relatives are tentative hosts. The examples are the rows of Data.Examples.Tsiakmakis2025.

References

• [Tsi25]
• [Kra81b]
• [Gia98]
• [RH04]
• [Tov96]
• [Tah21]
• [Gre20]
• [Esp92]

The two negators (section 2)

def Tsiakmakis2025.neg2 {W : Type u_1} (f g : Modality.Background W) (p : Set W) : Set W

(13): negative NEG₂, the negative min: the negation holds throughout the best worlds.

Equations

• Tsiakmakis2025.neg2 f g p = {w : W | Modality.necessity f g (fun (x : W) => x ∈ pᶜ) w}

def Tsiakmakis2025.neg2Expl {W : Type u_1} (f g : Modality.Background W) (p : Set W) : Set W

(58), (94): expletive NEG₂, the expletive min: the modal component without the negation, a modal biased towards the proposition.

Equations

• Tsiakmakis2025.neg2Expl f g p = {w : W | Modality.necessity f g (fun (x : W) => x ∈ p) w}

theorem Tsiakmakis2025.neg2Expl_compl {W : Type u_1} (f g : Modality.Background W) (p : Set W) : neg2Expl f g pᶜ = neg2 f g p

(39), (47), (53): canonical dhen under expletive min is negative min.

theorem Tsiakmakis2025.neg2_compl {W : Type u_1} (f g : Modality.Background W) (p : Set W) : neg2 f g pᶜ = neg2Expl f g p

Negative min applied to a negation is expletive min: the two share the modal component and differ by the negation alone.

theorem Tsiakmakis2025.not_possibility_compl_of_mem_neg2Expl {W : Type u_1} {f g : Modality.Background W} {p : Set W} {w : W} (h : w ∈ neg2Expl f g p) : ¬Modality.possibility f g (fun (x : W) => x ∈ pᶜ) w

Positive bias: under expletive min the negative alternative holds in no best world.

def Tsiakmakis2025.Ignorant {W : Type u_1} {f g : Modality.Background W} (p : Set W) (w : W) : Prop

The ignorance of a min-free question, (55b): both alternatives hold in some best world.

Equations

• Tsiakmakis2025.Ignorant p w = (Modality.possibility f g (fun (x : W) => x ∈ p) w ∧ Modality.possibility f g (fun (x : W) => x ∈ pᶜ) w)

theorem Tsiakmakis2025.not_ignorant_of_mem_neg2Expl {W : Type u_1} {f g : Modality.Background W} {p : Set W} {w : W} (h : w ∈ neg2Expl f g p) : ¬Ignorant p w

(55): a question with expletive min is not the question of an ignorant speaker.

theorem Tsiakmakis2025.bestWorlds_eq_empty_of_mem_neg2Expl_of_mem_neg2 {W : Type u_1} {f g : Modality.Background W} {p : Set W} {w : W} (h₁ : w ∈ neg2Expl f g p) (h₂ : w ∈ neg2 f g p) : Modality.bestWorlds f g w = ∅

Expletive and negative min are jointly satisfiable only when no world is best.

The revised host inventory (section 5)

inductive Tsiakmakis2025.ApparentHost : Type

(95): apparent expletive negation hosts, whose negator is NEG₁ with its negation masked by a factor at the level of the utterance.

• temporalExpression : ApparentHost
• negativeAdverbial : ApparentHost
• comparative : ApparentHost
• optionallyBiasedQuestion : ApparentHost
• rhetoricalQuestion : ApparentHost
• exclamative : ApparentHost

@[instance_reducible]

instance Tsiakmakis2025.instDecidableEqApparentHost : DecidableEq ApparentHost

Equations

• Tsiakmakis2025.instDecidableEqApparentHost x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Tsiakmakis2025.instReprApparentHost.repr : ApparentHost → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Tsiakmakis2025.instReprApparentHost : Repr ApparentHost

Equations

• Tsiakmakis2025.instReprApparentHost = { reprPrec := Tsiakmakis2025.instReprApparentHost.repr }

inductive Tsiakmakis2025.Masking : Type

The factors masking NEG₁: the lexical aspect that makes the negated and unnegated until-clauses coincide, (69); negative concord with the licensing adverbial, (73); the negation built into the comparative operator, of which NEG₁ is the spell-out, (78); the speaker's bias towards the positive answer, (36); and rhetoricity, the polarity reversal that rhetorical questions and negative exclamatives show without any negator, (29), (87).

• lexicalAspect : Masking
• negativeConcord : Masking
• comparativeOperator : Masking
• speakerBias : Masking
• rhetoricity : Masking

@[instance_reducible]

instance Tsiakmakis2025.instDecidableEqMasking : DecidableEq Masking

Equations

• Tsiakmakis2025.instDecidableEqMasking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Tsiakmakis2025.instReprMasking.repr : Masking → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Tsiakmakis2025.instReprMasking : Repr Masking

Equations

• Tsiakmakis2025.instReprMasking = { reprPrec := Tsiakmakis2025.instReprMasking.repr }

def Tsiakmakis2025.ApparentHost.masking : ApparentHost → Masking

The masking factor of each apparent host.

Equations

• Tsiakmakis2025.ApparentHost.temporalExpression.masking = Tsiakmakis2025.Masking.lexicalAspect
• Tsiakmakis2025.ApparentHost.negativeAdverbial.masking = Tsiakmakis2025.Masking.negativeConcord
• Tsiakmakis2025.ApparentHost.comparative.masking = Tsiakmakis2025.Masking.comparativeOperator
• Tsiakmakis2025.ApparentHost.optionallyBiasedQuestion.masking = Tsiakmakis2025.Masking.speakerBias
• Tsiakmakis2025.ApparentHost.rhetoricalQuestion.masking = Tsiakmakis2025.Masking.rhetoricity
• Tsiakmakis2025.ApparentHost.exclamative.masking = Tsiakmakis2025.Masking.rhetoricity

inductive Tsiakmakis2025.ProperHost : Type

(95): expletive negation hosts proper, whose negator is NEG₂, the spell-out of an ordering source; conditionals and free relatives are tentative, the former licensing NEG₂ in a positive antecedent only in Greek, (74), the latter ranking no worlds, (92).

• emotiveDoxasticPredicate : ProperHost
• negativePredicate : ProperHost
• dubitativePredicate : ProperHost
• biasedQuestion : ProperHost
• conditional : ProperHost
• freeRelative : ProperHost

@[instance_reducible]

instance Tsiakmakis2025.instDecidableEqProperHost : DecidableEq ProperHost

Equations

• Tsiakmakis2025.instDecidableEqProperHost x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Tsiakmakis2025.instReprProperHost : Repr ProperHost

Equations

• Tsiakmakis2025.instReprProperHost = { reprPrec := Tsiakmakis2025.instReprProperHost.repr }

def Tsiakmakis2025.instReprProperHost.repr : ProperHost → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Tsiakmakis2025.Host : Type

The revised inventory.

Equations

• Tsiakmakis2025.Host = (Tsiakmakis2025.ApparentHost ⊕ Tsiakmakis2025.ProperHost)

inductive Tsiakmakis2025.Negator : Type

The two negators.

• neg1 : Negator
• neg2 : Negator

@[instance_reducible]

instance Tsiakmakis2025.instDecidableEqNegator : DecidableEq Negator

Equations

• Tsiakmakis2025.instDecidableEqNegator x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Tsiakmakis2025.instReprNegator.repr : Negator → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Tsiakmakis2025.instReprNegator : Repr Negator

Equations

• Tsiakmakis2025.instReprNegator = { reprPrec := Tsiakmakis2025.instReprNegator.repr }

def Tsiakmakis2025.Host.negator : Host → Negator

The negator a host features, by its class.

Equations

• Tsiakmakis2025.Host.negator = Sum.elim (fun (x : Tsiakmakis2025.ApparentHost) => Tsiakmakis2025.Negator.neg1) fun (x : Tsiakmakis2025.ProperHost) => Tsiakmakis2025.Negator.neg2

def Tsiakmakis2025.Negator.greek : Negator → Negation.Marker

Greek spells NEG₁ dhen and NEG₂ min.

Equations

• Tsiakmakis2025.Negator.neg1.greek = Greek.StandardModern.Negation.dhen
• Tsiakmakis2025.Negator.neg2.greek = Greek.StandardModern.Negation.min

def Tsiakmakis2025.host? (e : Datum) : Option Host

The host of expletive negation a row names.

Equations

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

theorem Tsiakmakis2025.greek_expletive_negator (e : Datum) : e ∈ Examples.all → e.language = "mode1248" → e.feature? "use" = some "expletive" → Option.map (fun (x : Host) => List.map (fun (x : Morphology.Morph) => x.form) x.negator.greek.morphs) (host? e) = Option.map (fun (x : String) => [x]) (e.feature? "negator")

(20): each Greek host of expletive negation features the Greek spell-out of the negator its class assigns, dhen in an apparent host and min in a host proper.