Documentation

Studies.Roussou2010

Roussou (2010): Selecting complementizers #

This file formalizes the paper's account of the Modern Greek complementizers as nominal elements, each with a lexical specification that fixes what it can embed and what can embed it (profile). oti, an, and pu merge outside the clause, as the internal argument of the matrix verb, and take a proposition: oti is an indefinite over propositions, an an indefinite that is a polarity item, and pu a definite, which is why a pu-clause is factive, its content presupposed and projecting through negation (puClause_ne_zero_iff, pu_projects_through_negation), while the oti-clause of the same verb carries only the weak, deniable presupposition the verb supplies. na merges inside the clause and reopens the subject position, so a na-clause is a property rather than a proposition and cannot be embedded under the outside mergers (comp_over_na_type_clash). The distribution follows from the specifications and the lexical semantics of the selecting predicate: an needs a binder, an interrogative predicate or a matrix negation or question over a proposition-taking one (polar_needs_binder); pu needs an emotive factive, a recollection reading, or a focused predicate; na is taken freely by volitionals and verbs of knowing, with control, and by epistemic predicates only in the present tense (epistemic_na_present). The paper's examples are rows, read by rows as the analysis predicts.

Implementation notes #

The matrix predicates are entries of the Greek fragment, classified for selection as the paper classifies them; the classification is the paper's, with the recollection sense of thimáme the fragment's stative entry, and nomízo's need of an operator for its na-complement a lexical mark. The type-level incompatibility of the outside mergers with na is stated on the composition substrate's types, propositions as t and properties as ⟨e,t⟩. Control, the dynamic modal reading of kséro with na, the Romance and English parallels, and the paper's argument against uninterpretable features are not formalized.

References #

The lexical specification #

inductive Roussou2010.Quantification :

An outside-merging complementizer contributes a quantification over propositions — an indefinite ranging over a set of propositions, a polar indefinite requiring a binder, or a definite binding a single proposition.

indefinite : Quantification
polar : Quantification
definite : Quantification

Instances For

@[instance_reducible]

instance Roussou2010.instDecidableEqQuantification :

DecidableEq Quantification

Equations

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

def Roussou2010.instReprQuantification.repr :

Quantification → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Roussou2010.instReprQuantification :

Repr Quantification

Equations

Roussou2010.instReprQuantification = { reprPrec := Roussou2010.instReprQuantification.repr }

inductive Roussou2010.Spec :

A clause-typing element is lexically specified as merging outside the clause, as the matrix verb's argument, with a quantification over propositions, or inside its lower C domain, binding no propositional variable.

outside (q : Quantification) : Spec
inside : Spec

Instances For

@[instance_reducible]

instance Roussou2010.instDecidableEqSpec :

DecidableEq Spec

Equations

Roussou2010.instDecidableEqSpec = Roussou2010.instDecidableEqSpec.decEq

def Roussou2010.instDecidableEqSpec.decEq (x✝ x✝¹ : Spec) :

Decidable (x✝ = x✝¹)

Equations

Roussou2010.instDecidableEqSpec.decEq (Roussou2010.Spec.outside a) (Roussou2010.Spec.outside b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Roussou2010.instDecidableEqSpec.decEq (Roussou2010.Spec.outside q) Roussou2010.Spec.inside = isFalse ⋯
Roussou2010.instDecidableEqSpec.decEq Roussou2010.Spec.inside (Roussou2010.Spec.outside q) = isFalse ⋯
Roussou2010.instDecidableEqSpec.decEq Roussou2010.Spec.inside Roussou2010.Spec.inside = isTrue ⋯

Instances For

@[instance_reducible]

instance Roussou2010.instReprSpec :

Repr Spec

Equations

Roussou2010.instReprSpec = { reprPrec := Roussou2010.instReprSpec.repr }

def Roussou2010.instReprSpec.repr :

Spec → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
Roussou2010.instReprSpec.repr Roussou2010.Spec.inside prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Roussou2010.Spec.inside")).group prec✝

Instances For

def Roussou2010.profile (c : Complementizer) :

Option Spec

Among the Modern Greek complementizers, oti is indefinite, an polar and pu definite, all merging outside, and na merges inside.

Equations

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

Instances For

theorem Roussou2010.factive_iff_definite (c : Complementizer) :

c ∈ Greek.StandardModern.Complementizers.complementizers → (c.factive = some true ↔ profile c = some (Spec.outside Quantification.definite))

The fragment's lexical factivity is definiteness — the one definite complementizer is the one factive one, the factive reading of an oti-clause being the verb's.

The denotations #

noncomputable def Roussou2010.otiClause {W : Type u_1} (p : Set W) :

W → SignType

The oti-clause is an indefinite over propositions, asserting its content without presupposition.

Equations

Roussou2010.otiClause p w = SignType.ofProp (w ∈ p)

Instances For

noncomputable def Roussou2010.puClause {W : Type u_1} (p : Set W) :

W → SignType

The pu-clause is a definite over propositions, presupposing the proposition it locates and so true wherever it is defined.

Equations

Roussou2010.puClause p = p.indicator 1

Instances For

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

The an-clause is the polar set of the proposition and its negation.

Equations

Roussou2010.anClause p = Question.polar p

Instances For

theorem Roussou2010.puClause_ne_zero_iff {W : Type u_1} (p : Set W) (w : W) :

puClause p w ≠ 0 ↔ w ∈ p

Factivity is the definite's 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) :

((-puClause p) w ≠ 0 ↔ w ∈ p) ∧ (-otiClause p) w ≠ 0

The presupposition of the pu-clause projects through negation, so denying it still commits to its content, while the oti-clause is defined everywhere and its denial carries no factive residue.

theorem Roussou2010.posExt_puClause_subset {W : Type u_1} (p : Set W) :

Trivalent.posExt (puClause p) ⊆ Trivalent.posExt (otiClause p)

The pu-clause strongly entails the oti-clause, strong presupposition against weak.

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

¬(anClause p).IsInformative

The an-clause asserts nothing, raising only the issue its binder must settle.

theorem Roussou2010.comp_over_na_type_clash (b : Montague.Ty) :

HeimKratzer.Tree.tyBinary (Montague.Ty.t ⇒ b) (Montague.Ty.e ⇒ Montague.Ty.t) = none

An outside merger takes a proposition, and a na-clause, its subject position reopened, is a property, so no composition mode combines them, whatever the merger returns.

Selection #

inductive Roussou2010.Class :

The paper distinguishes these classes of selecting predicate — interrogatives, which bind the polar complementizer themselves; verbs of knowing, which take any complement; epistemic verbs, which take na only in the present tense, some of them only under an operator; volitionals, which take na alone; emotive factives, which take pu alone; emotives that take pu on a factive and oti on a non-factive reading; factive non-emotives, which take oti and not pu; verbs of saying; and the recollection sense of remember, which takes pu.

interrogative : Class
knowing : Class
epistemic (needsOperator : Bool) : Class
volitional : Class
emotiveFactive : Class
emotive : Class
factive : Class
saying : Class
recollection : Class

Instances For

@[instance_reducible]

instance Roussou2010.instDecidableEqClass :

DecidableEq Class

Equations

Roussou2010.instDecidableEqClass = Roussou2010.instDecidableEqClass.decEq

def Roussou2010.instDecidableEqClass.decEq (x✝ x✝¹ : Class) :

Decidable (x✝ = x✝¹)

Equations

Instances For

def Roussou2010.instReprClass.repr :

Class → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
Roussou2010.instReprClass.repr Roussou2010.Class.knowing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Roussou2010.Class.knowing")).group prec✝
Roussou2010.instReprClass.repr Roussou2010.Class.emotive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Roussou2010.Class.emotive")).group prec✝
Roussou2010.instReprClass.repr Roussou2010.Class.factive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Roussou2010.Class.factive")).group prec✝
Roussou2010.instReprClass.repr Roussou2010.Class.saying prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Roussou2010.Class.saying")).group prec✝

Instances For

@[instance_reducible]

instance Roussou2010.instReprClass :

Repr Class

Equations

Roussou2010.instReprClass = { reprPrec := Roussou2010.instReprClass.repr }

def Roussou2010.classOf (v : Verb) :

Option Class

The paper's classification of the fragment's predicates.

Equations

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

Instances For

structure Roussou2010.Config :

A selection configuration records the predicate's class, the complementizer, and the matrix operators and tenses the paper finds relevant.

cls : Class
comp : Complementizer
negated : Bool
question : Bool
focused : Bool
past : Bool
embeddedPast : Bool

Instances For

def Roussou2010.instDecidableEqConfig.decEq (x✝ x✝¹ : Config) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance Roussou2010.instDecidableEqConfig :

DecidableEq Config

Equations

Roussou2010.instDecidableEqConfig = Roussou2010.instDecidableEqConfig.decEq

def Roussou2010.instReprConfig.repr :

Config → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Roussou2010.instReprConfig :

Equations

Roussou2010.instReprConfig = { reprPrec := Roussou2010.instReprConfig.repr }

def Roussou2010.Class.TakesProposition :

The class takes a propositional complement, so an indefinite complementizer.

Equations

Roussou2010.Class.knowing.TakesProposition = True
(Roussou2010.Class.epistemic needsOperator).TakesProposition = True
Roussou2010.Class.emotive.TakesProposition = True
Roussou2010.Class.factive.TakesProposition = True
Roussou2010.Class.saying.TakesProposition = True
Roussou2010.Class.recollection.TakesProposition = True
Roussou2010.Class.interrogative.TakesProposition = False
Roussou2010.Class.volitional.TakesProposition = False
Roussou2010.Class.emotiveFactive.TakesProposition = False

Instances For

@[instance_reducible]

instance Roussou2010.instDecidablePredClassTakesProposition :

DecidablePred Class.TakesProposition

Equations

Roussou2010.instDecidablePredClassTakesProposition Roussou2010.Class.knowing = isTrue trivial
Roussou2010.instDecidablePredClassTakesProposition (Roussou2010.Class.epistemic needsOperator) = isTrue trivial
Roussou2010.instDecidablePredClassTakesProposition Roussou2010.Class.emotive = isTrue trivial
Roussou2010.instDecidablePredClassTakesProposition Roussou2010.Class.factive = isTrue trivial
Roussou2010.instDecidablePredClassTakesProposition Roussou2010.Class.saying = isTrue trivial
Roussou2010.instDecidablePredClassTakesProposition Roussou2010.Class.recollection = isTrue trivial
Roussou2010.instDecidablePredClassTakesProposition Roussou2010.Class.interrogative = isFalse Roussou2010.instDecidablePredClassTakesProposition._proof_1
Roussou2010.instDecidablePredClassTakesProposition Roussou2010.Class.volitional = isFalse Roussou2010.instDecidablePredClassTakesProposition._proof_2
Roussou2010.instDecidablePredClassTakesProposition Roussou2010.Class.emotiveFactive = isFalse Roussou2010.instDecidablePredClassTakesProposition._proof_3

def Roussou2010.Class.TakesSet :

The class takes a set of propositions under an operator — the proposition-taking classes other than the epistemic ones.

Equations

Roussou2010.Class.knowing.TakesSet = True
Roussou2010.Class.factive.TakesSet = True
Roussou2010.Class.saying.TakesSet = True
x✝.TakesSet = False

Instances For

@[instance_reducible]

instance Roussou2010.instDecidablePredClassTakesSet :

DecidablePred Class.TakesSet

Equations

def Roussou2010.Licensed (k : Config) :

The complementizer is licensed in the configuration — oti by a proposition-taking predicate; an by an interrogative predicate, or by a matrix negation or question over a predicate taking a set of propositions; pu by an emotive factive, an emotive, a recollection reading, or a focused predicate; na by a volitional, by a verb of knowing with a present-tense complement, or by a present-tense epistemic, with an operator when the verb demands one.

Equations

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

Instances For

@[instance_reducible]

instance Roussou2010.instDecidableLicensed (k : Config) :

Decidable (Licensed k)

Equations

Roussou2010.instDecidableLicensed k = id inferInstance

theorem Roussou2010.polar_needs_binder (k : Config) (hc : k.comp = Greek.StandardModern.Complementizers.an) (h : Licensed k) :

k.cls = Class.interrogative ∨ k.negated = true ∨ k.question = true

The polar complementizer needs a binder — an interrogative predicate, or a matrix negation or question.

theorem Roussou2010.epistemic_na_present (k : Config) (b : Bool) (hc : k.comp = Greek.StandardModern.Complementizers.na) (hk : k.cls = Class.epistemic b) (h : Licensed k) :

¬k.past = true

An epistemic predicate takes na only in the present tense.

The rows #

def Roussou2010.verbOf :

String → Option Verb

The fragment entry named by a row.

Equations

Roussou2010.verbOf "ksero" = some Greek.StandardModern.Verbs.ksero
Roussou2010.verbOf "anarotjeme" = some Greek.StandardModern.Verbs.anarotjeme
Roussou2010.verbOf "xerome" = some Greek.StandardModern.Verbs.xerome
Roussou2010.verbOf "thelo" = some Greek.StandardModern.Verbs.thelo
Roussou2010.verbOf "pistevo" = some Greek.StandardModern.Verbs.pistevo
Roussou2010.verbOf "nomizo" = some Greek.StandardModern.Verbs.nomizo
Roussou2010.verbOf "thimame" = some Greek.StandardModern.Verbs.thimame
Roussou2010.verbOf "thimameStat" = some Greek.StandardModern.Verbs.thimameStat
Roussou2010.verbOf "paradhexome" = some Greek.StandardModern.Verbs.paradhexome
Roussou2010.verbOf "anisixo" = some Greek.StandardModern.Verbs.anisixo
Roussou2010.verbOf "leo" = some Greek.StandardModern.Verbs.leo
Roussou2010.verbOf x✝ = none

Instances For

def Roussou2010.datum (r : Datum) :

Option (Config × Judgment)

A row's configuration and judgment.

Equations

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

Instances For

def Roussou2010.data :

List (Config × Judgment)

The paper's examples.

Equations

Roussou2010.data = List.filterMap Roussou2010.datum Roussou2010.Examples.all

Instances For

theorem Roussou2010.data_length :

data.length = Examples.all.length

Every row has its configuration.

theorem Roussou2010.rows (d : Config × Judgment) :

d ∈ data → (d.2 = Judgment.acceptable ↔ Licensed d.1)

The examples are acceptable exactly when their complementizer is licensed.