Roussou 2010: Selecting complementizers

[Rou10]

Modern Greek complementizers in their dual capacity of being selected and of selecting. oti, pu, and an are nominal elements merging OUTSIDE the embedded clause (under N, as the matrix verb's internal argument); na merges INSIDE the lower C domain and re-opens the EPP position. The paper's informal semantic glosses are formalized here on their classical anchors, each denotation carrying its distribution:

• pu is definite ([Chr86]; the factive-definite lineage of [KK70]): puClause presupposes the proposition it locates, so factivity IS the definite's existence presupposition — projecting through negation (ex. 15b) where the presupposition-free otiClause is freely deniable (ex. 16).
• an denotes the Hamblin polar set {p, ¬p} (the paper adopts [AQ01]'s (6b), after [Ham73]): anClause is the inquisitive polar question — informationally inert, so some operator must close the open set. That polarity requirement is anItem, an NPI over the propositional domain whose licensing routes through the substrate's [Zwa98] / [vR03b] table: matrix negation (ex. 11), question — supplied lexically by rogatives (ex. 10) or structurally (ex. 2c) — and incorporated-negation predicates ('doubt', 'forget', ex. 14). True/False predicates ([AQ01]; ipothéto 'assume', ex. 7) are veridical embedders: no row of the table corresponds to them, and none could — that absence is the account's rendering of their blocking effect.
• na-clauses denote properties, [Chi84]'s control-complement layer, despite finite morphology (MG lacks infinitives): control (ex. 25–26) is the matrix argument saturating the open slot, and the outside mergers cannot embed a na-clause because they consume propositions — a type-level application failure.

Selection is thus not one-to-one (ex. 1–3): epistemic pistévo takes na only with present-tense matrix inflection (ex. 23) and focus licenses otherwise unselected pu (ex. 22) — both left as prose.

Main declarations

• PropQuant, MergeSite, CProfile, profile — the lexical specification table (§3–4)
• otiClause, puClause, anClause — the three denotations; puClause_factive, pu_projects_through_negation, puClause_strongEntails_oti, anClause_not_informative
• anItem — an as Polarity.Item; anItem_licensed routes its distribution through LicensingContext.licenses
• naLayer, na_layer_diverges_from_coding, comp_over_na_type_clash — the property-layer analysis of na
• factive_iff_definite — the fragment's factive flag coincides with definite propositional quantification

The lexical specification (§3–4)

inductive Roussou2010.PropQuant : Type

Propositional quantification contributed by an outside-merging complementizer: definite (binds a single proposition, locating it to a reference point) vs indefinite (ranges over a set of propositions).

• definite : PropQuant
• indefinite : PropQuant

@[implicit_reducible]

instance Roussou2010.instDecidableEqPropQuant : DecidableEq PropQuant

Equations

• Roussou2010.instDecidableEqPropQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Roussou2010.instReprPropQuant : Repr PropQuant

Equations

• Roussou2010.instReprPropQuant = { reprPrec := Roussou2010.instReprPropQuant.repr }

def Roussou2010.instReprPropQuant.repr : PropQuant → ℕ → Std.Format

Equations

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

inductive Roussou2010.MergeSite : Type

Merge site of a clause-typing element: outside the embedded clause (under N, as the matrix verb's internal argument — oti, pu, an) or inside its lower C domain (na, ex. 28).

• outside : MergeSite
• inside : MergeSite

@[implicit_reducible]

instance Roussou2010.instDecidableEqMergeSite : DecidableEq MergeSite

Equations

• Roussou2010.instDecidableEqMergeSite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Roussou2010.instReprMergeSite : Repr MergeSite

Equations

• Roussou2010.instReprMergeSite = { reprPrec := Roussou2010.instReprMergeSite.repr }

def Roussou2010.instReprMergeSite.repr : MergeSite → ℕ → Std.Format

Equations

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

structure Roussou2010.CProfile : Type

The lexical specification §4 attributes to a clause-typer: merge site, propositional quantification (none for inside-mergers, which bind no propositional variable), and polarity sensitivity.

• site : MergeSite
• quant : Option PropQuant
• polar : Bool

def Roussou2010.instDecidableEqCProfile.decEq (x✝ x✝¹ : CProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Roussou2010.instDecidableEqCProfile : DecidableEq CProfile

Equations

• Roussou2010.instDecidableEqCProfile = Roussou2010.instDecidableEqCProfile.decEq

@[implicit_reducible]

instance Roussou2010.instReprCProfile : Repr CProfile

Equations

• Roussou2010.instReprCProfile = { reprPrec := Roussou2010.instReprCProfile.repr }

def Roussou2010.instReprCProfile.repr : CProfile → ℕ → Std.Format

Equations

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

def Roussou2010.profile (c : Complementizer) : Option CProfile

The MG assignment (§3.1, §4): oti indefinite, an polar indefinite, pu definite — all outside — and na inside with no propositional quantification.

Equations

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

theorem Roussou2010.factive_iff_definite (c : Complementizer) : c ∈ [Greek.StandardModern.Complementizers.oti, Greek.StandardModern.Complementizers.pu, Greek.StandardModern.Complementizers.an, Greek.StandardModern.Complementizers.na] → (c.factive = some true ↔ ((profile c).bind fun (x : CProfile) => x.quant) = some PropQuant.definite)

Definiteness is what the fragment's lexical factive flag records ([Chr86]: pu as the definite article of the propositional domain). One way only: the factive doxastics (kséro, katalavéno) take indefinite oti (ex. 19), with weak, deniable, verb-derived factivity (ex. 15).

The denotations

def Roussou2010.otiClause {W : Type u_1} (p : Set W) : Semantics.Presupposition.PartialProp W

The oti-clause: a plain indefinite over propositions — presupposition-free assertion of its content. Any factive flavor is verb-derived and deniable (ex. 15–16).

Equations

• Roussou2010.otiClause p = { presup := fun (x : W) => True, assertion := fun (x : W) => x ∈ p }

def Roussou2010.puClause {W : Type u_1} (p : Set W) : Semantics.Presupposition.PartialProp W

The pu-clause: a definite over propositions ([Chr86]; [KK70]'s factive-definite) — it presupposes the proposition it locates to the reference point.

Equations

• Roussou2010.puClause p = { presup := fun (x : W) => x ∈ p, assertion := fun (x : W) => x ∈ p }

def Roussou2010.anClause {W : Type u_1} (p : Set W) : Question W

The an-clause: the Hamblin polar set {p, ¬p} (the paper's (6b), after [AQ01] and [Ham73]), as the inquisitive polar question.

Equations

• Roussou2010.anClause p = Question.polar p

theorem Roussou2010.puClause_factive {W : Type u_1} (p : Set W) (w : W) : Semantics.Presupposition.PartialProp.defined w (puClause p) ↔ w ∈ p

Factivity IS the definite's existence presupposition: the pu-clause is defined at a world exactly when its content holds there.

theorem Roussou2010.pu_projects_through_negation {W : Type u_1} (p : Set W) (w : W) : (Semantics.Presupposition.PartialProp.defined w (puClause p).neg ↔ w ∈ p) ∧ Semantics.Presupposition.PartialProp.defined w (otiClause p).neg

ex. 15b: the definite's presupposition projects through internal negation — denying a pu-clause still commits to its content — while the oti-clause stays defined everywhere, so denial carries no factive residue (ex. 16).

theorem Roussou2010.puClause_strongEntails_oti {W : Type u_1} (p : Set W) : (puClause p).strongEntails (otiClause p)

ex. 17 (thimáme oti/pu): the pu-reading strong-entails the oti-reading — Terrell's strong vs weak presupposition as strongEntails.

theorem Roussou2010.anClause_not_informative {W : Type u_1} (p : Set W) : ¬(anClause p).isInformative

The an-clause is informationally inert: it asserts nothing, only raising the {p, ¬p} issue. The polarity requirement is the demand that some operator close this open set.

an as a polarity item (§2)

def Roussou2010.anItem : Semantics.Polarity.Item

an as an NPI over the propositional domain: weak licensor requirement, with the paper's binder inventory mapped onto the substrate's licensing rows — matrix negation (ex. 11), question, whether supplied lexically by a rogative (ex. 10) or structurally (ex. 2c), and incorporated-negation predicates (amfivállo 'doubt', ksexnó 'forget', ex. 14). True/False predicates (ex. 7) are veridical embedders: no licensing row corresponds to them, which is the account's rendering of their blocking effect.

Equations

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

theorem Roussou2010.anItem_isNPI : anItem.isNPI

an's polarity is a bona fide licensor requirement.

theorem Roussou2010.anItem_licensed (c : Features.LicensingContext) : c ∈ anItem.licensingContexts → c.licenses anItem

Each context of the inventory in fact licenses an under the substrate's keystone ([Zwa98] strength on the signature rows, [vR03b] entropy on questions).

na and the property layer (§3.2, §4)

def Roussou2010.naLayer : Semantics.Composition.TypeShifting.ComplSemLayer

na re-opens the EPP position, so the na-clause denotes a property — [Chi84]'s control-complement layer — despite finite morphology.

Equations

• Roussou2010.naLayer = Semantics.Composition.TypeShifting.ComplSemLayer.property

theorem Roussou2010.na_layer_diverges_from_coding : naLayer = Semantics.Composition.TypeShifting.ComplSemLayer.property ∧ Chierchia1984.complSemLayer ComplementType.finiteClause = some Semantics.Composition.TypeShifting.ComplSemLayer.proposition

MG detaches the property layer from nonfinite coding: the coding-based mapping sends finite clauses to the propositional layer (Chierchia1984.complSemLayer), but the finite na-clause is a property. Control (ex. 25–26) is the matrix argument saturating the open slot.

theorem Roussou2010.comp_over_na_type_clash (b : Intensional.Ty) : Semantics.Composition.Tree.canApply (Intensional.Ty.t ⇒ b) (Intensional.Ty.e ⇒ Intensional.Ty.t) = none

The merge-site split cashed out at type level (p. 597): an outside merger consumes a proposition (.t), while the na-clause — its EPP re-opened — is a property, .fn .e .t; application is undefined whatever the merger returns. Relative pu + na (ex. 31) escapes because relative pu binds an individual variable instead.