Documentation

Linglib.Fragments.Greek.TemporalConnectives

Greek Temporal Connectives Fragment #

@cite{giannakidou-2002} @cite{giannakidou-1998}

Greek lexicalizes the two-until distinction and the veridicality asymmetry through mood selection:

πριν / prin ('before'): requires subjunctive (in modern Greek), patterns with English before. Non-veridical complement, licenses NPIs. Differs from NPI-until on actualization (@cite{giannakidou-2002}, §6).
μέχρι / mexri ('until'): requires indicative, patterns with English durative until. Veridical complement, requires imperfective/stative main clause, does NOT license NPIs.
αφού / afou ('after'): veridical complement.
όταν / otan ('when'): veridical complement, temporal coincidence.

The subjunctive/indicative mood split independently diagnoses the veridicality distinction: subjunctive signals non-veridicality (the complement event is presented as unrealized), while indicative signals veridicality (the complement event is presented as factual). This parallels Japanese tense marking (mae non-past / ato past) diagnosed in the @cite{ogihara-steinert-threlkeld-2024} data.

def Fragments.Greek.TemporalConnectives.prin :

English.TemporalExpressions.TemporalExprEntry

Greek πριν / prin ('before'): non-veridical, subjunctive complement. Licenses NPIs. Default before-start reading. "Efije prin na erthi o Janis." ('She left before Janis came.')

Equations

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

Instances For

def Fragments.Greek.TemporalConnectives.mexri :

English.TemporalExpressions.TemporalExprEntry

Greek μέχρι / mexri ('until'): veridical, indicative complement. Does NOT license NPIs. Requires imperfective/stative main clause. "I Maria perimine mexri irthi o Janis." ('Maria waited until Janis came.')

Equations

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

Instances For

def Fragments.Greek.TemporalConnectives.afou :

English.TemporalExpressions.TemporalExprEntry

Greek αφού / afou ('after'): veridical, indicative complement. "Efije afou irthe o Janis." ('She left after Janis came.')

Equations

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

Instances For

def Fragments.Greek.TemporalConnectives.otan :

English.TemporalExpressions.TemporalExprEntry

Greek όταν / otan ('when'): veridical, temporal coincidence. "Efije otan irthe o Janis." ('She left when Janis came.')

Equations

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

Instances For

def Fragments.Greek.TemporalConnectives.paraMonon :

English.TemporalExpressions.TemporalExprEntry

Greek παρά μονον / para monon (lit. 'but only'): eventive NPI-until. Lexically distinct from both mexri (durative until) and prin (before). Requires anti-veridical trigger (negation, 'without'). Scalar: introduces a scale of contextually relevant times. Forces punctual/eventive reading.

@cite{giannakidou-2002}, §3.2, ex. (39): the event P occurs at the boundary time Q, and no earlier event of type P occurred. Actualization is an entailment, not an implicature — cancellation yields contradiction (ex. 38: '#The princess didn't arrive until midnight. She didn't even arrive that night.').

"I prigipisa dhen (apo)kimithike para monon ta mesanixta." ('The princess didn't fall asleep until midnight.')

Equations

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

Instances For

theorem Fragments.Greek.TemporalConnectives.two_until_lexicalized :

prin.form ≠ mexri.form ∧ prin.order ≠ mexri.order

Greek lexicalizes the two-until distinction with different lexemes: prin (NPI-type, = before) vs mexri (durative endpoint type).

theorem Fragments.Greek.TemporalConnectives.prin_is_before :

prin.order = English.TemporalExpressions.TemporalOrder.before

Prin is semantically before (order =.before), confirming Karttunen's identity: NPI-until = ¬before.

theorem Fragments.Greek.TemporalConnectives.mexri_is_until :

mexri.order = English.TemporalExpressions.TemporalOrder.until_

Mexri is semantically until (order =.until_), the true durative endpoint connective.

Greek veridicality asymmetry: prin non-veridical, afou/mexri veridical. This is diagnosed by mood selection: subjunctive (prin) vs indicative (afou, mexri, otan).

theorem Fragments.Greek.TemporalConnectives.npi_pattern :

prin.licensesNPI = true ∧ mexri.licensesNPI = false ∧ afou.licensesNPI = false ∧ otan.licensesNPI = false

NPI licensing: only prin (before-type) licenses NPIs. Neither the durative until (mexri) nor after/when license NPIs. This confirms the cross-linguistic generalization: NPI licensing tracks the before-type semantics, not the until label.

Greek prin and English before agree on all semantic properties.

Greek afou and English after agree on all semantic properties.

Greek mexri and English until agree on all semantic properties.

Greek otan and English when agree on all semantic properties.

inductive Fragments.Greek.TemporalConnectives.MoodType :

Mood selection type: subjunctive (non-veridical) vs indicative (veridical).

subjunctive : MoodType
indicative : MoodType

Instances For

instance Fragments.Greek.TemporalConnectives.instDecidableEqMoodType :

DecidableEq MoodType

Equations

Fragments.Greek.TemporalConnectives.instDecidableEqMoodType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Greek.TemporalConnectives.instReprMoodType.repr :

MoodType → ℕ → Std.Format

Equations

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

Instances For

instance Fragments.Greek.TemporalConnectives.instReprMoodType :

Equations

Fragments.Greek.TemporalConnectives.instReprMoodType = { reprPrec := Fragments.Greek.TemporalConnectives.instReprMoodType.repr }

def Fragments.Greek.TemporalConnectives.instBEqMoodType.beq :

MoodType → MoodType → Bool

Equations

Fragments.Greek.TemporalConnectives.instBEqMoodType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Fragments.Greek.TemporalConnectives.instBEqMoodType :

Equations

Fragments.Greek.TemporalConnectives.instBEqMoodType = { beq := Fragments.Greek.TemporalConnectives.instBEqMoodType.beq }

def Fragments.Greek.TemporalConnectives.moodSelection :

English.TemporalExpressions.TemporalOrder → MoodType

Greek mood selection for temporal connectives.

Equations

Instances For

theorem Fragments.Greek.TemporalConnectives.three_way_lexicalized :

prin.form ≠ mexri.form ∧ prin.form ≠ paraMonon.form ∧ mexri.form ≠ paraMonon.form

Greek lexicalizes a THREE-way distinction: prin (before), mexri (durative until), and para monon (eventive/NPI until). All three have distinct surface forms.

theorem Fragments.Greek.TemporalConnectives.npi_three_way :

prin.licensesNPI = true ∧ mexri.licensesNPI = false ∧ paraMonon.licensesNPI = false

Para monon is an NPI (it doesn't license NPIs; it IS one). Prin licenses NPIs. Mexri does not. This three-way pattern on NPI properties is unique to Greek and confirms that the three connectives occupy distinct positions in the polarity hierarchy.

theorem Fragments.Greek.TemporalConnectives.paraMonon_nonveridical :

paraMonon.complementVeridical = false ∧ paraMonon.complementVeridical = prin.complementVeridical ∧ paraMonon.complementVeridical ≠ mexri.complementVeridical

Para monon is non-veridical (like prin), not veridical (like mexri). Both prin and para monon appear in non-veridical contexts, but only para monon requires an anti-veridical trigger (negation).

theorem Fragments.Greek.TemporalConnectives.paraMonon_punctual :

paraMonon.forcesPunctual = true ∧ mexri.forcesPunctual = false

Para monon forces a punctual reading; mexri does not. This captures the eventive vs durative distinction at the fragment level.

theorem Fragments.Greek.TemporalConnectives.paraMonon_order :

paraMonon.order = mexri.order ∧ paraMonon.order ≠ prin.order

Para monon shares temporal ordering with mexri (both are .until_) but differs from prin (which is .before). The semantic difference between para monon and mexri is captured by punctuality and veridicality, not by temporal order.